mCRL2 specification

Every mCRL2 specification defines a process. The language elements that allow you to specify processes rely on the use of data. These aspects are presented in separate parts of the documentation. For the sake of completeness, a separate section is included that describes the lexical elements of the mCRL2 language.

Specification syntax

The mCRL2 specification format requires only that an init statement be present. This statement says which process the specification represents. It might be the case that a specification file contains definitions for multiple processes; the init statement specifies which of these definitions (if any) is used.

mCRL2SpecElt Init mCRL2Spec

mCRL2SpecElt ::=  SortSpec |
                  ConsSpec |
                  MapSpec |
                  EqnSpec |
                  GlobVarSpec |
                  ActSpec |
                  ProcSpec
Init         ::=  'init' ProcExpr ';'
mCRL2Spec    ::=  mCRL2SpecElt* Init mCRL2SpecElt*

Example

Assume that delta is a valid process (it is: it is the process that cannot do any action). A fairly minimal valid mCRL2 specification would be the following:

init delta;

Example

A slightly more elaborate specification that does not use data can be made by using constructs from the process language:

act a, b;
proc P = a . P + b;
init P;

This specification defines the process that can do any number of a actions, followed by a single b. After this, it terminates.

Note that the three lines in this specification could have been put in any order, and it would still specify the same process.