Data specifications

This page describes all built-in data types with their associated functions and operators, and describes how custom data types can be defined.

A data specification consists of a number of sorts, a number of constructors for each sort, a number of mappings, and a set of equations. A data specification is an equational specification, in which sorts denote data types. The semantics of a sort is a non-empty set. The elements of the semantics of a sort are described by its constructors, whereas the mappings are functions defined on the semantics of sorts. The equations (axioms) describe equational properties of functions and elements of the semantics.

Note that every element of the semantics of a sort can be constructed from its constructors (this is a property also known as “no junk”). It may however be the case that an element can be described by several constructors (in which case it violates a property commonly known as “no confusion”). The only exception to this are the booleans; true and false are distinct elements.

In mCRL2, a sort is either a predefined sort, a constructed sort, or a sort that was declared in a sort specification. The grammar of a sort description is given by the non-terminal SortExpr.

ProjDecl ProjDeclList ConstrDecl ConstrDeclList SortExpr

ProjDecl       ::=  (Id ':')? SortExpr
ProjDeclList   ::=  ProjDecl (',' ProjDecl)*
ConstrDecl     ::=  Id ('(' ProjDeclList ')')? ('?' Id)?
ConstrDeclList ::=  ConstrDecl ('|' ConstrDecl)*
SortExpr       ::=  'Bool' |
                    'Pos' |
                    'Nat' |
                    'Int' |
                    'Real' |
                    'List' '(' SortExpr ')' |
                    'Set' '(' SortExpr ')' |
                    'Bag' '(' SortExpr ')' |
                    'FSet' '(' SortExpr ')' |
                    'FBag' '(' SortExpr ')' |
                    Id |
                    '(' SortExpr ')' |
                    'struct' ConstrDeclList |
                    SortExpr '->' SortExpr |
                    SortExpr '#' SortExpr

Specifying sorts

In an mCRL2 specification, sorts may be declared in a sort specification. In the grammar below, a sort specification is generated by the non-terminal SortSpec in the grammar below.

SortDecl SortSpec IdsDecl ConsSpec

SortDecl ::=  IdList ';' |
              Id '=' SortExpr ';'
SortSpec ::=  'sort' SortDecl+
IdsDecl  ::=  IdList ':' SortExpr
ConsSpec ::=  'cons' (IdsDecl ';')+

Sort specifications are best understood by looking at an example. We will define a sort Natural, representing the natural numbers. We will do so by defining a constructor zero for it, and a successor relation succ:

sort Natural;
cons zero: Natural;
     succ: Natural -> Natural;

Note that if we leave out the cons statement, we have still defined the sort Natural. In that case, however, mCRL2 will not know anything about this sort except that it represents a non-empty set. There are cases in which such underspecification can be used, for instance to model user data that passes through a system, but that does not influence the behaviour of a system.

The syntax of constructor specifications is given by the ConsSpec non-terminal above. Every constructor for a sort S must be specified in a cons block, and is specified by a name and a sort that is a mapping to S. Note that S can be seen as a nullary mapping to S.

A sort can either be one one of the predefined sorts, or a sort that you specified yourself (or will specify later in the specification, as the order of the statements in an mCRL2 specification does not change the meaning of the specification).

Let’s have a look at a slightly more complicated encoding of numbers, in this case the positive numbers. We will use the predefined sort Bool, which consists of the (distinct) elements true and false:

sort Positive;
cons one: Positive;
     cdub: Bool # Positive -> Positive;

If we now interpret the term cdub(true, num) (where num is a term of sort Positive) as “twice the number that num represents, plus 1”, and interpret cdub(false, num) as “twice the number that num represents”, then we have created a binary encoding of the positive numbers. For instance, cdub(true, one) represents the number 3, and cdub(false, cdub(true, cdub(false, one))) represents the number 10.

Note

In mCRL2, the encoding of numbers (integers, positive numbers and natural numbers) is binary, much like the example above.

Hint

If you need a more complex sort than described above, you will usually be able to make a constructed sort that suits your needs.

