lutin

Lutin: modeling stochastic reactive systems
IN THIS PACKAGE
Module Polyhedron
type range =
| RangeI of Num.num * Num.num
| RangeF of float * float

Convex range

val build_poly_list_from_delayed_cstr : int -> range Util.StringMap.t -> Constraint.ineq list -> range Util.StringMap.t * Var.name list * (Var.vnt list * Poly.t * ( int -> string ) * Constraint.ineq list) list

build_poly_list_from_delayed_cstr verb tbl cl puts the constraint cl in several polyhedra (one polyhedra per group of constraints holding on disjunct set of variables), taking into account constraints already made on vars (which can be found in tbl).

Also returns the list of variables involved in cl as well as a new tbl where the delayed constraints have been removed from the range based store.

type point = float list
val get_vertices : Poly.t -> ( int -> string ) -> point list
val point_to_subst_list : Var.vnt list -> ( int -> string ) -> point -> Var.num_subst list

Transform a point into a list of substitutions, performing the necessary conversion (which are wrong from float to integers !).

val point_is_in_poly : Var.vnt list -> point -> ( int -> string ) -> Constraint.ineq list -> bool