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