Commit graph

1135 commits

Author SHA1 Message Date
Gwenaël Delaval
63e090633c Corrected bug in causality analysis
The following node was accepted by the causality analysis:

node m(x:int) = (y,z:int)
let
    automaton
    state A
    do
      y = x + z;
      z = x + 1;
    until x = 3 then B
    state B
    do
      y = x + 3;
      z = y * x;
    until x = 10 then A
    end
tel

Each state is indeed causal, but once the automaton is translated to equations
(which is the systematic way in the current version), the node is not
schedulable.

Correction: all "Or" of dependency constraints translated to "And".

This constraint could be relaxed if code generation is done from Heptagon code,
before translation to minils equations.
2017-05-23 10:56:50 +02:00
Gwenaël Delaval
cc666cb32c Bug correction in init analysis
Correction: nodes instances must have well initialized inputs.
2017-03-17 15:18:31 +01:00
Gwenaël Delaval
faf707db4a Added test for bug [#14076] (initialization analysis)
Bug [#14076]:
node sum(x:int) returns (y:int) let y = x + (0 fby y); tel
node main(x : int) returns (y : int)
let
y = 0 -> sum(pre x);
tel

is accepted whereas the node "sum" will memorize an absent value (pre x)
and use it at next instant.

Removed auto2.ept (duplicate of auto.ept)
2017-03-17 15:15:27 +01:00
Gwenaël Delaval
7f9b72755a Correction of compile_sdc_run test script
Pointing HETPLIB to ../../lib for correct execution of heptc
and ctrl2ept with local Heptagon library.
2017-03-17 12:06:57 +01:00
Gwenaël Delaval
5440bb3129 Logico-numerical DCS example 2017-03-16 11:59:47 +01:00
Gwenaël Delaval
f284ff2872 Reachability example
Reachability example: use of reax to chech reachability of states.
2017-03-16 11:59:02 +01:00
Gwenaël Delaval
15238eaf8b Correction of DCS tests
- contrenum.ept includes contracts and controllable variable: moved to sdc test directory
- lnum_simple.ept: added "enforce true" contract (at least one objective in the syntax)
- script compile_sdc_run: heptc options to point to local Heptagon library
2017-03-16 11:56:43 +01:00
Gwenaël Delaval
e4f51fea68 Switch to non-deprecated String functions
Use of String.*_ascii non-deprecated versions.

NB: Heptagon becomes available only for Ocaml versions >= 4.03.0.
2017-03-14 12:24:29 +01:00
Gwenaël Delaval
d2dfed5019 Correction of shift/reduce conflict in syntax
Correction: in a contract, the list of objectives cannot be empty.
2017-03-14 12:14:19 +01:00
Gwenaël Delaval
0515cf4f80 Handling of implication operator in Ctrln back-end 2017-03-13 18:01:05 +01:00
Gwenaël Delaval
b0d719dcf2 Added SDC tests 2017-03-05 23:55:07 +01:00
Gwenaël Delaval
3a8a3e1ff9 Modification of compile_sdc_run test script
Test script compile_sdc_run: handling of different controller
synthesis algorithms.
In a test file, put a special comment :
(* SDC algorithm *)
on a single line, to activate synthesis algorithm "algorithm"
for this test file.

Examples:
(* SDC sB *)
(* SDC sS *)
(* SDC sS:d={P:D} *)

NB: assertions not yet handled.
2017-03-05 23:50:39 +01:00
Gwenaël Delaval
6c3caec234 Bug correction in ctrl2ept: no systematic conversion from int to float 2017-03-04 01:53:32 +01:00
Gwenaël Delaval
2f18926bf4 Clean up documentation comments 2017-03-03 11:41:57 +01:00
Gwenaël Delaval
2e107cd872 Suppress "c_" prefix in Ctrl-Nbac generation 2017-02-23 02:45:04 +01:00
Gwenaël Delaval
5b215f832b Version 1.03.02 2017-02-08 21:36:04 +01:00
Gwenaël Delaval
9456322f8c Added sdc tests in CTestTestfile.cmake 2017-02-06 18:02:31 +01:00
Gwenaël Delaval
cffb195b6d Compile/sdc/run test script 2017-02-06 18:02:05 +01:00
Gwenaël Delaval
03c64bd519 Updated test modular.ept 2017-02-06 18:01:20 +01:00
Gwenaël Delaval
7bc5e4c115 Examples with contracts and sdc for tests 2017-02-06 15:32:44 +01:00
Gwenaël Delaval
ace152e096 Test script for controller synthesis
Added compile_sdc_run script which runs bzreax (compiles and run controller
synthesis tool reax) on heptagon programs.
2017-02-06 15:30:52 +01:00
Gwenaël Delaval
7392680a5f Heptagon webpage update
Publications page: HAL Heptagon collection
2016-07-02 22:51:30 +02:00
Gwenaël Delaval
a0e97b82ea CtrlNbac backend: systematic sink state, outputs as local variables
Changes in CtrlNbac back-end :
- systematic sink state, only in ctrln code
- sink state "ok" removed (useless as was coded)
- no sink state in minils code
- outputs in ctrln are local variables, no longer state variables
2016-06-25 08:40:50 +02:00
Gwenaël Delaval
69b8cc5a18 Added operator (=>) in Pervasives module
Operator (=>) for implication added in Pervasives module.

"a => b" is translated into "not a or b" at code generation.
2016-06-25 08:37:47 +02:00
Gwenaël Delaval
5e277fcc8a Version 1.03.01 2016-06-02 01:59:51 +02:00
Gwenaël Delaval
f34031dbda Correct link for webpage 2016-06-02 01:33:02 +02:00
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