lutin

Lutin: modeling stochastic reactive systems
IN THIS PACKAGE
Module Prog
type atomic_ctrl_state = string
type ctrl_state = atomic_ctrl_state list
type dyn_weight =
| V of int
| Infin

Weigths, once evaluated (no more memories nor inputs)

type wt = children Util.StringMap.t * string

A wt (weigthed tree) is a n-ary tree encoding the set of possible formula for the next step.

and children =
| Children of (dyn_weight * string) list
| Leave of Exp.formula * atomic_ctrl_state
| Stop of string
type t = {
initial_ctrl_state : ctrl_state list;
in_vars : Exp.var list;
out_vars : Exp.var list;
loc_vars : Exp.var list;
ext_func_tbl : Exp.ext_func_tbl;
memories_names : (string * Exp.var) list;
bool_vars_to_gen : Exp.var list list;
num_vars_to_gen : Exp.var list list;
output_var_names : Var.name list list;
reactive : bool;
get_wtl : Var.env_in -> state -> ctrl_state -> wt list;
is_final : ctrl_state list -> bool;
gen_dot : ctrl_state list -> ctrl_state list -> string -> int;
}

The Digested Lucky program (form the static part of the state). Holds a list of independant programs (i.e., they don't share any I/O).

and dynamic_state_fields = {
memory : Var.env;
ctrl_state : ctrl_state list;
last_input : Var.env;
last_output : Var.env;
last_local : Var.env;
snt : Solver.t;
verbose : int;
}

The dynamic part of the state (that changes at each cycle).

and state = {
d : dynamic_state_fields;
s : t;
}
val memory_of_state : state -> Var.env
val last_values_of_state : state -> Var.env * Var.env * Var.env
val compute_weight : Exp.weight -> Var.env_in -> state -> dyn_weight
val print_wt : wt -> unit

Pretty-printing

val ctrl_state_to_string : ctrl_state -> string
val ctrl_state_list_to_string_list : ctrl_state -> string list
val ctrl_state_to_string_long : ctrl_state list -> string

Used for printing information about the current control point in error messages.