Data expressions

Data expressions are descriptions of an element of a sort. Therefore, any closed, well-typed expression is a data expression. The full grammar is given below.

DataExpr DataExprList BagEnumElt BagEnumEltList IdList VarDecl VarsDecl VarsDeclList Assignment AssignmentList

DataExpr       ::=  Id |
                    Number |
                    'true' |
                    'false' |
                    '[' ']' |
                    '{' '}' |
                    '{'':''}' |
                    '[' DataExprList ']' |
                    '{' BagEnumEltList '}' |
                    '{' VarDecl '|' DataExpr '}' |
                    '{' DataExprList '}' |
                    '(' DataExpr ')' |
                    DataExpr '[' DataExpr '->' DataExpr ']' |
                    DataExpr '(' DataExprList ')' |
                    '!' DataExpr |
                    '-' DataExpr |
                    '#' DataExpr |
                    'forall' VarsDeclList '.' DataExpr |
                    'exists' VarsDeclList '.' DataExpr |
                    'lambda' VarsDeclList '.' DataExpr |
                    DataExpr '=>' DataExpr |
                    DataExpr '||' DataExpr |
                    DataExpr '&&' DataExpr |
                    DataExpr '==' DataExpr |
                    DataExpr '!=' DataExpr |
                    DataExpr '<' DataExpr |
                    DataExpr '<=' DataExpr |
                    DataExpr '>=' DataExpr |
                    DataExpr '>' DataExpr |
                    DataExpr 'in' DataExpr |
                    DataExpr '|>' DataExpr |
                    DataExpr '<|' DataExpr |
                    DataExpr '++' DataExpr |
                    DataExpr '+' DataExpr |
                    DataExpr '-' DataExpr |
                    DataExpr '/' DataExpr |
                    DataExpr 'div' DataExpr |
                    DataExpr 'mod' DataExpr |
                    DataExpr '*' DataExpr |
                    DataExpr '.' DataExpr |
                    DataExpr 'whr' AssignmentList 'end'
DataExprList   ::=  DataExpr (',' DataExpr)*
BagEnumElt     ::=  DataExpr ':' DataExpr
BagEnumEltList ::=  BagEnumElt (',' BagEnumElt)*
IdList         ::=  Id (',' Id)*
VarDecl        ::=  Id ':' SortExpr
VarsDecl       ::=  IdList ':' SortExpr
VarsDeclList   ::=  VarsDecl (',' VarsDecl)*
Assignment     ::=  Id '=' DataExpr
AssignmentList ::=  Assignment (',' Assignment)*

A notable construction that is not standard is the where clause, which can be used to substitute subexpressions in a data expression. Where clauses can be useful for efficiency reasons. For example, we can define a function that computes the square of the sum of two numbers as follows:

map square_sum: Int # Int -> Int;
var x, y: Int;
eqn square_sum(x, y) = (x + y) * (x + y);

When evaluating square_sum(2, 3), this will rewrite to (2 + 3) * (2 + 3), which causes the expression 2 + 3 to be evaluated twice.

Using a where clause we enforce that the right-hand sides of local definitions is evaluated exactly once:

var x, y: Int;
eqn square_sum(x,y) = z * z whr z = x + y end;

Note that technically a where clause just introduces a beta-redex, so we could also have defined the following:

var x, y: Int;
eqn square_sum(x, y) = (lambda z: Int . z * z)(x + y);

Specifying mappings

Mappings, like constructors, are functions that take zero or more arguments. The difference lies in the fact that mappings say nothing about the sort that is their image (where constructors show you how to construct elements of that sort).

To be more precise, mappings are aliases for an element of a specific sort, and can be specified by the following grammar:

IdsDecl MapSpec

IdsDecl ::=  IdList ':' SortExpr
MapSpec ::=  'map' (IdsDecl ';')+

Equational specifications give further information about how the elements that these aliases represent behave. Equational specifications are given by the grammar below.

VarsDecl VarsDeclList VarSpec EqnDecl EqnSpec

