Module Nuscrlib.Efsm

Endpoint finite state machines (EFSM)

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

List of silent variables and their types

rec_expr_updates : Expr.t Base.list;(*

List of updates to recursion variables


Annotation for refined actions, used when RefinementTypes pragma is enabled

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

Sending a message to name

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

Receiving a message from name

| Epsilon(*

Not used


Transitions in the EFSM

type state =

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

type rec_var_info = (Base.bool * Gtype.rec_var) Base.list Base.Map.M(Base.Int).t

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(Nuscrlib__.Names.PayloadTypeName).t
val find_all_roles : G.t -> Base.Set.M(Nuscrlib__.Names.RoleName).t