Lutin: modeling stochastic reactive systems
Module Store
type t = {
var : vars_domain;
substl : Ne.subst list;
delay : Constraint.ineq list;
untouched : Exp.var list;
and vars_domain =
| Unsat of Constraint.t * t
| Range of range_store
val create : Exp.var list -> t

Store.create varl returns an initial store (the universe) for the variable contained in varl.

val add_constraint : t -> Formula_to_bdd.t -> Constraint.t -> t

add_constraint s c returns the store s with the numeric constraint c added.

val is_store_satisfiable : int -> t -> bool

Returns false iff one of the variable domain is empty.

type p = (Var.vnt list * Poly.t * ( int -> string ) * Constraint.ineq list) list

Convex Polyhedron.

type t' = {
range : range_store;
substl' : Ne.subst list;
untouched' : Exp.var list;

contains basically the same info as t with a few fields removed

exception No_polyedral_solution

Raised by the 2 functions below

val switch_to_polyhedron_representation : int -> t -> t' * p

switch_to_polyhedron_representation store is called when all the constraints have been handled, and returns a range-based and a list of polyhedra (cf the algorithm above).

Raises No_polyedral_solution if that conversion fails