lutin

Lutin: modeling stochastic reactive systems
IN THIS PACKAGE
Module LutExe
type t
val make : MainArg.t -> string list -> string -> t
val in_var_list : t -> Exp.var list
val out_var_list : t -> Exp.var list
val loc_var_list : t -> Exp.var list
type control_state
type data_state = {
ins : Value.OfIdent.t;
outs : Value.OfIdent.t;
mems : Value.OfIdent.t;
}
type guard
val guard_to_string : guard -> string
type behavior =
| Goto of guard * control_state
| Raise of string
| Vanish
type behavior_gen =
| NoMoreBehavior of int
| SomeBehavior of behavior * unit -> behavior_gen
val get_init_state : t -> control_state
val clear : t -> t
val get_init_pres : t -> Value.OfIdent.t
val get_behavior_gen : t -> Var.env_in -> Var.env -> control_state -> unit -> t * behavior_gen
val find_some_sols : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard -> t * guard * (Var.env_out * Var.env_loc) list
val find_one_sol : t -> guard -> t * guard * (Var.env_out * Var.env_loc)
val make_pre : Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
type ctx = RdbgEvent.t
type e = RdbgEvent.t
val step_rdbg : ctx -> string -> t -> control_state -> data_state -> ( ctx -> t -> control_state -> data_state -> e ) -> e
type internal_state
val get_init_internal_state : t -> internal_state
exception Stop
exception Exception of string
val dump : t -> unit
val string_of_control_state : control_state -> string