sig
type t = {
f_static : Fsm.inst;
f_vars : (string * (Types.typ * Expr.value)) list;
f_state : string;
f_has_reacted : bool;
}
type lenv = (string * Expr.value) list
type genv = {
fe_inputs : (string * (Types.typ * Expr.value)) list;
fe_csts : (string * (Types.typ * Expr.value)) list;
fe_fns : (string * (Types.typ * Expr.value)) list;
fe_vars : (string * (Types.typ * Expr.value)) list;
fe_evs : (string * (Types.typ * Expr.value)) list;
}
val create : Fsm.inst -> Fsm_dyn.t
type event = Fsm_dyn.loc * Expr.value
and loc =
LVar of Ident.t
| LArrInd of Ident.t * int
| LRField of Ident.t * string
exception IllegalTrans of Fsm_dyn.t * string
exception IllegalAction of Fsm_dyn.t * Action.t
exception Undeterminate of Fsm_dyn.t * string * Types.date
exception NonDetTrans of Fsm_dyn.t * Fsm.transition list * Types.date
exception NonAtomicIoWrite of Fsm_dyn.t * Action.t
val fireable : Fsm_dyn.t -> Fsm_dyn.lenv -> Fsm.Repr.transition -> bool
val check_cond : Fsm_dyn.t -> Fsm_dyn.lenv -> Condition.t -> bool
val is_event_set : Fsm_dyn.lenv -> Condition.event -> bool
val init : Fsm_dyn.genv -> Fsm_dyn.t -> Fsm_dyn.t * Fsm_dyn.event list
val react :
Types.date -> Fsm_dyn.genv -> Fsm_dyn.t -> Fsm_dyn.t * Fsm_dyn.event list
end