VarsDecl     ::=  IdList ':' SortExpr
VarsDeclList ::=  VarsDecl (',' VarsDecl)*
VarSpec      ::=  'var' (VarsDeclList ';')+
EqnDecl      ::=  (DataExpr '->')? DataExpr '=' DataExpr ';'
EqnSpec      ::=  VarSpec? 'eqn' EqnDecl+

Equation systems are optionally preceded by a var block that defines variables that are used in the eqn block that follows. Variables are used to do pattern matching in equation systems. To illustrate this, let us look at a specification of the Fibonacci sequence:

map fib: Nat -> Nat;
var n: Nat;
eqn n <= 1 -> fib(n) = n;
    n > 1 -> fib(n) = fib(Int2Nat(n - 1)) + fib(Int2Nat(n - 2))

Going through the code line by line, we see a mapping fib being defined that maps natural numbers to natural numbers. Then a variable n of sort Nat is declared.

On the third line, the first rewrite rule is declared, that says that if a term of the form fib(n) is encountered, where n is the variable and can hence match any term of sort Nat, then it can be rewritten to the value that matches the variable, if that value is at most 1.

The second rewrite rule says that if a term of the form fib(n) is encountered, then it can be rewritten to fib(Int2Nat(n - 1)) + fib(Int2Nat(n - 2)) if n was larger than 1.

In the above, we need to use Int2Nat to convince the type checking system that n-1 and n-2 will indeed be natural numbers. In general this is not true (for n <= 1), but we are making the executive decision that we know better than the type checker, because we know that the condition of the rewrite rule will prevent us from getting into trouble.

Example (underspecification)

Consider the following data specification:

sort A, B;
cons b: B;
map f: A;
    g: B;
    h: A -> B;
var a: A;
eqn h(a) = b;

The sort B is defined as the singleton set {b}, but A is left unspecified. Therefore, we cannot know what element f maps to. For g on the other hand, we know that g maps to b, as it is the only element of B, but as this is not specified in the equational specification, mCRL2 will not detect this. However, the data expression h(f) will be rewritten to b, as it matches the only rule in this equation system.

Example (rewrite rules)

In order to describe the behaviour of mappings, we need to give mCRL2 an equational specification of the mapping we wish to define. As an example, we will specify the exclusive or operation on booleans:

map xor: Bool # Bool -> Bool;
eqn xor(false, false) = false;
    xor(false, true) = true;
    xor(true, false) = true;
    xor(true, true) = false;

This is rather verbose if we know that we already have a definition of inequality of booleans. We could therefore also specify it as follows:

map xor: Bool # Bool -> Bool;
var a, b: Bool;
eqn xor(a, b) = a != b;

Yet another way of specifying the same mapping would be to use the rewrite conditions to test for equality:

map xor: Bool # Bool -> Bool;
var a, b: Bool;
eqn a == b -> xor(a, b) = false;
    a != b -> xor(a, b) = true;

Warning

Functional programmers might have written down the following specification for the Fibonacci sequence:

map fib: Nat -> Nat;
var n: Nat;
eqn fib(0) = 0;
    fib(1) = 1;
    fib(n + 2) = fib(n) + fib(n + 1);

This, however, will not work in mCRL2: fib(10) will not rewrite at all. The reason is that the pattern matching used in the rewrite system fails to match n + 2 to 10, because the number 10 is internally represented using a binary encoding, and therefore has a different structure than n + 2.

This kind of pattern matching can still be used, but it is advisable to only match terms that consist of only constructors and variables. One particularly useful example is that of lists, for which the constructors [] and |> are defined:

map remove: List(Nat) # Nat -> List(Nat);
var x, y: Nat;
    l: List(Nat);
eqn remove([], x) = [];
    x == y -> remove(x |> l, y) = l;
    x != y -> remove(x |> l, y) = x |> remove(l, y);

Predefined mappings

The mappings in the following table are defined on all sorts, even on user-defined sorts.

