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
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”, and interpret
cdub(false, num)
as “twice the number that num represents, plus
one”, then we have created a binary encoding of the positive numbers. For
instance, cdub(false, one)
represents the number 2, 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 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);
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 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);
The mappings in the following table are defined on all sorts, even on user-defined 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}
.
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 |
---|---|
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
.
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 |
---|---|---|
! 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.
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
.
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
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 |
---|---|---|
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];
mCRL2 defines a number of “containers”: meta-sorts that allow you to specify a list, set or bag (multiset) of a certain sort.
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
):
Name | Sort(s) | Semantics |
---|---|---|
a in b |
C(S) # S -> C(S)` |
True if a occurs in b , false otherwise. |
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 |
---|---|---|
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 a . |
tail(a) |
List(S) -> List(S) |
a without its first element. |
rhead(a) |
List(S) -> Nat |
The last element of a . |
rtail(a) |
List(S) -> Nat |
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 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 |
---|---|---|
{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 (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 |
---|---|---|
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:
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 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.
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.