rfsm
  1. Overview
  2. Docs

Reactive Finite State Machines

type act_semantics =
  1. | Sequential
    (*

    sequential (ex: x:=x+1;y:=x with x=1 gives x=2,y=2)

    *)
  2. | Synchronous
    (*

    synchronous (ex: x:=x+1:y=x with x=1 gives x=2,y=1)

    *)
type fsm_config = {
  1. mutable act_sep : string;
    (*

    Default value: " "

    *)
  2. mutable act_sem : act_semantics;
    (*

    Default value: Sequential

    *)
}
val cfg : fsm_config
exception Undef_symbol of string * string * string

FSM, kind, name

exception Invalid_state of string * string

FSM, kind, name

FSM, id

exception Typing_error of string * string * Types.typ * Types.typ

FSM, id

what, where, type, type

States

module State : sig ... end

Transition labels

module TransLabel : sig ... end

Internal representation

module Repr : Lascar.Lts.T with type state = State.t and type label = TransLabel.t
type state = State.t
type transition = State.t * TransLabel.t * State.t
type itransition = TransLabel.t * State.t
val string_of_transition : transition -> string
val string_of_state : state -> string

FSM model

type model = {
  1. fm_name : string;
    (*

    name

    *)
  2. fm_params : (string * Types.typ) list;
    (*

    generic parameters

    *)
  3. fm_ios : (string * (Types.dir * Types.typ)) list;
    (*

    i/os

    *)
  4. fm_vars : (string * Types.typ) list;
    (*

    internal variables

    *)
  5. fm_repr : Repr.t;
    (*

    underlying LTS

    *)
}

FSM instance

type inst = {
  1. f_name : string;
  2. f_model : model;
  3. f_params : (string * (Types.typ * Expr.value)) list;
    (*

    name, type, actual value

    *)
  4. f_inps : (string * (Types.typ * Global.global)) list;
    (*

    local name, (type, global)

    *)
  5. f_outps : (string * (Types.typ * Global.global)) list;
    (*

    local name, (type, global)

    *)
  6. f_inouts : (string * (Types.typ * Global.global)) list;
    (*

    local name, (type, global)

    *)
  7. f_vars : (string * Types.typ) list;
    (*

    name, type

    *)
  8. f_repr : Repr.t;
    (*

    Static representation as a LTS (with _local_ names)

    *)
  9. f_l2g : string -> string;
    (*

    local -> global name

    *)
}

Builders

val build_model : name:string -> states:state list -> params:(string * Types.typ) list -> ios:(Types.dir * string * Types.typ) list -> vars:(string * Types.typ) list -> trans: (state * (Condition.event * Condition.guard list) * Action.t list * state * int) list -> itrans:(state * Action.t list) -> model
val build_instance : name:string -> model:model -> params:(string * Expr.value) list -> ios:Global.global list -> inst

Accessors

val states_of_inst : inst -> state list
val istate_of_inst : inst -> state option
val transitions_of_inst : inst -> transition list
val itransitions_of_inst : inst -> itransition list
val succs_inst : inst -> state -> (state * TransLabel.t) list
val input_events_of_inst : inst -> string list
val output_events_of_inst : inst -> string list
val is_rtl_inst : inst -> bool

is_rtl f is true iff all is_rtl a for all actions a of f

val states_of_model : model -> state list
val istate_of_model : model -> state option
val transitions_of_model : model -> transition list
val itransitions_of_model : model -> itransition list
val succs_model : model -> state -> (state * TransLabel.t) list
val input_events_of_model : model -> string list
val output_events_of_model : model -> string list
val is_rtl_model : model -> bool

is_rtl f is true iff all is_rtl a for all actions a of f

Exceptions

exception Binding_mismatch of string * string * string

FSM, kind, id

exception Invalid_parameter of string * string

FSM, kind, id

FSM, name

exception Uninstanciated_type_vars of string * string * string * string list

FSM, name

Externalizers

type dot_options =
  1. | OmitImplicitTransitions
  2. | GlobalNames
  3. | NoCaption
val dot_output_oc : out_channel -> ?dot_options:Utils.Dot.graph_style list -> ?options:dot_options list -> inst -> unit
val dot_output : ?fname:string -> ?dot_options:Utils.Dot.graph_style list -> ?options:dot_options list -> dir:string -> inst -> string

dot_output dir f writes a DOT representation of FSM instance f in directory dir. Returns the name of the written file.

val dot_output_model : ?fname:string -> ?dot_options:Utils.Dot.graph_style list -> ?options:dot_options list -> dir:string -> model -> string

dot_output_model dir m writes a DOT representation of FSM model m in directory dir. Returns the name of the written file.

val dump_model : out_channel -> model -> unit
val dump_inst : out_channel -> inst -> unit