Predefined operations on *all* sorts
Name	Sort(s)	Semantics
`a == b`	`S # S -> Bool`	Equality
`a != b`	`S # S -> Bool`	Inequality, always equivalent to `!(a == b)`
`a < b`	`S # S -> Bool`	Less than
`a > b`	`S # S -> Bool`	Greater than, always equivalent to `b < a`
`a <= b`	`S # S -> Bool`	Less than or equal to, always equivalent to `a < b \|\| a == b`.
`a >= b`	`S # S -> Bool`	Greater than or equal to, always equivalent to `b <= a`
`if(c, a, b)`	`Bool # S # S -> S`	Conditional value

For any sort S (even for user defined sorts), the mappings have the following equational properties:

var s, t: S;
    b: Bool;
eqn s == s -> true;
    s < s -> false;
    s <= s -> true;
    if(true, s, t) = s;
    if(false, s, t) = t;
    if(b, s, s) = s;

For mapping sorts and user defined sorts, only these equations are specified.

For the predefined sorts, the mappings work as expected (so 12 < 16 and 23/12 == 46/24). For lists, the < and <= operators define the lexicographical ordering (so [2, 3] > [1, 2, 3], and [] < [1]). For sets and bags, they define the subset (resp. subbag) relation.

Finally, for structured sorts, the definitions of < and <= are a bit more involved; they are described in the section about structured sorts.

Note

The fact that every predefined and constructed sort has a strict ordering associated with it makes it possible for mCRL2 to define a fairly efficient implementation of sets.

Warning

Be careful when specifying user defined sorts: the above operations are only partially defined. Trying to compare two syntactically different data expressions may not lead to the desired result, unless additional rewrite rules for ==, < and <= are added.

In particular, the following will not work as expected:

sort S;
cons a, b: S;
map x: Set(S);
eqn x = {a} + {b};

Evaluating x will show you that it is equal to @fset_union(@false_, @false_, {a}, {b}), which may not be what you were expecting to see. Completing the definition of < for S fixes the problem:

sort S;
cons a, b: S;
map x: Set(S);
eqn x = {a} + {b};
    a < b = true;
    b < a = false;

Now, x evaluates to {a, b}.

Predefined sorts

To make modelling more convenient, mCRL2 provides a number of predefined sorts. These sorts are listed in the table below. In section Mappings on predefined sorts standard operations are defined on all predefined sorts.

Basic sorts in mCRL2
Sort	Semantics
`Bool`	Booleans
`Pos`	Positive numbers
`Nat`	Natural numbers
`Int`	Integers
`Real`	Rationals

The constants true and false are defined as the only constructors for the sort Bool.

Any Number that occurs in mCRL2 input is interpreted as a constant of one of the integral sorts. All datatypes, including the standard data types, are internally represented using abstract data types. This has the advantage that numbers do not have a limited range. In particular, there is no largest number in any of these domains, and there are no smallest integers and reals.

Example

If the mCRL2 toolset encounters the string 1024 in a context where a Pos, Nat, Int or Real was expected, then it will be interpreted as the decimal number 1024 of sort Pos, as this is the most specific type that matches.

Example

To specify the decimal fractional value 3.141592, you will need to specify it as a fraction, i.e., 3141592/1000000.

Mappings on predefined sorts

For the predefined sorts, mCRL2 defines some common operations. The predefined operations on the Booleans are given in the table below.

Predefined operations on Booleans
Name	Sort(s)	Semantics
`! a`	`Bool -> Bool`	Logical negation
`a && b`	`Bool # Bool -> Bool`	Logical and
`a \|\| b`	`Bool # Bool -> Bool`	Logical or
`a => b`	`Bool # Bool -> Bool`	Logical implication
`forall V . b`	`Bool -> Bool`	Universal quantifier
`exists V . b`	`Bool -> Bool`	Existential quantifier

The universal and existential quantifier need some extra clarification. Their concrete syntax (as given by the non-terminal DataExpr) is illustrated in the example below:

exists n, m: Nat, p: Pos . n + m == p;

