Previous  Up  

Module Simul

module Simul: sig .. end

The simulator

exception Error of string
type config = {
   mutable max_micro_reactions : int;
} 
val cfg : config
type stimulus = Fsm_dyn.loc * Expr.value 
type response = Fsm_dyn.loc * Expr.value 
type reaction = Types.date * string * Stimuli.stimuli list * response list * string 
type context = {
   c_date : Types.date;
   c_inputs : (string * (Types.typ * Expr.value)) list;
   c_outputs : (string * (Types.typ * Expr.value)) list;
   c_fns : (string * (Types.typ * Expr.value)) list;
   c_csts : (string * (Types.typ * Expr.value)) list;
   c_vars : (string * (Types.typ * Expr.value)) list;
   c_evs : (string * (Types.typ * Expr.value)) list;
   c_fsms : Fsm_dyn.t list * Fsm_dyn.t list;
} 
exception OverReaction of Types.date
val react : Types.date ->
       context -> stimulus list -> context * response list

react t ctx stimuli computes a global reaction in ctx at time t given a set of stimuli stimuli, producing an updated context ctx' and a set of responses resps. The (operational) semantics is that of StateCharts. A reaction is viewed as a (finite) sequence of "micro-reactions". Each micro-reaction can generate stimuli which can trigger another micro-reaction (the related stimuli are here called "reentrant". However, a given FSM can only react once during a sequence of micro-reactions (this is implemented by partitionning FSMs into active/inactive subsets during a reaction. A reaction ends when all the micro-reactions have taken place, i.e. when the last one did not produce any further re-entrant stimulus.

val run : Sysm.t -> context * (Types.date * response list) list

run m runs a simulation of system m, returning the final context and a list of timed responses

Printers

val dump_context : context -> unit
val dump_reaction : int * Fsm_dyn.event list -> unit