Module ScmWrapper
module ScmWrapper:SCM Model Wrapper.sig
..end
This module provides a wrapper around Tristan Le Gall's syntax and semantics
modules for systems of communicating machines (SCMs). This permits access to
the SCM library through an implementation that respects the input interface
of the model-checking engines, defined in the Model
module.
The current implementation abstracts away all numerical information, i.e. the abstract numerical lattice used for lattice automata is the trivial lattice with two elements.
The semantics of lossy channels in this model corresponds to a (potential) loss of messages on emissions. Formally, if a channel c is declared lossy, then the semantics of send operations in this channel is given by:
If initial configurations have empty queues, then the reachability set with
this loss on emissions semantics is the same as the reachability set with
the classical lossy semantics (where channels can lose messages at any time
non-deterministically).
module Make:
Model.S
interface for a given
global SCM.
val parse : Lexing.lexbuf -> Scm_syn.scm
val make_global : Scm_syn.scm -> Scm_syn.global_scm
val check_global : Scm_syn.global_scm -> unit