The V in the table above is a specification of locally bound variables, that occur in the expression after the period (.). Evaluation of quantifiers is done by using the constructors of a sort to enumerate all possible values of that sort, and then check for each such value whether the expression holds. This means that evaluation some quantifiers will not terminate:

exists n: Nat . n + 1 == n + 2
exists n: Nat . n - 1 == n - 2

The upper expression will evaluate to false, because the rewriter happens to rewrite n + 1 and n + 2 to a form in which it can prove that they are not equal. The expression below that, however, will be rewritten forever, because the rewriter will decide to check the equality for every value of n.

For the numeric sorts, the predefined mappings are listed in the table below. Where N is used in the sort of a mapping, any numeric sort may be substituted.

Predefined operations on numeric sorts
Name	Sort(s)	Semantics
`- a`	`Pos -> Int` `Nat -> Int` `Int -> Int` `Real -> Real`	Negation
`min(a, b)`	`N # N -> N`	Minimum of `a` and `b`.
`max(a, b)`	`N # N -> N`	Maximum of `a` and `b`.
`a + b`	`Pos # Pos -> Pos` `Pos # Nat -> Pos` `Nat # Pos -> Pos` `Nat # Nat -> Nat` `Int # Int -> Int` `Real # Real -> Real`	Sum (addition) of `a` and `b`.
`a - b`	`Pos # Pos -> Int` `Nat # Nat -> Int` `Int # Int -> Int` `Real # Real -> Real`	Difference (subtraction) of `a` and `b`.
`a * b`	`N # N -> N`	Product (multiplication) of `a` and `b`
`a / b`	`N # N -> Real`	Quotient (division) of `a` and `b`
`succ(a)`	`Pos -> Pos` `Nat -> Pos` `Int -> Int` `Real -> Real`	Successor (equivalent to `a + 1`)
`pred(a)`	`Pos -> Nat` `Nat -> Int` `Int -> Int` `Real -> Real`	Predecessor (equivalent to `a - 1`)
`a div b`	`Nat # Pos -> Nat` `Int # Pos -> Int`	Integer division
`a mod b`	`Nat # Pos -> Nat` `Int # Pos -> Nat`	Remainder of `a` divided by `b`.
`exp(a, b)`	`Pos # Nat -> Pos` `Nat # Nat -> Nat` `Int # Nat -> Int` `Real # Int -> Real`	Exponentiation (`a` raised to the power `b`).
`abs(a)`	`Int -> Nat` `Real -> Real`	Absolute value of `a`.
`floor(a)`	`Real -> Int`	The greatest integer smaller than `a`.
`ceil(a)`	`Real -> Int`	The least integer larger than `a`.
`round(a)`	`Real -> Int`	Equal to `floor(a + 1/2)`.
`Pos2Nat(_)`	`Pos -> Nat`	Cast
`Nat2Pos(_)`	`Nat -> Pos`	Cast

Lastly, there are a number of casts that allow the user to interpret a numeric value as if it were of a different sort. To this end, the mappings A2B are defined, where A and B are either of Pos, Nat, Int or Real.

Constructed sorts

To enable users to quickly specify more complicated sorts without having to resort to manually specifying constructors and operations on those sorts, mCRL2 provides some standard constructs to build new sorts out of existing ones.

SortExpr

SortExpr ::=  'Bool' |
              'Pos' |
              'Nat' |
              'Int' |
              'Real' |
              'List' '(' SortExpr ')' |
              'Set' '(' SortExpr ')' |
              'Bag' '(' SortExpr ')' |
              'FSet' '(' SortExpr ')' |
              'FBag' '(' SortExpr ')' |
              Id |
              '(' SortExpr ')' |
              'struct' ConstrDeclList |
              SortExpr '->' SortExpr |
              SortExpr '#' SortExpr

Mapping sorts

