Commit graph

399 commits

Author SHA1 Message Date
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
95bb1a72ad Handle implication operator in Sigali backend 2018-03-02 14:26:10 +00: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
Nicolas Berthier
15b2c09425 Adapt to new interface of reatk.ctrlNbac (≥ 0.11) 2017-09-20 16:47:17 +01: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
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
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
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
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
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
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
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
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
541dd83fca Optional compilation of Controllable-Nbac-related modules and tools. 2014-10-21 15:41:40 +02:00
Nicolas Berthier
9a29c6fa4b Upgrading to new ReaTK API (>= 0.9.4). 2014-10-03 10:57:23 +02:00
Nicolas Berthier
99ab12aa13 Fixed warnings. 2014-03-18 11:01:56 +01:00
Nicolas Berthier
c3c7a331b6 Using ReaTK's Controllable-Nbac backend library. 2014-03-18 10:58:57 +01:00
Nicolas Berthier
850e8522dd Merge branch 'decade' into ctrl-n 2014-03-03 16:46:21 +01:00
Gwenaël Delaval
e885f82e00 Bug correction/feature adding: abstraction within contracts
Allowing additional inputs from abstractions within contracts. Thus,
calling non-inlined subnodes is allowed, as well as operations on
non-Boolean inputs or states (in contracts).
2014-02-21 17:39:37 +01:00
Gwenaël Delaval
c61e01f19b Correct handling of comparison operators in Sigali
- bug fix: comparison between two non-constant integer expressions in Sigali
 - bug fix: correct handling of "=" and "<>" operators in Sigali
2014-01-14 23:09:22 +01:00
Nicolas Berthier
c132b53732 Handle `when' operators in general expressions, in Controllable-Nbac backend.
- CtrlNbacGen: ignore sub-sampling in general expressions.
2013-11-26 18:03:07 +01:00
Nicolas Berthier
934c9f9a85 Handle `when' operators for non-Boolean expressions in Controllable-Nbac backend. 2013-11-20 12:13:01 +01:00
Nicolas Berthier
808b9772f3 Merge branch 'decade' into ctrl-n 2013-11-20 08:53:00 +01:00
Gwenaël Delaval
71497a82b2 Corrected bug in inline_extvalues
Inline_extvalues: added local variables of contracts into environments
2013-11-19 20:39:01 +01:00
Nicolas Berthier
ae6a3aac2e Attractivity property of Controllable-Nbac output; minor refactorings. 2013-11-13 15:35:15 +01:00
Nicolas Berthier
216550c0d1 Fixed warnings & documentation comments.
- gitignore: ignore files generated by `configure' script.
2013-11-08 18:51:06 +01:00
Nicolas Berthier
10bdab4dc6 Exclusively use ocamlfind; source documentation generation.
- Stripped portions of `myocamlbuild{,_config}.ml' that seem useless
  when `-use-ocamlfind' is passed to ocamlbuild.

- Added some code in `myocamlbuild_config.ml' to be able to generate
  documentation by merging interface and implementation files.
2013-11-08 15:50:36 +01:00
Nicolas Berthier
8aeab651ce First draft for Controllable-Nbac format generation.
- CtrlNbac: new module for internal representation and output code for
  Controllable-Nbac format;

- CtrlNbacGen: translation into Controllable-Nbac of Minils nodes
  necessitating controller synthesis; the insertion of calls to
  controllers is not yet done, and the nodes are left unchanged.
2013-11-08 15:13:39 +01:00
Gwenaël Delaval
f3d34f57d1 Abstraction of integers for Sigali
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
2013-09-05 19:03:22 +02:00
Gwenaël Delaval
71f7db2d11 Bug correction in Mls_printer and Hept_printer
Correction of infix operators printing : infix printing only
when two arguments of pervasives infix operators (no assertions
on number of arguments).
2013-07-10 09:57:19 +02:00
Gwenal Delaval
f696203eb1 Bug in sigalimain
Bug correction: code generation to sigali for stateless nodes

=> stateless nodes handled like stateful nodes, if not in pervasives.
2013-07-09 21:16:30 +02:00
Gwenal Delaval
2d150a3a3d Infix operators in printers
Infix operators handled in Heptagon and Minils printers
2013-07-09 21:15:31 +02:00
Cédric Pasteur
a00620ca19 Fixed interference of fast memories
A fast memory should be considered alive during
the whole step function when its clock is false.
2013-05-06 11:47:05 +02:00
Cédric Pasteur
99dc7820c7 Avoid crash in memalloc
Check if both variables are optmized
2013-04-22 18:11:10 +02:00
Nicolas Berthier
8497bafa2e Minor but correction in sigali output.
- Translation to z3z now evaluates constant expressions instead of
  abstracting them. This non-feature could cause "false" synthesis
  failures due to non-translatable yet constant expressions possibly
  introduced by tomato (or manually), for instance `not false' in node
  `n' bellow:

    node n (a: bool) returns (ok: bool)
      contract assume true enforce ok with ()
    let
      ok = a or not false;
    tel
2013-04-11 17:30:30 +02:00