# 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.