If D1, D2, …, DN are sorts, and I is a sort, then D1 # D2 # ... # DN -> I is the sort of a mapping from the carthesian product of D1 through DN to I. Note that # and -> are distinct operators, the first creating the carthesian product of two sorts, and the second creating a sort that represents the mapping of one sort to another. The use of carthesian products as sorts is however limited in mCRL2: they may only occur as the domain of mapping sorts. One further exception will be made later, when we look at the process language, where we will see that also actions are allowed to have a sort that is a carthesian product.

Predefined operations on mapping sorts
Name	Sort(s)	Semantics
`a(b1, ..., bN)`	`(S1 # ... # SN -> I) # S1 # ... # SN -> I`	Function application (applies `a` to arguments `b1` through `bN`).
`a[b -> c]`	`(S -> I) # S # I -> (S -> I)`	Function update; returns a mapping that maps `b` to `c`, and that maps all other elements like `a` does.
`lambda V . a`	`S -> I`	Lambda abstraction.

The syntax of lambda abstraction is similar to that of quantifiers. As an example, we define the mapping f that returns true if the sum of its first two arguments is equal to the third argument:

map f: Nat # Nat # Pos -> Bool;
eqn f = lambda x,y: Nat, p: Pos . x + y == p

For mappings that take one argument, we can use function updates to change a mapping locally, which can be useful to model (infinite) arrays:

sort Array = Nat -> Bool;
map set: Array # Nat -> Array;
    clear: Array # Nat -> Array;
var a: Array;
    n: Nat;
eqn set(a, n) = a[n -> true];
    clear(a, n) = a[n -> false];

Lists, sets and bags

mCRL2 defines a number of “containers”: meta-sorts that allow you to specify a list, set or bag (multiset) of a certain sort.

Container sorts in mCRL2
Sort	Semantics
`List(S)`	Lists with elements of sort `S`
`Set(S)`	Sets with elements of sort `S`
`Bag(S)`	Bags with elements of sort `S`

For these container sorts, a number of operations is defined. One operation is defined on all containers (substitute List, Set or Bag for C):

Predefined operations on containers
Name	Sort(s)	Semantics
`a in b`	C(S) # S -> C(S)`	True if `a` occurs in `b`, false otherwise.

Lists

For a given sort S, mCRL2 defines the [] as a constructor of sort List(S), representing the empty list. Furthermore, the constructor |> (pronounce “cons”) of sort S # List(S) -> List(S) is defined. List enumeration is defined as a shorthand to denote lists:

[a, b, ...] == a |> b |> ... |> []

Predefined operations on lists
Name	Sort(s)	Semantics
`a <\| b` (“snoc”)	`List(S) # S -> List(S)`	`a` with `b` appended to it.
`a in b`	`S # List(S) -> Bool`	True if `a` occurs in `b`, false otherwise.
`# a`	`List(S) -> Nat`	The length of `a`.
`a . b`	`List(S) # Nat -> S`	The element of `a` at position `b`. Indices are zero-based.
`a ++ b`	`List(S) # List(S) -> List(S)`	`a` concatenated with `b`.
`head(a)`	`List(S) -> S`	The first element of `a`.
`tail(a)`	`List(S) -> List(S)`	`a` without its first element.
`rhead(a)`	`List(S) -> S`	The last element of `a`.
`rtail(a)`	`List(S) -> List(S)`	`a` without its last element.

Warning

Lists are implemented as singly-linked lists. This means that the # operation is quite expensive (it has to run through the entire list), as are the <|, rhead and rtail operations.

Warning

The head (or rhead) of an empty list is not defined. In practice, this means that head([]) will not be rewritten any further.

Sets

Sets are defined in a similar fashion to lists. For every sort``S``, Set(S) denotes the sort of sets of elements from S. One constructor is publicly available: {}, the empty set. The other constructors are hidden from the user, as they are implementation specific. Sets can, like lists, be enumerated: {a, b, c} denotes the set containing elements a, b and c. Operations on sets are given by the following table.

