package nuscr

  1. Overview
  2. Docs
A tool to manipulate and validate Scribble-style multiparty protocols

Install 

dune-project
 Dependency

nuscr.dev Changelog Edit opam file Versions (5)

Authors

  1. F
    Francisco Ferreira
  2. F
    Fangyi Zhou
  3. S
    Simon Castellan
  4. B
    Benito Echarren

Maintainers

  1. F
    Francisco Ferreira

Sources

nuscr-2.1.1.tbz
sha256=c5a419fd1fdea78fb63b3a3c335b0e6b0f2b08d65b79870565bdcc0f997bc728
sha512=83ef593ed514eeef1b10069af54562833d617d1c338c5adaf82ee5c3ea7ec4569b3643fcbb237b3cb79ce2f579094cbd17217efa5f4e522bd20f67e1df3a7dbd

doc/nuscr.lib/Nuscrlib/Ltype/index.html

Module Nuscrlib.Ltype

Local type management

type t =
  1. | RecvL of Gtype.message * Names.RoleName.t * t
    (*

    RecvL (msg, name, t) waits for message msg from name and continues as t

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

    SendL (msg, name, t) sends message msg to name and continues as t

    *)
  3. | ChoiceL of Names.RoleName.t * t Base.list
    (*

    ChoiceL (name, ts) is a choice (internal or external) from name between the ts

    *)
  4. | TVarL of Names.TypeVariableName.t * Expr.t Base.list
    (*

    TVarL (type_var, exprs) is a type variable, scoped inside a recursion. type_var is the name of the type variable, exprs are expressions supplied into paramterised recursion, used in RefinementTypes extension. Otherwise an empty list is supplied when that feature is not used.

    *)
  5. | MuL of Names.TypeVariableName.t * (Base.bool * Gtype.rec_var) Base.list * t
    (*

    MuL (type_var, rec_vars, l) is a recursive type, corresponding to the syntax `\mu t. L`, where t is represented by type_var and L is represented by t. rec_vars are recursion parameters, where the first component represents whether the variable is a silent variable (with multiplicity 0). These parameters are used in RefinementTypes extension for parameterised recursion, an empty list is supplied when that feature is not used.

    *)
  6. | EndL
    (*

    Empty type

    *)
  7. | InviteCreateL of Names.RoleName.t Base.list * Names.RoleName.t Base.list * Names.ProtocolName.t * t
    (*

    Send invitations to existing roles and set up/create dynamic pariticipants, used only in NestedProtocols extension

    *)
  8. | AcceptL of Names.RoleName.t * Names.ProtocolName.t * Names.RoleName.t Base.list * Names.RoleName.t Base.list * Names.RoleName.t * t
    (*

    accept role@Proto(roles...; new roles...) from X; t, used only in Nested Protocols extension

    *)
  9. | SilentL of Names.VariableName.t * Expr.payload_type * t
    (*

    Used with refinement types to indicate knowledge obtained via a global protocol, used only in RefinementTypes extension

    *)

Local types. See also LiteratureSyntax.local for a simpler syntax.

module LocalProtocolId : sig ... end

Unique id identifying a local protocol

Mapping of local protocol id to the protocol's roles and local type

val show : t -> Base.string

Converts a local type to a string.

val show_nested_t : nested_t -> Base.string
val project : Names.RoleName.t -> Gtype.t -> t

Project a global type into a particular role.

val project_nested_t : Gtype.nested_t -> nested_t

Generate the local protocols for a given global_t

val ensure_unique_tvars : nested_t -> nested_t

Ensure that all the local variables in each local protocol are globally unique, renaming variables to resolve conflicts

Mapping from local protocol ids to their unique local protocol names

val build_local_proto_name_lookup : nested_t -> local_proto_name_lookup

Builds a map containing the unique string representations for the unique local protocol ids

val show_lookup_table : local_proto_name_lookup -> Base.string

Converts a local protocol name lookup table to a string

Return the unique local protocol name for a (role, protocol) pair

Look up the unique name for a local protocol id