module TransLabel:sig
..end
typet =
Condition.t * Action.t list * int * bool
(cond,acts,p,i)
means that the corresponding carrying transition will be
taken whenever cond
evaluates to true
, triggering actions acts
.
p
gives the priority level (used to resolve non-deterministic transitions).
i
indicates whether the corresponding transition is an implicit one.
val compare : t -> t -> int
val to_string : t -> string
val rename : (string -> string) -> t -> t
rename f l
renames f v
each variable v
occurring in l
val subst : Eval.env -> t -> t
subst env l
replaces each variable v
occuring in l
by its value if found in env
,
simplifying the resulting expression whenever possible.
val is_rtl : t -> bool
is_rtl t
returns true
iff each variable written by transition t
is written only once.
For rtl transitions, the sequantial and synchronous interpretations are equivalent.