Predefined operations on sets
Name	Sort(s)	Semantics
`{a : S \| b(a) }`	`(S -> Bool) -> Set(S)`	Set comprehension: denotes the set of elements `a` in `S` for which `b(a)` is true.
`!a`	`Set(S) -> Set(S)`	Set complement of `a`.
`a + b`	`Set(S) # Set(S) -> Set(S)`	Set union of `a` and `b`.
`a - b`	`Set(S) # Set(S) -> Set(S)`	Set difference of `a` and `b`.
`a * b`	`Set(S) # Set(S) -> Set(S)`	Set intersection of `a` and `b`.

A typical use of the set comprehension is for instance the following definition of the set of all prime numbers:

{ n: Pos | n > 1 && forall m, m': Pos . (m > 1 && m' > 1) => n != m * m' }

Bags

Bags (or multisets) are denoted much like sets, but require a count for every element:

{a:1, b:4, c:0} == {a:1, b:2, b:2} == {a:1, b:4}

The same operations as for sets are defined on bags, with the difference that bag comprehensions specify the number of times an element occurs in that bag. For example, the bag that contains every natural number twice is defined as follows:

{ n: Nat | 2 }

One additional operation is defined on bags to count how often an element occurs in a bag:

Predefined operations on sets
Name	Sort(s)	Semantics
`count(a, b)`	`S # Bag(S) -> Nat`	The number a`s in :samp:`b.

To make it easy to interpret sets as bags, and to convert bags to sets, the following operations are also defined:

Predefined operations on sets
Name	Sort(s)	Semantics
`Set2Bag(a)`	`Set(S) -> Bag(S)`	The bag `b` such that for all `x` in `S`, `count(b, x)` is 1 if `x in a`, and 0 otherwise.
`Bag2Set(a)`	`Bag(S) -> Set(S)`	The set `b` such that for all `x` in `S`, `x in b` iff `x in a`.

Structured sorts

Structured sorts are a short way to specify recursive data types as are commonly used in functional programming languages.

A structured type is of the following form:

struct c_1(p_1_1: S_1_1, ..., p_1_k1: S_1_k1)?r_1
       c_2(p_2_1: S_2_1, ..., p_2_k2: S_2_k2)?r_2
       ...
       c_n(p_n_1: S_n_1, ..., p_n_kn: S_n_kn)?r_n

This defines the type which we designate by S for brevity, together with the following functions:

cons c_i: S_i_1 # ... # S_i_ki -> S;
map p_i_j: S -> S_i_j;
    r_i: S -> Bool;

Here, p_i_j are projection functions, and r_i are recogniser functions. Projection and recogniser functions are optional; if a projection function is not specified the subsequent : symbol should also be left out, likewise if a recogniser function is not specified its preceding ? symbol should also be left out (see below for examples).

Note that structured sorts are often used in combination with sort references:

sort S = struct ... ;

This defines a structured sort which has S as an alias.

Note

The constructors of a structured sorts can be compared with the < and <= operators. They are defined as lexicographical orderings on the constructors and their elements: the first constructor specified is the least element, the last constructor the greatest; if a constructor has arguments, then two terms that have the same constructor as outermost symbol are compared by comparing their arguments lexicographically (left-to-right).

Example

A well known and illustrative example of a structured sort is the definition of the tree data structure in which elements of some sort A can be stored:

sort Tree = struct leaf(A) | node(Tree, Tree);

This specifies that a tree is either an expression of the form leaf(a) where a is an expression of sort A, or a tree is an expression of the form node(u, v) where u and v are expressions of sort Tree. What is actually generated out of this one line, is the following data specification:

sort Tree;
cons leaf: A -> Tree;
     node: Tree # Tree -> Tree;
var a, a': A;
    l, r, l', r': Tree;
