Presentation
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 [1]. It is thus able to deal with any combination of logical operators and linear constraints.
More information can be found in The Lutin Tutorial (pdf version) and in The Lutin Manual.
The gitlab project hosting the lutin v6 sources is accessible from: https://gricad-gitlab.univ-grenoble...
Argosim and Stimulus
Lutin is currently being transfered by the Argosim start-up compagny. Their Lutin is named Stimulus.
Install
cf the Lustre V6 toolbox install section
Misc
— Lutin programs can be used with rdbg
— A paper describing the Lutin semantics [2]
— Two papers illustrating the use of Lutin [3],
[4]
