Commit graph

1144 commits

Author SHA1 Message Date
Gwenaël Delaval
4274b21733 Version 1.03.04 2017-05-24 01:19:55 +02:00
Gwenaël Delaval
b942f456ed "Last" pass bug correction 2017-05-23 23:30:11 +02:00
Gwenaël Delaval
35bce1d5e8 Added simple scheduler with -simple-scheduler option
Scheduler_simple module: simplest possible scheduler, with
only topological sort and without any "smart" algo/heuristic.
2017-05-23 22:16:57 +02:00
Gwenaël Delaval
7d6106d0aa Passes optimization
Translation to tail-recursive versions of functions
for handling of (very) big nodes.
2017-05-23 22:13:32 +02:00
Gwenaël Delaval
b9870eefc0 Debug mode in _tags.in 2017-05-23 22:12:27 +02:00
Gwenaël Delaval
db5524df3f Tests addition 2017-05-23 22:10:39 +02:00
Gwenaël Delaval
e4b0578b38 User manual update 2017-05-23 22:04:46 +02:00
Gwenaël Delaval
1ead8a98ea Correction of unary minus priority
To fix: see test minus_pre.ept:

node main() = (o,p:int)
let
  o = ~-1 -> pre o + 1;
  p = -1 fby p + 1
tel
2017-05-23 22:01:05 +02:00
Gwenaël Delaval
028c564a31 Clean-up of verbose output
Leave only comments about compilation passes.
Remove output of intermediate code on standard output: added
generation of <module>.log containing all intermediate code.
2017-05-23 11:37:30 +02:00
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