eqn leaf(a) == leaf(a') = a == b;
    leaf(a) == node(l, r) = false;
    node(l, r) == leaf(a) = false;
    node(l, r) == node(l', r') = l == l' && r == r';
    leaf(a) < leaf(a') = a < a';
    leaf(a) < node(l, r) = true;
    node(l, r) < leaf(a) = false;
    node(l, r) < node(l', r') = l < l' || (l == l' && r < r');
    leaf(a) <= leaf(a') = a <= a';
    leaf(a) <= node(l, r) = true;
    node(l, r) <= leaf(a) = false;
    node(l, r) <= node(l', r') = l < l' || (l == l' && r <= r');

We can extend our tree to also have recogniser and projection functions:

sort Tree = struct leaf(value: A) ? is_leaf
                 | node(left: Tree, right: Tree) ? is_node;

This causes the following additional data specification to be added:

map value: Tree -> A;
    left: Tree -> Tree;
    right: Tree -> Tree;
    is_leaf: Tree -> Bool;
    is_node: Tree -> Bool;
var a: A;
    l, r: Tree;
eqn value(leaf(a)) = a;
    left(node(l, r)) = l;
    right(node(l, r)) = r;
    is_leaf(leaf(a)) = true;
    is_leaf(node(l, r)) = false;
    is_node(leaf(a)) = false;
    is_node(node(l, r)) = true;

The projection functions now enable you to extract data from trees:

map dfs: Tree -> List(A);
var t: Tree;
eqn is_leaf(t) -> dfs(t) = [value(t)];
    is_node(t) -> dfs(t) = dfs(left(t)) ++ dfs(right(t));

Example

An often used structured type is the enumerated type that consists of a finite number of elements. For instance, the sort MachineMode can be declared by

sort MachineMode = struct idle ? is_idle
                        | running ? is_running
                        | broken ? is_broken;

Note that idle < running and running < broken: there is a strict ordering on the constructors of the structured sort.

Example

A common example is the sort of pairs for given sorts A and B:

sort Pair = struct pair(fst: A, snd: B);

For a pair p the expression fst(p) gives its first element and snd(p) the second element.

Global variables

GlobVarSpec

GlobVarSpec ::=  'glob' (VarsDeclList ';')+

In process specifications and in parameterised boolean equation systems (PBESs), it is possible to use free variables. An example is the following:

act a;
glob x: Nat;
proc P = a(x) . P;
init P;

This represents a whole class of processes, namely for every value of x this process has a different value. The keyword glob stands for global variable. In each specification the keyword glob can be used an arbitrary number of times.

All glob declarations are grouped together. The names of the variables cannot coincide with other declared functions, processes, actions, variables (both in equations and in sum operators) and process and PBES parameters. Global variables can occur in process equations, in parameterised fixed point formulas and in init sections.

Global variables can be used in the common mathematical way. Consider for instance the equation: \(ax^2 + bx + c = 0\). There are four variables in this equation, namely \(a, b, c\) and \(x\). The use of the variables \(a, b\) and \(c\) allow to study this polynomial in a far more general setting than when these variables would have concrete values.

In some cases, the concrete values for global variables do not have influence on the process. In such a case instantiating the global variables to various concrete values will mean that the process has the same behaviour modulo strong bisimulation, or the same solution as a parameterised boolean equation system. In this case we call the process or PBES global variable insensitive.

An example is the following linearisation of a buffer:

sort D;
glob dummy1, dummy2: D;
act read, send: D;
proc P(b: Bool, d: D) =
       sum e: D . b -> read(e) . P(false, e) +
                 !b -> send(d) . P(true, dummy1);
init P(true, dummy2);

The idea is that if the parameter b is true, the value of the second parameter is not relevant anymore. Therefore, it can be set to any arbitrary value, which is indicated by the use of dummy1 and dummy2. As this specification is global variable insensitive, arbitrary concrete values can be chosen for these global variables if this is opportune.

The tool mcrl22lps may generate linear processes with global variables. It guarantees that the resulting specification is global variable insensitive. Certain transformation tools, like lpsconstelm and lps2pbes yield global variable insensitive output, provided the input in global variable insensitive. In case systems are not global variable insensitive the output of these tools can be garbage. It is the responsibility of those who apply the tools that the tools are used in a proper way. It is likely that most tools leave global variables untouched, unless a switch indicates that global variable insensitivity can be used.