Module Condition

module Condition: sig .. end

Trigerring condition for transitions

type t = event list * guard list

The event list will be a singleton for normal transition, empty for initial transition

type event = string

event name

type guard = Expr.t

type env = (string * Expr.value) list

exception Illegal_guard_expr of Expr.t

Accessors

val vars_of : t -> Expr.VarSet.t

val events_of : t -> Expr.VarSet.t

Operations

val eval_guard : env -> guard -> bool

val eval_guards : env -> guard list -> bool

eval_guards env [g1;...gN] is true iff eval_guard env gi is true for each i=1...N

val rename : (string -> string) -> t -> t

rename f c renames f v each variable v occurring in c

val subst : Eval.env -> t -> t

subst env (evs,guards) replaces each variable v occuring in guards by its value if found in env, simplifying the resulting expression whenever possible.

Printers

val string_of_guard : guard -> string

val to_string : t -> string