lutin

Lutin: modeling stochastic reactive systems
IN THIS PACKAGE
Module Constraint
type ineq =
| GZ of Ne.t(*

expr > 0

*)
| GeqZ of Ne.t(*

expr >= 0

*)

Normalised linear constraints.

type t =
| Bv of Exp.var(*

booleans

*)
| EqZ of Ne.t(*

expr = 0

*)
| Ineq of ineq(*

> or >=

*)
val dimension : t -> int

Returns the number of variables involved in the constraint

val dimension_ineq : ineq -> int
val get_vars : t -> string list

returns the vars appearing in a constraint

val get_vars_ineq : ineq -> string list
val apply_subst : Ne.subst -> t -> t

apply_subst cstr s applies s to cstr. Note that the result could have been multiplied by a constant.

val apply_subst_ineq : Ne.subst -> ineq -> ineq
val apply_substl : Ne.subst list -> t -> t
val apply_substl_ineq : Ne.subst list -> ineq -> ineq
val neg_ineq : ineq -> ineq

neg_ineq cstr returns the negation of an inequality constraint.

val opp_ineq : ineq -> ineq

neg_ineq cstr returns cstr where its Ne.t is replaces by its opposite.

val to_string : t -> string

Pretty printing.

val to_string_verbose : t -> string
val print : t -> unit
val ineq_to_string : ineq -> string
val print_ineq : ineq -> unit
val eval_ineq : Var.num_subst list -> ineq -> bool