Lutin: modeling stochastic reactive systems
Module Solver
type t = Bddd.t
val init : unit -> t
val tbl_to_string : t -> string
val is_satisfiable : t -> Var.env_in -> Var.env -> int -> string -> Exp.formula -> string -> t * bool

is_satisfiable input memory verbose_level msg f suceeds iff the formula f, once evaluated w.r.t. input and memories, is satisfiable from the Boolean point of vue. At this level, each numeric constraint is view as a Boolean variable. The numeric satisfiability will be checked later, during the draw. The reason for that is that we do not want to build unnecessary polyhedra because it is very expensive.

val is_satisfiable_bdd : t -> Var.env_in -> Var.env -> int -> string -> Exp.formula -> string -> t * bool * Bdd.t
val solve_formula : t -> Var.env_in -> Var.env -> int -> string -> list list -> Thickness.formula_draw_nb -> Thickness.numeric -> Exp.formula -> Exp.var list -> Exp.formula -> t * (Var.env * Var.env) list

solve_formula input memory verbose_level msg output_var_names fdn tn bools nums f randomly assigns tn values to variables in bools and nums (which ought to contains all output and local variables occurring in the formula f). It returns a list (of length tn) of pairs, where the left hand side of the pair contains the output vars, and the right hand side contains the local vars.

The Boolean list of variables is encoded in a formula for performance reasons: solve_formula is likely to be called significantly often with the same arguments so that it is worth precomputing this encoding before.

Side effect: fills in the solution number table

val eval_int_expr : t -> Exp.num -> string -> Var.env_in -> Var.env -> int -> int option