Lutin: modeling stochastic reactive systems
Module Lucky
type solution = Var.env_out * Var.env_loc

A solution (of a lucky step) is made of an instanciation of each controlleable (i.e., local and output) variables of the current set of lucky automata.

type step_mode =
| StepInside
| StepEdges
| StepVertices

To indicate whether the point used to perform the step is drawn inside, at edges, or at vertices of the convex hull of solutions; the step mode is used iff at least one controllable variable is numeric.

val env_step : step_mode -> Var.env_in -> Prog.state ref -> FGen.t list -> solution

env_step step_mode input state performs a step and returns the new automaton state as well as an instanciation of each controllable variables.

Raises FGen.NoMoreFormula when no more step can be done

val env_try : Thickness.t -> Var.env_in -> Prog.state -> FGen.t list -> FGen.t list * solution list

env_try thickness input state does basically the same things as env_step, except that it does not return any state, and that it returns several solutions. The number of returned solutions depends on the test thickness (cf the Thickness module).

Raises FGen.NoMoreFormula when no more try can be done