Data specifications
This page describes all builtin 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 nonempty 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 nonterminal 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 nonterminal
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 nonempty 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
nonterminal 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, welltyped 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 righthand 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 betaredex, 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:
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 n1
and n2
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 userdefined sorts.
Name 
Sort(s) 
Semantics 



Equality 


Inequality, always equivalent to 


Less than 


Greater than, always equivalent to 


Less than or equal to, always equivalent to 


Greater than or equal to, always equivalent to 


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.
Sort 
Semantics 


Booleans 

Positive numbers 

Natural numbers 

Integers 

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.
Name 
Sort(s) 
Semantics 



Logical negation 


Logical and 


Logical or 


Logical implication 


Universal quantifier 


Existential quantifier 
The universal and existential quantifier need some extra clarification. Their
concrete syntax (as given by the nonterminal 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.
Name 
Sort(s) 
Semantics 


Pos > Int Nat > Int Int > Int Real > Real 
Negation 


Minimum of 


Maximum of 

Pos # Pos > Pos Pos # Nat > Pos Nat # Pos > Pos Nat # Nat > Nat Int # Int > Int Real # Real > Real 
Sum (addition) of 

Pos # Pos > Int Nat # Nat > Int Int # Int > Int Real # Real > Real 
Difference (subtraction) of 


Product (multiplication) of 


Quotient (division) of 

Pos > Pos Nat > Pos Int > Int Real > Real 
Successor (equivalent to 

Pos > Nat Nat > Int Int > Int Real > Real 
Predecessor (equivalent to 

Nat # Pos > Nat Int # Pos > Int 
Integer division 

Nat # Pos > Nat Int # Pos > Nat 
Remainder of 

Pos # Nat > Pos Nat # Nat > Nat Int # Nat > Int Real # Int > Real 
Exponentiation ( 

Int > Nat Real > Real 
Absolute value of 


The greatest integer smaller than 


The least integer larger than 


Equal to 


Cast 


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.
Name 
Sort(s) 
Semantics 



Function application (applies 


Function update; returns a mapping that maps 


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”: metasorts that allow you to specify a list, set or bag (multiset) of a certain sort.
Sort 
Semantics 


Lists with elements of sort 

Sets with elements of sort 

Bags with elements of sort 
For these container sorts, a number of operations is defined. One operation is
defined on all containers (substitute List
, Set
or Bag
for
C
):
Name 
Sort(s) 
Semantics 



True if 
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 > ... > []
Name 
Sort(s) 
Semantics 






True if 


The length of 


The element of 





The first element of 





The last element of 



Warning
Lists are implemented as singlylinked 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.
Name 
Sort(s) 
Semantics 



Set comprehension: denotes the set of elements 


Set complement of 


Set union of 


Set difference of 


Set intersection of 
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:
Name 
Sort(s) 
Semantics 



The number 
To make it easy to interpret sets as bags, and to convert bags to sets, the following operations are also defined:
Name 
Sort(s) 
Semantics 



The bag 


The set 
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 (lefttoright).
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.