2c1717e99f
Removal of -custom option for compilation
...
-custom option trigger bugs with opam
2015-12-11 17:00:29 +01:00
2777753b7e
Cleanup : removal of useless files
2015-12-11 16:58:26 +01:00
65908e7ca3
New configure script options to enable/disable byte/native targets
2015-09-21 18:53:52 +02:00
fb6755efb2
Bugfix in ctrl2ept: do not reset symbol table after loading type declarations
2015-09-21 15:17:30 +02:00
14a7b67a70
New option to force abstraction of infinite-domain state variables in ctrln export
...
Also add an option to silence related warnings
2015-09-18 14:11:04 +02:00
2d874f8070
New option to silence warnings about untranslatable constructs
2015-09-18 13:59:33 +02:00
74b94c9718
Fix handling of nodes without actual controllers by ctrl2ept
...
These changes allow to handle the case where contracts are only used
for verification purposes, in which case the functions generated by
ReaX have no outputs and are not functions stricto sensu. Indeed, in
this case the new controller module still needs to be declared and
compiled as we may have re-qualified types during the generation of
the Controllable-Nbac code: we moved all types declared in the
original module into the controller module to break cyclic module
dependencies that would otherwise be introduced if the controller is
expressed using data of such types.
2015-09-18 09:51:41 +02:00
bb324eee17
Update of Makefile-distrib for heptreax manual inclusion
2015-09-17 17:22:46 +02:00
0a65ffc8e2
Update of example Extern_C
2015-09-17 17:20:31 +02:00
3b81368074
CHANGES for version 1.01.00
2015-09-17 16:58:41 +02:00
8dbb283310
User manual for Heptagon+ReaX
2015-09-17 16:54:10 +02:00
015875b279
Math module
...
The Math module contains mathematic functions.
2015-09-17 16:51:24 +02:00
f720c1844f
Added example heptreax
...
Example heptreax, use of ReaX controller synthesis tool for verification
and controller synthesis.
2015-09-17 16:21:05 +02:00
d5ee87b7ed
Added example Markov
...
Example Markov : simulation of a Markov chain.
Use of a Random module, external call to C rand() function.
2015-09-17 11:17:29 +02:00
61f043856a
Version 1.01.00
2015-09-17 10:29:20 +02:00
9b75408f23
Bug correction in reset
...
"e1 fby e2" was not handled in the reset pass.
2015-09-04 17:35:12 +02:00
fd4dffef62
Adding tests
2015-09-04 17:33:49 +02:00
e0bbc838d5
Allow use of declared parameters within parameters
...
Allow this node :
node f<<m:int; t1: int^m>>(a:int^m) = (o:int^m)
let
o = map<<m>> (+)(a, t1);
tel
2015-02-27 16:15:55 +01:00
c5c5654068
Added bzreax script ; added uninstall target in Makefiles
2015-02-27 15:50:21 +01:00
0d1aef8c78
Bug correction: support of enumerated types as input for simulation
...
- use of a buffer to translate enumerated types from string to enum value
- hepts : correct interface with main
2015-02-27 15:39:39 +01:00
95aa03ed21
Interface for new incremental API of menhir parsers' relies on MenhirLib
2015-01-28 18:08:53 +01:00
3dfbeffeb6
Added syntax for reachability and attractivity in contracts
...
Contracts can now comprise a list of objectives (in any order).
One objective can be (e being a Boolean heptagon expression) :
- invariance, with the syntax "enforce e"
- reachability, "reachable e"
- attractivity, "attractive e"
2015-01-06 00:26:59 +01:00
177f5f9f3e
Avoid exporting contract-less or parametric nodes into DCS tool formats.
2014-12-15 15:56:37 +01:00
307f3d8418
Controllable-Nbac import&export now support relocation of alias types.
...
- Controllable-Nbac export (CtrlNbacGen): correct handling of float
expressions, as well as alias types;
- Controllable-Nbac controller importer (CtrlNbacAsEpt): Declaration
of enumerated types and aliases that are relocated to controller
modules is now performed based on the interface. Dependencies
between type aliases are also taken into account now;
- ctrl2ept tool: correct loading of pervasives module.
2014-12-15 15:56:04 +01:00
c86d7af0b1
Introducing a hack to normalize comparison of tuples in Heptagon.
2014-12-15 15:42:37 +01:00
045e624f94
Bug fix with controllable-less contracts in ControllableNbac exporter.
2014-12-02 10:20:15 +01:00
2a0927bd98
Bug correction in maybe_ctrln_pass
2014-12-01 14:44:08 +01:00
cbcf8b9ac0
Using unqualified names for string representation of constructors in C backend.
...
+ minor modifications in various places.
2014-11-13 09:45:15 +01:00
d4fe017864
Bug correction in names of C functions for converting constructors to string.
2014-10-31 15:40:05 +01:00
2d00f0a91c
Fix sink state variable generation in Controllable-Nbac export.
2014-10-31 14:42:37 +01:00
0afdb16c57
Requalify enumeration types only when exporintg to Controllable-Nbac.
2014-10-31 14:16:05 +01:00
39aa0e13c1
Ugly fix for handling enumerated types when exporting to Controllable-Nbac.
...
To avoid cyclic module dependencies (that show up when trying to
compile, e.g, the generated C code), enumerated types declared in the
main program are now "moved" into the module containing the generated
controllers.
2014-10-30 12:01:25 +01:00
be21bf31d8
Insertion of call to controller(s) when exporting to Controllable-Nbac node.
...
To enable recovery of parameter and output ordering by `ctrl2ept', the
Controllable-Nbac generation procedure now declares a new module
dedicated to the encapsulation of the controller functions yet to be
synthesized.
Handling of type declarations are probably buggy.
2014-10-28 16:43:13 +01:00
d84ae09cab
Bug fix (preprocessor variable).
2014-10-23 11:23:36 +02:00
8551a91a05
Fix configure script for optional compilation of `ctrl2ept'.
2014-10-23 11:06:32 +02:00
bc17d71e3f
New tool `ctrl2ept' for translating ReaX's output functions into Heptagon
...
Compilation of the tool is dependent on the presence of the
`reatk.ctrlNbac' library.
2014-10-22 17:46:05 +02:00
541dd83fca
Optional compilation of Controllable-Nbac-related modules and tools.
2014-10-21 15:41:40 +02:00
3b27de8146
Configure script now checks for `reatk.ctrlnbac' package.
2014-10-21 13:43:30 +02:00
5506690de5
Merge branch 'decade' into ctrl-n
2014-10-03 10:58:41 +02:00
9a29c6fa4b
Upgrading to new ReaTK API (>= 0.9.4).
2014-10-03 10:57:23 +02:00
1f2e084e6e
Fixed a bug where loops were not generated for copying arrays.
2014-06-25 18:53:34 +02:00
99ab12aa13
Fixed warnings.
2014-03-18 11:01:56 +01:00
c3c7a331b6
Using ReaTK's Controllable-Nbac backend library.
2014-03-18 10:58:57 +01:00
850e8522dd
Merge branch 'decade' into ctrl-n
2014-03-03 16:46:21 +01:00
478e621ac5
Handling of contracts in Mls2obc
...
Handling of contracts when the "z3z" target is off. Equations of contracts are
put into the node in the Mls2obc pass (done by the "z3z" code generation).
2014-02-22 23:53:49 +01:00
8650ac5695
Version 1.00.06
2014-02-21 18:12:07 +01:00
bcba3569ed
Added tests - types, constants, contracts
...
- ais.ept: tests inclusion of array types into structure types
- ce.ept: constant propagation
- contract.ept: contract constructs
- contract_automaton.ept: contract constructs and automata
2014-02-21 17:49:51 +01:00
e885f82e00
Bug correction/feature adding: abstraction within contracts
...
Allowing additional inputs from abstractions within contracts. Thus,
calling non-inlined subnodes is allowed, as well as operations on
non-Boolean inputs or states (in contracts).
2014-02-21 17:39:37 +01:00
9c4b3f3267
Version 1.00.05
2014-01-28 16:31:16 +01:00
2d96b60c49
Bug corrections in contracts
...
Contracts handling : added variables for assume/guarantee
parts of subnodes as defined names in b_defnames
2014-01-27 00:26:24 +01:00
Gwenaël Delaval