Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package rfsm
Dynamic models (used by the simulator)
FSM
type fsm = {f_static : Fsm.inst;(*Static representation
*)f_vars : (string * (Types.typ * Expr.value)) list;(*name, (type, value)
*)f_state : string;(*Current state
*)f_has_reacted : bool;(*true when implied in the last reaction
*)
}Local evaluation environment
type lenv = (string * Expr.value) listGlobal evaluation environment
type genv = {fe_inputs : (string * (Types.typ * Expr.value)) list;(*Global inputs
*)fe_csts : (string * (Types.typ * Expr.value)) list;(*Global constants
*)fe_fns : (string * (Types.typ * Expr.value)) list;(*Global functions
*)fe_vars : (string * (Types.typ * Expr.value)) list;(*Shared variables
*)fe_evs : (string * (Types.typ * Expr.value)) list;(*Shared events
*)
}Builders
Input and output events
type event = loc * Expr.valueEvent location, new value
Exceptions
exception IllegalTrans of fsm * stringexception Undeterminate of fsm * string * Types.dateexception NonDetTrans of fsm * Fsm.transition list * Types.dateAccessors
fireable f env t returns true iff transition t in FSM f is fireable, given ocal env env.
val check_cond : fsm -> lenv -> Condition.t -> boolcheck_cond f env c evaluatues condition c in FSM f, in the context of local env env.
val is_event_set : lenv -> Condition.event -> boolis_event_set env ev indicates whether event ev is set in local environment env
Simulation
init env f performs the initial transition of FSM f, in global environment env, Returns an updated fsm and list of events consisting of
- updates to global outputs or shared objects
- updates to local variables (including state move)
val react : Types.date -> genv -> fsm -> fsm * event listreact t env f compute the reaction, at time t of FSM f in global environment env. The global environment contains the values of global inputs, shared objects and global functions/constants. As for init, returns an updated fsm and list of events.