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.
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.
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.
Leave only comments about compilation passes.
Remove output of intermediate code on standard output: added
generation of <module>.log containing all intermediate code.
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.
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)
- 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
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.
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
* 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
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.
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.
