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
9 years ago
c5c5654068
Added bzreax script ; added uninstall target in Makefiles
9 years ago
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
9 years ago
95aa03ed21
Interface for new incremental API of menhir parsers' relies on MenhirLib
9 years ago
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"
10 years ago
177f5f9f3e
Avoid exporting contract-less or parametric nodes into DCS tool formats.
10 years ago
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.
10 years ago
c86d7af0b1
Introducing a hack to normalize comparison of tuples in Heptagon.
10 years ago
045e624f94
Bug fix with controllable-less contracts in ControllableNbac exporter.
10 years ago
2a0927bd98
Bug correction in maybe_ctrln_pass
10 years ago
cbcf8b9ac0
Using unqualified names for string representation of constructors in C backend.
...
+ minor modifications in various places.
10 years ago
d4fe017864
Bug correction in names of C functions for converting constructors to string.
10 years ago
2d00f0a91c
Fix sink state variable generation in Controllable-Nbac export.
10 years ago
0afdb16c57
Requalify enumeration types only when exporintg to Controllable-Nbac.
10 years ago
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.
10 years ago
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.
10 years ago
d84ae09cab
Bug fix (preprocessor variable).
10 years ago
8551a91a05
Fix configure script for optional compilation of `ctrl2ept'.
10 years ago
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.
10 years ago
541dd83fca
Optional compilation of Controllable-Nbac-related modules and tools.
10 years ago
3b27de8146
Configure script now checks for `reatk.ctrlnbac' package.
10 years ago
5506690de5
Merge branch 'decade' into ctrl-n
10 years ago
9a29c6fa4b
Upgrading to new ReaTK API (>= 0.9.4).
10 years ago
1f2e084e6e
Fixed a bug where loops were not generated for copying arrays.
10 years ago
99ab12aa13
Fixed warnings.
10 years ago
c3c7a331b6
Using ReaTK's Controllable-Nbac backend library.
10 years ago
850e8522dd
Merge branch 'decade' into ctrl-n
10 years ago
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).
10 years ago
8650ac5695
Version 1.00.06
10 years ago
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
10 years ago
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).
10 years ago
9c4b3f3267
Version 1.00.05
10 years ago
2d96b60c49
Bug corrections in contracts
...
Contracts handling : added variables for assume/guarantee
parts of subnodes as defined names in b_defnames
10 years ago
1a373b84eb
Added some tests
...
Tests from image_filters
Examples of array iterators used
10 years ago
c61e01f19b
Correct handling of comparison operators in Sigali
...
- bug fix: comparison between two non-constant integer expressions in Sigali
- bug fix: correct handling of "=" and "<>" operators in Sigali
10 years ago
4f7413282e
Merge branch 'decade' into ctrl-n
11 years ago
c132b53732
Handle `when' operators in general expressions, in Controllable-Nbac backend.
...
- CtrlNbacGen: ignore sub-sampling in general expressions.
11 years ago
934c9f9a85
Handle `when' operators for non-Boolean expressions in Controllable-Nbac backend.
11 years ago
d27db41485
Version 1.00.03
11 years ago
808b9772f3
Merge branch 'decade' into ctrl-n
11 years ago
71497a82b2
Corrected bug in inline_extvalues
...
Inline_extvalues: added local variables of contracts into environments
11 years ago
ae6a3aac2e
Attractivity property of Controllable-Nbac output; minor refactorings.
11 years ago
216550c0d1
Fixed warnings & documentation comments.
...
- gitignore: ignore files generated by `configure' script.
11 years ago
10bdab4dc6
Exclusively use ocamlfind; source documentation generation.
...
- Stripped portions of `myocamlbuild{,_config}.ml' that seem useless
when `-use-ocamlfind' is passed to ocamlbuild.
- Added some code in `myocamlbuild_config.ml' to be able to generate
documentation by merging interface and implementation files.
11 years ago
8aeab651ce
First draft for Controllable-Nbac format generation.
...
- CtrlNbac: new module for internal representation and output code for
Controllable-Nbac format;
- CtrlNbacGen: translation into Controllable-Nbac of Minils nodes
necessitating controller synthesis; the insertion of calls to
controllers is not yet done, and the nodes are left unchanged.
11 years ago
106b1339ac
Corrected Makefile for binary distribution
11 years ago
5b98f9cdf6
Version 1.00.02
...
Added CHANGES file
11 years ago
13d616c930
Scrollbars on inputs/outputs of hepts
...
Allowed shrinking hepts main window and added scrollbars on frames
for inputs and outputs.
11 years ago
f5872cbcf4
Change URL for sim2chro in manual
...
- change URL for download of sim2chro (towards Lustre v4 distribution)
- added GTKWave in INSTALL
- change font of pdf manual
11 years ago
c0b84bd186
Abstraction of integers for Sigali
...
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
11 years ago
Gwenaël Delaval
Nicolas Berthier
Valentin Perrelle