Commit graph

1169 commits

Author SHA1 Message Date
Gwenaël Delaval
d2234e64d8 Merge branch 'fix_heptc_script' into 'master'
Remove broken Python bit from heptc script

See merge request gdelaval/heptagon!2
2018-10-30 10:13:53 +01:00
Adrien Guatto
99460e24e5 Remove broken Python bit from heptc script 2018-10-12 16:05:09 +02:00
Gwenaël Delaval
e0d1900f3a Version 1.05.00
- Option -simple-scheduler active for scheduling post-ctrln code generation
 - Handle implication operator in Sigali backend
 - Compatibility with reatk >= 0.14
2018-06-19 22:07:03 +02:00
Gwenaël Delaval
b51c292231 Allow use of simple scheduler after control synthesis code generation
The -simple-scheduler option now imply the use of simple scheduler
both before and after control synthesis code generation.
2018-06-07 11:57:51 +02:00
Nicolas Berthier
7abe92dc0d Adapt to new interface of reatk.ctrlNbac (≥ 0.14) 2018-06-06 14:45:50 +01:00
Nicolas Berthier
8872bb3998 Do not remove sub-directories in `Compiler_utils.clean_dir' 2018-03-02 14:27:15 +00:00
Nicolas Berthier
95bb1a72ad Handle implication operator in Sigali backend 2018-03-02 14:26:10 +00:00
Gwenaël Delaval
95c9eb699b Version 1.04.00 2017-09-29 14:58:37 +02:00
Gwenaël Delaval
24469c9ae1 Update .gitignore 2017-09-29 00:08:42 +02:00
Timothy Bourke
63289fe9f6 Allow semicolons after tel's 2017-09-29 00:08:42 +02:00
Timothy Bourke
fa4aaee865 Typedef for real in C target 2017-09-29 00:08:42 +02:00
Timothy Bourke
94badc5f01 Add an abbreviation for the 'real' type 2017-09-29 00:08:42 +02:00
Timothy Bourke
0747494c7a Fix line counting. Ignore kind2 property comments 2017-09-29 00:08:42 +02:00
Timothy Bourke
abfc038b6b Accept single line "--" comments 2017-09-29 00:08:42 +02:00
Timothy Bourke
2d9fb52bec Fix a mistake in new when patterns 2017-09-29 00:08:42 +02:00
Timothy Bourke
4dadf6b4d6 Enforce well-formedness of clocks
For a clock (ck on x) to be well-formed in an environment H, we must
have H x = ck, i.e., the clock of x is the same as the clock ck of the
stream being sampled.

This constraint is guaranteed by construction for fully inferred clocks
(by the rules for when and merge), but nothing guarantees that user
declarations be well-formed. This can lead to problems.

For instance, this invalid program is incorrectly accepted:

    node f (x : bool; a : bool :: . on b;
		      b : bool :: . on a) returns (y:bool);
    let
	y = true;
    tel

as is this one:

    node f(a: bool :: . on a; b: bool :: . on a)
    returns (z: bool);
    var w : bool;
    let
	w = a when b;
	z = false fby w;
    tel

This invalid program is incorrectly accepted and leads to an internal
compiler error:

    node f (x : bool) returns (y:bool);
    var a : bool :: . on b;
	b : bool :: . on a;
    let
	y = true;
	a = true;
	b = true;
    tel

This patch enforces the well-formedness constraint. It gives a sensible
error message when the constraint cannot be satisfied.
2017-09-29 00:08:42 +02:00
Timothy Bourke
cae38d0e60 Accept when-syntax for declaring clocks
The parameter or local declaration:
    x : bool :: . on y

Can now be made using the 'standard' Lustre syntax:
    x : bool when y

In this case, the translation gives x the clock:
    'a on y

and relies on the (MiniLS) Clocking pass to instantiate the fresh clock
variables.
2017-09-29 00:08:42 +02:00
Timothy Bourke
0ef0ac5529 Allow "and" as a synonym for "&" 2017-09-29 00:08:42 +02:00
Timothy Bourke
3d75602a0d Accept "e when not x" for "e whenot x" 2017-09-29 00:08:42 +02:00
Timothy Bourke
9de1a96843 Allow (optional) semicolon after returns clause 2017-09-29 00:08:42 +02:00
Timothy Bourke
685c3aa862 Accept .lus file extension 2017-09-29 00:08:42 +02:00
Timothy Bourke
66da5f4b5c Minor fix to Merlin improvements. 2017-09-29 00:08:42 +02:00
Timothy Bourke
f8afddd0d9 Work better with merlin 2017-09-29 00:08:42 +02:00
Nicolas Berthier
100c08ee36 Bug correction in normalization of merge: fix propagation of type annotations
Minils.CtrlNbacGen relies on such type annotations to generat
Controllable-Nbac nodes.  This fix allows the use of ReaX to enforce
contracts of nodes involving merge operations on tuples over multiple
data types, such as:

  (a, b) = merge c
           (true -> ((true when c), (0 when c)))
           (false -> ((false whenot c), (2 whenot c)));

This kind of code previously led to erroneous Controllable-Nbac code.
2017-09-21 16:29:06 +01:00
Nicolas Berthier
15b2c09425 Adapt to new interface of reatk.ctrlNbac (≥ 0.11) 2017-09-20 16:47:17 +01:00
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