package rfsm

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

Innovation. Community. Security.