|
| | | Download |
The different executables (see below) can be found here (includes documentation).
| Name | Integer arithmetic in Polyhedra | Coments |
| nbaci.opt | 32 bits machine integer | the fastest, but easy (and undetected) overflows |
| nbacl.opt | 64 bits machine integer | better, but (undetected) overflows can still occur |
| nbacg.opt | multiprecision GMP integer | robust, but slower |
The most frequent sign that an overflow has occured is an infinite loop inside the polyhedra library NewPolka.
We describe the toolchain to convert Lustre programs equipped with property observers to NBac files.
The tools coming from the Lustre language compilation toolchain are distributed with the kind permission of Nicolas Halbwachs and Pascal Raymond, members of the synchronous team of VERIMAG.
Executables are available here (only for Linux computers on Intel processors, but ask for something else).
The following files are required:
| Name | Description |
| lus2nbac | main shell script which generate a NBac program from a Lustre program and the name of a safety property observer contained in the program. A safety observer is a Lustre node returning a single Boolean output. A false value of this output at any point during the execution means that the property has been violated. See the litterature about synchronous programming available at the above-mentioned WEB page. Example: (see directory example): lus2nbac ascenseur.lus Prop1 |
| pollux | front-end of the Lustre compiler |
| lus2ec | shell script using pollux. Convert a Lustre file to EC format (flattened and sliced Lustre program). |
| ec2nbac | Converting from EC format to NBac format |
See here for an overview of the tools and how to use it.
Executables are available here only for Linux computers on Intel processors (but ask for something else).
| Name | Description |
| autoc2auto | For building a product of automata and generating a single automaton in AUTO format. The product can be controlled to be partially explicit, partially implicit (ie, encoded in variables). |
| auto2nbac | For translating an automaton in AUTO format into a texscNBac specification. The explicit control structure if the automaton is preserved. |
| nbac2auto | For annotating an initial AUTO specification with the information computed by NBAC. This produces a new annotated AUTO file. |
| auto2dot | For conversion to DOT |
|
| | | Download |