lustre
lus2ec, ecexe, luciole, simec, lus2oc, ec2oc, ocmin, lus2atg, oc2atg, ec2c, poc, lux, lesar, ecverif, xlesar - lustre v4 tools
The front-end for Lustre-V4 tools is the pre-processor lus2ec
This compiler transforms a Lustre-V4 program (.lus file, with modularity, arrays, recursion) into a Lustre-expended-code program (.ec file, with a single node, no arrays, no recursion).
All other tools (compilers, simulators ...) are actually running on the .ec format, but the distribution provides (in general) shell scripts combining the front-end (lus2ec) with the various back-ends (compilers and simulators).
The Lustre-V4 distribution provides simulation tools that interpret ec code. They only run on basic programs, that do not require external types, constants or functions; however, some classical functions are supported, corresponding to the math C library. All those tools are based on the same interpreter, and only differ on the user interface:
ecexe is a unix-filter like tool, reading on standard input and writing to standard output.
xecexe (script xsimlus) provides a graphical interface to the ec interpreter; this tool, based on X-intrinsics and Athena widgets is quite old and no longer maintained.
simec (script luciole) provides a more friendly interface, based on tcl-tk widgets. Moreover, it allows the user to (slightly) customize the graphical interfaces.
Originally, the lustre compiler was designed to use an intermediate format, called oc (for object code). This format was initiated by a collaboration with the Esterel team, and several releases where defined. The main characteristic of this format is that the control structure consists of a finite state automaton. The tool ec2oc (script lus2ec or lustre) supports oc version 2 ( oc2) and 5 (oc5). It also provides lot of options that allow the user to choose the automaton stucture of the generated code.
Some tools based on the oc format are provided by the Esterel team, in particular C and Ada code generators (occ, ocada). An alternative Ansi-C code generator, poc, is provided within the lustre distribution.
The distribution also provides a tool that performs minimization of oc automata (ocmin) and a translator to the autograph format (oc2atg).
The low-level target format in Lustre-V4 is Ansi-C. This code can be obtained either:
via ec2oc, using the poc compiler,
directly from the ec code, using the compiler ec2c.
Note that the code generated by ec2c is different from the one generated by ec2oc; in particular ec2c does not build any kind of automaton. On the contrary the generated interface is the same for both compiler, so one can (normally) easily swap between code generated by poc and code generated by ec2c.
By default, those compilers only provide a transition function, and the user has to write his (her) own input/output and main procedures. Moreover, the user has to provide the implementation of all external objects (types, constants and functions) declared in the Lustre source.
Nevertheless, both poc and ec2c have an option -loop that builds an additional main procedure. This simple "loop" works as a unix filter (just like ecexe). In order to obtain an executable, this main program may be completed by the implementation of the (possible) external objects. Anyway, it can be used as a pattern for more complex application.
If the code does not require external objects, the main generated by the -loop option can be linked "as it is" with the transition function, in order to build a stand-alone application. This is the case for almost all programs that can be simulated using ecexe; by the way, the execution of such a stand-alone program is completly similar to a simulation with ecexe: standard input to standard output, interactive when called form a terminal.
The script lux is the best way for quickly building a stand-alone application: it can take either lus, ec or oc files as input, and uses the most suitable compilers calls and build, if possible, a sstand-alone application. Note that C compilation and the link-editing are performed by the host Ansi-C compiler; by default, lux calls the GNU C compiler gcc, but one may customize this script.
The Lustre model-checker is ecverif (shell lesar). It provides several algorithms to check the validity of safety properties on Lustre programs. lesar (resp. ecverif) takes as input special lustre (resp. ec) programs, called verification programs. Roughly speaking, such a program must be the parallel product of a program to validate, a program observing that the desired property is satisfied, and another one observing that the hypothesis on the environment are satisfied. The user may build this product himself, and at last, lesar only checks that its input has a single Boolean output, wich is supposed to be the property to check; the hypothesis are supposed to be the conjunction of all the assertions appearing in the verification program.
xlesar is a graphical interface to lesar/ecverif. This tool is particularly suitable for managing a set of verifications on the same Lustre programs.