The different executables (see below) can be found here (includes documentation).

NBac executables

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.

Translation from Lustre language to NBac format

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

Translation from AutoC/Auto 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

Bertrand Jeannet, February 10, 2011