Overview

Lustre compiler toolset.

lustrec is structured around the modular compilation scheme proposed by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08.
It is an open source lustre compiler that provides verification capabilities.
It is currently mainly used through the CocoSim platform, a Matlab toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre language is used as an intermediate representation and relies mainly on lustrec to produce code or verification artifacts.

LustreC is in active development: a few developper with a few time to make progress, so it is highly unstable!
The master branch is rarely updated, so please consider using the unstable one.

The current development and addition of features is spread among too many branches. We are currently trying to clean up the mess.

LustreC toolset provides multiple binaries:

lustre compiler lustrec producing C code in a modular way. It also produces Horn clauses encoding of the provided Lustre models.
lustre test generator: lustret
lustre importer: lustrei
lustre stateflow: lustresf
lustre verifier: lustrev

These binaries are more or less usable. The main one being lustrec, used by CocoSim to produce code and perform model-checking.
Lustret is also rather stable and produces covering criteria for test generation, as well as the production of mutants files.

Source can be access through git:
git clone --depth 1 https://cavale.enseeiht.fr/git/lustrec

Since the code is quite old (it started in 2012) and has lived through multiple repositories, we recommand using the depth 1 option to obtain the last commit rather than all the history.

Let us know if you need any help with it. We would be happy to hear about you.

Pierre-Loïc for the lustrec team