### 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.

### Argosim and Stimulus

Lutin is currently being transfered by the Argosim start-up compagny. Their Lutin is named Stimulus.

### Install

Lutin is availlable via opam

` opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"`

opam update

opam install lutin

### Misc

— A paper describing the Lutin semantics [2]

— Two papers illustrating the use of Lutin [3],
[4]