Module ScmWrapper


module ScmWrapper: sig .. end
SCM Model Wrapper.

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:

w -- c!a --> w' if w' = w or w' = w·a

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: 
functor (A : sig
val scm : Scm_syn.global_scm
end) -> Model.S
Functor providing an implementation of the 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