lutin

Lutin: modeling stochastic reactive systems
Library lutin
Module Gne
type t
val add : t -> t -> t

Respectively adds, substracts, multiplies, divides, and computes the modulo, the opposite of garded normal expressions.

val diff : t -> t -> t
val mult : t -> t -> t
val modulo : t -> t -> t
val div : t -> t -> t
val opposite : t -> t
val quot : t -> t -> t
val empty : unit -> t

empty () returns an empty gne.t

val make : Ne.t -> bool -> t

make ne bdd b returns the gne containing the expr ne guarded by (bdd_true, b).

val of_ite : Bdd.t -> bool -> t -> t -> t

of_ite cond flag gne_then gne_else

val fold : ( Ne.t -> (Bdd.t * bool) -> 'acc -> 'acc ) -> t -> 'acc -> 'acc

fold f gne applies f to every expr in gne.

val get_constant : t -> Value.num option

get_constant gne returns an Value.num iff gne is equal to the degenerated garded normal expression [(i, true)]. This function is useful to get dynamic weigths and default values.

val to_string : t -> string

Pretty-printing

val dump : t -> unit