jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity
1082 commits 2 branches 0 tags 6.9 MiB
Commit graph

1082 commits

This branch
This branch
All branches
Author SHA1 Message Date
Gwenaël Delaval
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
Gwenaël Delaval
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
Gwenaël Delaval
61f043856a Version 1.01.00 2015-09-17 10:29:20 +02:00
Gwenaël Delaval
9b75408f23 Bug correction in reset 
"e1 fby e2" was not handled in the reset pass.
 2015-09-04 17:35:12 +02:00
Gwenaël Delaval
fd4dffef62 Adding tests 2015-09-04 17:33:49 +02:00
Gwenaël Delaval
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
Gwenaël Delaval
c5c5654068 Added bzreax script ; added uninstall target in Makefiles 2015-02-27 15:50:21 +01:00
Gwenaël Delaval
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
Nicolas Berthier
95aa03ed21 Interface for new incremental API of menhir parsers' relies on MenhirLib 2015-01-28 18:08:53 +01:00
Gwenaël Delaval
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
Nicolas Berthier
177f5f9f3e Avoid exporting contract-less or parametric nodes into DCS tool formats. 2014-12-15 15:56:37 +01:00
Nicolas Berthier
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
Nicolas Berthier
c86d7af0b1 Introducing a hack to normalize comparison of tuples in Heptagon. 2014-12-15 15:42:37 +01:00
Nicolas Berthier
045e624f94 Bug fix with controllable-less contracts in ControllableNbac exporter. 2014-12-02 10:20:15 +01:00
Gwenaël Delaval
2a0927bd98 Bug correction in maybe_ctrln_pass 2014-12-01 14:44:08 +01:00
Nicolas Berthier
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
Nicolas Berthier
d4fe017864 Bug correction in names of C functions for converting constructors to string. 2014-10-31 15:40:05 +01:00
Nicolas Berthier
2d00f0a91c Fix sink state variable generation in Controllable-Nbac export. 2014-10-31 14:42:37 +01:00
Nicolas Berthier
0afdb16c57 Requalify enumeration types only when exporintg to Controllable-Nbac. 2014-10-31 14:16:05 +01:00
Nicolas Berthier
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
Nicolas Berthier
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
Nicolas Berthier
d84ae09cab Bug fix (preprocessor variable). 2014-10-23 11:23:36 +02:00
Nicolas Berthier
8551a91a05 Fix configure script for optional compilation of `ctrl2ept'. 2014-10-23 11:06:32 +02:00
Nicolas Berthier
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
Nicolas Berthier
541dd83fca Optional compilation of Controllable-Nbac-related modules and tools. 2014-10-21 15:41:40 +02:00
Nicolas Berthier
3b27de8146 Configure script now checks for `reatk.ctrlnbac' package. 2014-10-21 13:43:30 +02:00
Nicolas Berthier
5506690de5 Merge branch 'decade' into ctrl-n 2014-10-03 10:58:41 +02:00
Nicolas Berthier
9a29c6fa4b Upgrading to new ReaTK API (>= 0.9.4). 2014-10-03 10:57:23 +02:00
Valentin Perrelle
1f2e084e6e Fixed a bug where loops were not generated for copying arrays. 2014-06-25 18:53:34 +02:00
Nicolas Berthier
99ab12aa13 Fixed warnings. 2014-03-18 11:01:56 +01:00
Nicolas Berthier
c3c7a331b6 Using ReaTK's Controllable-Nbac backend library. 2014-03-18 10:58:57 +01:00
Nicolas Berthier
850e8522dd Merge branch 'decade' into ctrl-n 2014-03-03 16:46:21 +01:00
Gwenaël Delaval
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
Gwenaël Delaval
8650ac5695 Version 1.00.06 2014-02-21 18:12:07 +01:00
Gwenaël Delaval
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
Gwenaël Delaval
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
Gwenaël Delaval
9c4b3f3267 Version 1.00.05 2014-01-28 16:31:16 +01:00
Gwenaël Delaval
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
1a373b84eb Added some tests 
Tests from image_filters
Examples of array iterators used
 2014-01-15 00:07:29 +01:00
Gwenaël Delaval
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
 2014-01-14 23:09:22 +01:00
Nicolas Berthier
4f7413282e Merge branch 'decade' into ctrl-n 2013-11-26 18:03:54 +01:00
Nicolas Berthier
c132b53732 Handle `when' operators in general expressions, in Controllable-Nbac backend. 
- CtrlNbacGen: ignore sub-sampling in general expressions.
 2013-11-26 18:03:07 +01:00
Nicolas Berthier
934c9f9a85 Handle `when' operators for non-Boolean expressions in Controllable-Nbac backend. 2013-11-20 12:13:01 +01:00
Gwenaël Delaval
d27db41485 Version 1.00.03 2013-11-20 10:20:35 +01:00
Nicolas Berthier
808b9772f3 Merge branch 'decade' into ctrl-n 2013-11-20 08:53:00 +01:00
Gwenaël Delaval
71497a82b2 Corrected bug in inline_extvalues 
Inline_extvalues: added local variables of contracts into environments
 2013-11-19 20:39:01 +01:00
Nicolas Berthier
ae6a3aac2e Attractivity property of Controllable-Nbac output; minor refactorings. 2013-11-13 15:35:15 +01:00
Nicolas Berthier
216550c0d1 Fixed warnings & documentation comments. 
- gitignore: ignore files generated by `configure' script.
 2013-11-08 18:51:06 +01:00
Nicolas Berthier
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.
 2013-11-08 15:50:36 +01:00
Nicolas Berthier
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.
 2013-11-08 15:13:39 +01:00