Commit graph

1109 commits

Author SHA1 Message Date
Gwenaël Delaval
83905f9039 Remove traces and warnings 2016-06-02 01:33:02 +02:00
Gwenaël Delaval
d8d24ffd95 Handle modularity/several controllers by module
* Several controllers by module : added option "-m <Module>" in ctrl2ept

Generate controllers for each node of one module in <module>_controller.ept

* Types of <Module> no longer moved to <Module>_controller

* Added "_types" suffix for type dependencies for C target
2016-06-02 01:33:02 +02:00
Gwenaël Delaval
05150f2078 [ctrl-n] Suppression of type declarations in Heptagon controller
TODO : move type declarations in separated module.
2016-06-02 01:33:02 +02:00
Timothy Bourke
0b7eba8458 Add error for non-stateful decls. in pervasives
Attempts to compile a pervasives.epi containing functions with multiple
outputs or nodes now fail with an informative error message.

* The following files demonstrate the problem:

  pervasives.epi:
    type bool = true | false
    external val node test(bool;bool) returns bool

  broken.ept:
    node broken() returns (y : bool)
    let
      y = test(false, false);
    tel

  Running:
    heptc -nopervasives pervasives.epi
    heptc -stdlib . -target c broken.ept

  Fails with:

    ---------
    Internal compiler error
    Passe : Static evaluation failed of the pervasive operator test
    ----------
    Fatal error: exception Misc.Assert_false

* A different error occurs for nodes that return multiple outputs:

  pervasives.epi:
    type bool = true | false
    external val node test(bool;bool) returns (bool;bool)

  broken.ept:
    node broken() returns (y : bool)
    var l1 : bool;
    let
      (y,l1) = test(false, false);
    tel

  Running:
    heptc -nopervasives pervasives.epi
    heptc -stdlib . broken.ept

  Gives:
    Inconsistent clock annotation for exp test(false, false).
    File "broken.ept", line 4, characters 11-29:
    >  (y,l1) = test(false, false);
    >           ^^^^^^^^^^^^^^^^^^
    Clock Clash: this expression has clock 'a3,
    but is expected to have clock ('a4 * 'a5).

  The name "test" is parsed as an Eextvalue (rather than an Eapp), and there
  is an implicit assumption in compiler/minils/analysis/clocking.ml that such
  values have a simple clock.
2016-04-26 16:34:26 +02:00
Nicolas Berthier
755b570a96 Correct typing of numericals when translating Controllable-Nbac nodes
Without this change one could end up with inconsistent numerical types
when expressions like 1 + xx /. 3.0 >= 0 (with xx being a float), that
is correctly handled in ReaTK's frontend, are translated into the
heptagon's internal representation.
2016-03-30 17:35:56 +01:00
Gwenaël Delaval
20d9ff7184 Updated heptagon manual for web 2016-02-16 17:58:41 +01:00
Gwenaël Delaval
73a3762895 Manual: control structures (present, reset) 2016-02-16 17:18:17 +01:00
Gwenaël Delaval
4f0ef44ebd Version 1.03.00 2016-01-18 17:43:25 +01:00
Gwenaël Delaval
e9540a2159 hepts: enum types & alias
The graphical simulator hepts now support type aliasing.
2016-01-18 17:24:51 +01:00
Gwenaël Delaval
2aed0f6537 Deadcode removal improvement
Deadcode removal in Obc :
- suppression of switch unused cases :

switch(true) {
  case false: ...
}

- activation with -deadcode option
2016-01-18 14:32:54 +01:00
Gwenaël Delaval
64b8c0592a Pretty-printing class parameters in obc 2016-01-18 14:31:04 +01:00
Gwenaël Delaval
19911506de Removal of warnings 2016-01-18 14:30:20 +01:00
Gwenaël Delaval
e8ec3e012c Merge branch 'ctrl-n' into decade 2015-12-15 09:33:25 +01:00
Gwenaël Delaval
4552f62872 Version 1.02.00 2015-12-13 22:38:24 +01:00
Gwenaël Delaval
2c1717e99f Removal of -custom option for compilation
-custom option trigger bugs with opam
2015-12-11 17:00:29 +01:00
Gwenaël Delaval
2777753b7e Cleanup : removal of useless files 2015-12-11 16:58:26 +01:00
Nicolas Berthier
65908e7ca3 New configure script options to enable/disable byte/native targets 2015-09-21 18:53:52 +02:00
Nicolas Berthier
fb6755efb2 Bugfix in ctrl2ept: do not reset symbol table after loading type declarations 2015-09-21 15:17:30 +02:00
Nicolas Berthier
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
Nicolas Berthier
2d874f8070 New option to silence warnings about untranslatable constructs 2015-09-18 13:59:33 +02:00
Nicolas Berthier
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
Gwenaël Delaval
bb324eee17 Update of Makefile-distrib for heptreax manual inclusion 2015-09-17 17:22:46 +02:00
Gwenaël Delaval
0a65ffc8e2 Update of example Extern_C 2015-09-17 17:20:31 +02:00
Gwenaël Delaval
3b81368074 CHANGES for version 1.01.00 2015-09-17 16:58:41 +02:00
Gwenaël Delaval
8dbb283310 User manual for Heptagon+ReaX 2015-09-17 16:54:10 +02:00
Gwenaël Delaval
015875b279 Math module
The Math module contains mathematic functions.
2015-09-17 16:51:24 +02:00
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
Adrien Guatto
dc47767ba4 Print an empty default statement at the end of all C switches
This prevents modern compilers from emitting warnings when the generated C code
contains switch statements with (intentionally) missing cases.
2015-06-12 17:49:59 +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