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