package rfsm

  1. Overview
  2. Docs

Dynamic models (used by the simulator)

FSM

type fsm = {
  1. f_static : Fsm.inst;
    (*

    Static representation

    *)
  2. f_vars : (string * (Types.typ * Expr.value)) list;
    (*

    name, (type, value)

    *)
  3. f_state : string;
    (*

    Current state

    *)
  4. f_has_reacted : bool;
    (*

    true when implied in the last reaction

    *)
}

Local evaluation environment

type lenv = (string * Expr.value) list

Global evaluation environment

type genv = {
  1. fe_inputs : (string * (Types.typ * Expr.value)) list;
    (*

    Global inputs

    *)
  2. fe_csts : (string * (Types.typ * Expr.value)) list;
    (*

    Global constants

    *)
  3. fe_fns : (string * (Types.typ * Expr.value)) list;
    (*

    Global functions

    *)
  4. fe_vars : (string * (Types.typ * Expr.value)) list;
    (*

    Shared variables

    *)
  5. fe_evs : (string * (Types.typ * Expr.value)) list;
    (*

    Shared events

    *)
}

Builders

val make_fsm : Fsm.inst -> fsm

create sf creates a dynamic FSM instance from a static description sf

Input and output events

type event = loc * Expr.value

Event location, new value

and loc =
  1. | LVar of Ident.t
    (*

    Scalar

    *)
  2. | LArrInd of Ident.t * int
    (*

    1D array location

    *)
  3. | LRField of Ident.t * string
    (*

    Record field

    *)

Exceptions

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

Accessors

val fireable : fsm -> lenv -> Fsm.Repr.transition -> bool

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 -> bool

check_cond f env c evaluatues condition c in FSM f, in the context of local env env.

val is_event_set : lenv -> Condition.event -> bool

is_event_set env ev indicates whether event ev is set in local environment env

Simulation

val init : genv -> fsm -> fsm * event list

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 list

react 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.

OCaml

Innovation. Community. Security.