Lutin is a language to program stochastic reactive systems. It has been designed to model environments and perform automated testing of reactive systems with Lurette.
It can be seen as a probabilistic extension of Lustre with an explicit control structure based on regular operators: sequence (fby, for "followed by"), Kleene star (loop), and choice (|). At each step, the Lutin interpreter
- computes the set of reachable constraints, which depends on the current control-state;
- removes from it unsatisfiable constraints, which depends on the current data-state (input and memories);
- draws a constraint among the satisfiable ones (control-level non-determinism);
- draws a point in the solution set of the constraint (data-level non-determinism).
This chosen point defines the output for the current reaction. The solver of the current Lutin interpreter uses Binary Decision Diagrams (BDD) and convex polyhedron libraries . It is thus able to deal with any combination of logical operators and linear constraints.
Lutin is currently being transfered by the Argosim start-up compagny. Their Lutin is named Stimulus.
Lutin is availlable via opam
opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam install lutin
If you install opam for this purpose, by default its uses the "system" ocaml, i.e., the one installed by your package manager. For some reasons (right permission issues), the previous commands might not work. If it is the case, try to install your own version of ocaml as follows:
opam switch 4.04.0