nuscr 2.1.1 (latest) · OCaml Package

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 ->
  Ppx_deriving_runtime.int

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

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(Names.PayloadTypeName).t

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

package nuscr