package nuscr

  1. Overview
  2. Docs

Module Nuscrlib.Efsm

Endpoint finite state machines (EFSM)

type refinement_action_annot = {
  1. silent_vars : (Names.VariableName.t * Expr.payload_type) Base.list;
    (*

    List of silent variables and their types

    *)
  2. rec_expr_updates : Expr.t Base.list;
    (*

    List of updates to recursion variables

    *)
}

Annotation for refined actions, used when RefinementTypes pragma is enabled

val sexp_of_refinement_action_annot : refinement_action_annot -> Sexplib0.Sexp.t
type action =
  1. | SendA of Names.RoleName.t * Gtype.message * refinement_action_annot
    (*

    Sending a message to name

    *)
  2. | RecvA of Names.RoleName.t * Gtype.message * refinement_action_annot
    (*

    Receiving a message from name

    *)
  3. | Epsilon
    (*

    Not used

    *)

Transitions in the EFSM

type state = Base.int

Type of states in EFSM

module G : Graph.Sig.P with type V.t = state and type E.label = action and type E.t = state * action * state

EFSM graph representation

Information regarding recursion variables

type t = G.t * rec_var_info

Type of the EFSM, rec_var_info is only populated when refinement types are enabled

val of_local_type : Ltype.t -> state * t

Construct an EFSM from a local type

val show : t -> Base.string

Produce a DOT representation of EFSM, which can be visualised by Graphviz

val state_action_type : G.t -> state -> [ `Send of Names.RoleName.t | `Recv of Names.RoleName.t | `Mixed | `Terminal ]

Returns whether a state in the EFSM is a sending state (with only SendA outgoing actions), a receiving state (with only RecvA outgoing actions), a mixed state (with a mixture of SendA and RecvA actions), or a terminal state (without outgoing actions)

val find_all_payloads : G.t -> Base.Set.M(Names.PayloadTypeName).t
val find_all_roles : G.t -> Base.Set.M(Names.RoleName).t