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.0.tbz
sha256=4798916862412a0ac4721f63b77c243d7d7327c8ff2d18d379eb2f4202d43e4d
sha512=8475f03a5e81fbde01fb6ddd90f2c07d8a327d5d71301a8da6e169c5c1c8a8f94f528296b2c2d2be7abfbe10fceee048834926abbf5e739a62274f904a8f0869

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

Module Nuscrlib.Pragma

This module contains variables configuarations, to be set by pragmas or command line arguments, not to be changed for the duration of the program

type t =
  1. | NestedProtocols
  2. | ShowPragmas
  3. | PrintUsage
  4. | RefinementTypes
  5. | SenderValidateRefinements
  6. | ReceiverValidateRefinements
  7. | ValidateRefinementSatisfiability
  8. | ValidateRefinementProgress
val pragma_of_string : string -> t
type pragmas = (t * string option) list
val show_pragmas : pragmas -> Ppx_deriving_runtime.string
val solver_show_queries : unit -> bool

Whether to display queries to SMT solvers (with RefinementTypes pragma)

val set_solver_show_queries : bool -> unit

Set solver_show_queries

val nested_protocol_enabled : unit -> bool

Whether NestedProtocol pragma is enabled

val set_nested_protocol : bool -> unit

Set nested_protocol_enabled

val refinement_type_enabled : unit -> bool

Whether RefinementTypes pragma is enabled

val set_refinement_type : bool -> unit

Set refinement_type

val sender_validate_refinements : unit -> bool

When refinement types are enabled, senders should validate refinements

val set_sender_validate_refinements : bool -> unit

Set sender_validate_refinements

val receiver_validate_refinements : unit -> bool

When refinement types are enabled, receivers should validate refinements

val set_receiver_validate_refinements : bool -> unit

Set receiver_validate_refinements

val validate_refinement_satisfiability : unit -> bool

Validate whether a refined global type is semantically satisfiable

val set_validate_refinement_satisfiability : bool -> unit

Set validate_refinement_satisfiability

val validate_refinement_progress : unit -> bool

Validate whether a refined global type satisfies progress semantically

val set_validate_refinement_progress : bool -> unit

Set validate_refinement_progress

val verbose : unit -> bool

Whether to produce verbose outputs

val set_verbose : bool -> unit

Set verbose

val reset : unit -> unit

Reset all configuration to default

val load_from_pragmas : pragmas -> unit

Load config from pragmas