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.

• Lexical elements
  • Comments
• Data specifications
  • Specifying sorts
  • Data expressions
  • Specifying mappings
  • Predefined mappings
  • Predefined sorts
  • Constructed sorts
  • Global variables
• Process syntax
• Process specifications
  • Actions
  • Process algebra
  • Adding data
  • Parallel composition
  • Communication and allow
  • Rename and hide
  • Time

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.