MCRL2 primer

From MCRL2

mCRL2 is a behavioural description language. In this article we indicate the main features of the language. Note that there is an example directory included in the mCRL2 distribution, which contains many examples of mCRL2 specifications, modal formulas and state spaces ready for visualisation.

History

Around 1980 many process algebras were designed to model behaviour. Most notably were CCS (Calculus of Communicating Processes, Milner), ACP (Algebra of Communicating Processes, Bergstra and Klop) and CSP (Communicating Sequential Processes, Hoare). These process algebras were mainly used as an object of study, mainly due to their lack of proper data types.

In order to use these languages for actual modelling of behaviour a number of process algebraic specifiation languages have been designed, which invariably were extended with equational datatypes. The most well known is LOTOS (Language of Temporal Ordering Specifications , Brinksma), but others are PSF (Process Specification Formalism, Mauw and Veltink) and μCRL (micro Common Representation Language, Groote and Ponse).

Unfortunately, the use of abstract data types made these languages unpleasant when it came to the specification of complex behaviour. Therefore, we designed the language mCRL2 (the successor of μCRL) to contain exactly those data types that one would expect when writing specifications, namely Bool, Pos, Nat, Int, Real, lists, sets, bags, functions and functional data types. These data types are machine independent. For instance there is no upperbound on natural numbers, sets are not necessarily finite, quantification can be used within boolean terms and lambda abstraction is part of the language. Furthermore, the language features time and multi-actions, which were not present in most of the process specification languages of the previous generation.

Note that mCRL2 is extremely rich and it is easy to express non-computable behavioural specifications in it. Typically, for those specifications, tool supported analysis will not be very fruitful. The advanced use of mCRL2 requires a good understanding of the language, the underlying notions and even of the implementation of the analysis tools. For more straightforward use this is not needed. An effective rule of thumb is that everything that could be done using languages such as LOTOS, PSF and μCRL, can be done without a problem using mCRL2.

Sequential processes

The primitive operation of mCRL2 is the action. An action represents an event of any kind, be it sending a message, printing a letter on a screen or shaking hands. Such events are declared by

act send: Message, print: Letter#Screen, Shake_hand;

where Message, Letter and Screen are the sorts of the objects that are exchanged in such an event. An action can have 0 or more of such arguments.

Actions can be combined to describe behaviour, which represents all possible sequences of actions that can be done. The main operators are sequential composition, the dot '.', which puts two behaviours in sequence, and the alternative composition, the plus '+', which represents the choice between two behaviours. So, in the following P is the process where actions a, b and c can happen in sequence. In the process Q there is a choice between actions d and e. Finally, the process R consists of first doing a choice between a and b, followed by a sequence of c, d and e.

act a, b, c, d, e;
 
proc P = a.b.c;
     Q = d + e;
     R = (a + b).c.d.e;

Whether a process P + Q behaves as P or Q is determined by the first action that either P or Q carries out.

By using process variables at the right-hand side, recursive behaviour can be specified. A process that iteratively performs a read and a write action is written as

act read, write;
 
proc P = read.write.P;
 
init P;

The keyword init indicates that the process starts with the process P.

Actions are allowed to occur simultaneously. In this case we speak about multi-actions. A multi-action is a sequence of actions that are separated by bars. E.g. a|b|...|z. If we reconsider the example above, but we want to express that reading and writing must happen at the same time, this can be specified by

act read, write;
 
proc P = (read|write).P;
 
init P;

Multi-actions are an effective weapon against the state space explosion problem. By grouping several actions into one multi-action, the number of states in a specification can be reduced.

The empty multi-action is the so-called hidden or internal action, which is written as tau. The hidden action cannot be observed. It is not very useful when specifying the behaviour of processes, but it is essential when it comes to analysing processes.

There is one special process called deadlock, written as delta, which denotes a process that cannot perform anything. In particular nothing can happen after delta. So, the process delta.a and delta are the same.

Data types

In this section all built-in data types, complete with their associated operators are given. By declaring sorts, constructors, and mappings and defining equations the user can also define his own sorts.

Most convenient are the built-in data types, and the standard type constructors for lists, sets, bags, structs and functions. All these data types have built-in equality, inequality, and if-then-else functions.

Bool, Pos, Nat, Int, Real

mCRL2 has a number of elementary datatypes, namely booleans (Bool), positive natural numbers (Pos), natural numbers (Nat), integers (Int) and real numbers (Real). Typical expression are true, false, x>17 && y<=24 and forall x:Nat. max(x,3)+5==min(y,8). 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 domain, and there are no smallest integers and reals.

The operators on boolean data types are given in the following table.

Operators on numbers are given by the following table. In A2B the letters A and B stand for Pos, Nat, Int and Real. Of course, A and B cannot be the same. Note that mCRL2 is a strictly typed language, with a simple form of type coercion. Elements of type Pos can automatically become Nat, Nat can become Int and Int can become Real. For example 1 is of type Pos, but it can be used at any place where a number of an other type is expected. Internally, an explicit function of the form A2B(_) is written around it. The pretty printers of mCRL2 sometimes print this function, but sometimes omit it to improve readability.

Lists

For every sort A the sort of lists over sort A can be made by writing List(A). Typical lists are [1,4,9,16] and 3 |> 5 |> -7|>[]. The following operations are provided for lists. The use of abstact data types allows to avoid giving the definition if no clear choice is possible. For instance the head of the empty list [] is not defined. In practice this means that head([]) will not be simplified any further.

Functions

mCRL2 features the full use of functions. For example, the sort of functions from Nat to Nat is denoted by Nat -> Nat. Also functions from functions to functions, etc. are allowed, e.g. (Nat -> Nat)->(Nat -> Nat). There are two operators on functions, given in the following table.

So, a function that multiplies two numbers, can be written as lambda n:Pos.lambda m:Pos.n*m. Note that the shorter lambda n,m:Pos.n*m is also allowed.

Functions are very useful to represent arrays. An array in which natural numbers can be stored is

sort Array = Nat -> Nat;

Getting the i-th element of an array f:Array is done by f(i), i.e. via ordinary function application. It is possible to define operations on an array as follows (see user defined sorts and mappings below). For instance the update function update(i,m,f) that sets value m at position i in array f is defined by:

map update: Nat # Nat # Array -> Array;
 
var i, n: Nat;
    f: Array;
eqn update(i,n,f) = lambda j:Nat . if(i==j, n, f(j));

Sets and bags

There are two more data types namely sets and bags. Sets and bags are common mathematical notions, and variants of lists, as they are often encountered in other specification languages. The types of sets and bags over a type A are declared by Set(A) and Bag(A). Sets can be denoted by explicit enumeration, e.g. {1,3,5,8} or by set comprehension. A typical example of a set is the set of all prime numbers, which can be written as

Bags are denoted by explicitly indicating the multiplicity of the elements. E.g. {a:1,b:2,c:3} is the set with one a, two b's and three c's. The bag where each positive number n occurs n+1 times, is denoted as:

Operators on sets are given by the following table.

Structured types

Structured types are types that are typically used in functional programming languages. Usually, a number of constructors and destructors is defined for terms with a very particular shape.

A well known and illustrative example 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 a term of the form leaf(a) where a is a term of sort A, or a tree is a term of the form node(t1,t2) where t1 and t2 are terms of sort Tree.

The functions leaf and node are called the constructors of sort Tree. Two terms consisting of constructors of a structured sort are equal if and only if they are syntactically equal.

By adding some more information to the struct declaration, projection and recognizer functions are generated automatically:

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

declares a sort Tree where is_leaf(t) is true if t is of the shape leaf(a) and is_node(t) is true if t has the shape node(t1,t2). These functions are called recognizers. The functions val, left and right are projection functions. On a tree of the shape leaf(a) the expression val(t) yields a. The functions left and right give the left and right subtree of a node.

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

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

A last 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.

User defined sorts and mappings

Besides using standard types and type constructors, there is a very direct way to define user defined sorts with a set of constructors and mappings. Internally, all standard types are defined in terms of these primitives.

Sorts can be declared by simply stating their existence:

sort D;

A sort represents a set of elements that cannot be empty. There is no limit on the number of elements a sort can represent. It can be finite, but also countably or uncountably infinite.

Sorts can be derived from other sorts. By writing

sort E = D;

sort E becomes equal to sort D.

It is possible to define constructors for a sort NAT as in the following example where the natural numbers are defined as done in Peano arithmetic (and which is not the way the predefined sort Nat is defined internally in mCRL2, because it is far too inefficient):

sort NAT;
cons zero: NAT;
     successor: NAT -> NAT;

If for some sort D there is a constructor with target sort D, we call the sort D a constructor sort. This implies that all terms of sort D can be written as the application of a constructor to subterms. In case of the sort NAT above, this subterm also consists of the application of a constructor. So, each element of sort NAT can be written as successor(successor(...successor(0)...)).

It is not possible that for some sort D there is only one constructor of the form

cons f: D -> D;

This implies that all terms consists of an unbounded sequence of applications of f, but this is not a proper term. Hence, no term with constructors can be made. So, as all elements of sort D should be equal to this non existing term, the domain D must be empty. But this is in contradiction with the fact that domains should at least contain one element. If a sort has no constructors, it can contain elements that can not be expressed by terms. Constructor domains always have at most a countably infinite number of elements. Non constructor sorts can have many more. Hence, the domain of real numbers can only be defined without constructors.

Besides constructors, auxiliary functions, generally called mappings, can be defined. For instance the definition of plus on the sort NAT can be declared as follows:

map plus: NAT # NAT -> NAT;

As plus is not a constructor, we know that each term of the form plus(t,u) can be written using constructors successor and zero only. We can use equations to make this relation explicit. Data types that are defined using constructors, mappings and equations are generally called equational abstract data types. The defining equations for plus are:

var n,m: NAT;
eqn plus(n,zero) = n;
    plus(n,succesor(m)) = succesor(plus(n,m));

Using the keyword var the variables are declared that are used in the equation section immediately following the declaration.

The mechanism using map and equations is also very useful to define functions on built in data types. For instance defining a mapping count that counts the number of elements in a Tree as defined above, can be done as follows:

var a: A, t,t': Tree;
eqn count(leaf(a)) = 1;
    count(node(t,t')) = count(t) + count(t');

The equations can also have conditions. For instance a successor function S on natural numbers that provides successors modulo some number N is written by:

eqn n <  N -> S(n) = n + 1;
    n == N -> S(n) = 1;

The condition is written before an implication arrow.

The formal interpretation of equations is that terms are equal if they can be proven equal using the equations and standard equational reasoning. Furthermore, terms are not equal if assuming that they are equal leads to the conclusion that true equals false by equational reasoning.

However, the tools generally use term rewriting as the technique to reason with the equations. This means that the left hand side of the equation is matched to a subterm and it is replaced by its right hand side, provided the condition of the equation evaluates to true. In order for this to work smoothly, there is a requirement that variables occurring in the condition or right hand side of the equation must also occur in the left hand side.

The mCRL2 toolset contains two innermost and two just-in-time (jitty) rewrite strategies. The innermost rewriters apply the rewrite rules depth first on a term. It rewrites this subterm first to normal form, which is a term to which no further rewrite rule can be applied. This has the disadvantage that unnecessary rewriting is done. For example, in if(b,t1,t2) first t1 and t2 are rewritten, and depending on whether b is true or false only one of these is selected. A better strategy is to first rewrite b, and based on its value to determine whether t1 or t2 must be rewritten. This is what the jitty rewriter does.

For both rewriters there is a compiling version that translates the rewrite rules to C code, which is subsequently compiled and dynamically loaded in the main programme. The performance of the compiling rewriter is much better than that of the interpreting rewriters, and its use is strongly recommended for tasks which are rewriting intensive, such as the generation of a state space. Unfortunately, due to the lack of standard compilers, the compiling rewriters are not available on the Windows platform. This is also the reason that the compiling rewriters are not the default in the tools.

Because equations are dealt with as rewrite rules, there is a pitfall. The left hand side of an equation is matched on a term. However, the matching only works if the term has the same shape as the left hand side of the equation. So, writing a count function on Tree as done above is ok, because trees in normal form have as main function symbols either leaf or node. However, with natural numbers, a compact and very effective internal representation is used, which causes the following to go astray:

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

The terms Fib(1), Fib(2), etc. will not be rewritten, because the internal representation of 1 is different from the 1 in the equation. Hence, they do not match. More fundamental is that 2 in no way has the shape n+2 and no matching will take place here either. The solution for this is to avoid pattern matching in the left hand side, if there is uncertainty about the shape of the normal forms of terms. In the concrete case above, it is strongly recommended to write:

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

Note that subtraction of two natural numbers yields an integer. In order to get the types right, a conversion function Int2Nat is required.

Processes with data

There are three ways to use data in processes: adding arguments to process variables and actions, using conditions, and using the sum operator.

Adding arguments to processes and actions

Processes can carry zero or more data parameters. For instance a clock that counts its ticks can be specified as follows:

act tick;
 
proc Clock(n: Nat) = tick . Clock(n + 1);
 
init Clock(0);

Also actions can have one or more arguments. So, we can extend the clock by showing the current time.

act tick;
    show: Nat;
 
proc Clock(n:Nat) = tick.Clock(n + 1)
                  + show(n) . Clock(n);
 
init Clock(0);

Conditions

We can let data influence the course of events by adding conditions to the process. We write c -> p for "if c then do process p" and c -> p <> q for "if c then p else q". For instance, the clock above can be forced to count modulo 100, and it may only be reset if n is smaller than 50.

act tick, reset;
 
proc Clock(n: Nat) = (n < 99) -> tick . Clock(n + 1) <> tick.Clock(0)
                   + (n < 50) -> reset . Clock(0);
 
init Clock(0);

Sum operators

The sum operator allows to formulate the choice between a possibly infinite number of processes in a very concise way. In other formalisms, and in semi-formal texts, the sum operator is often written using the choice operator.

The process sum n: Nat . p(n) can be seen as a shorthand for p(0) + p(1) + p(2) + .... The use of the sum operator is often to indicate that some value must be read, i.e. the process wants to read either a 0 or a 1 or a 2, etc. So, a buffer that reads some natural number and subsequently delivers it again can be compactly specified by:

act read, write: Nat;
 
proc Buffer = sum n: Nat. read(n) . write(n) . Buffer;
 
init Buffer;

Looking at the example of the clock, the clock can be set to a particular time using a sum operator and a set action:

act tick;
    set: Nat;
 
proc Clock(n: Nat) = tick . Clock(n + 1)
                   + sum m: Nat. set(m) . Clock(m);
 
init Clock(0);

If sum operators are used over infinite domains, such as Nat, then it is not possible to simulate these, or generate a state space. This for instance holds for the clock with the set action. In general, however, sums over infinite domains are used to read data from other processes. This is proper, and even encouraged, use of the mCRL2 toolset. All tools are optimised to deal with such situations. In general no enumeration of data elements takes place in such a situation.

There are situations where sums over infinite domains can be used safely for simulation or state space generation. For instance when there are conditions that restrict the domain. A typical example is the following:

act show: Nat;
 
proc P = sum n: Nat. (n < 10) -> show(n) . P;
 
init P;

Here the variable in the sum operator is restricted by a condition. Using the constructors of the data domain Nat the tools will figure out that only the finite set of numbers under 10 are relevant. This does not only work for natural numbers, but for any constructor sort.

Note that when using the toolset symbolically (e.g. by symbolically solving modal formulas, proving invariants, or calculating confluence) there is no finiteness constraint at all on the sum operators.

Parallel processes, communication and components

Up till now, we have only addressed simple, sequential processes. In this section we explain how to put these processes in parallel, and how to model the communication between the processes.

Putting processes in parallel

Processes can be put in parallel using the parallel operator. E.g. if p and q are processes, the expression

p || q

are the processes p and q executing in parallel. More precisely, the actions of p and q are executed in an interleaved fashion.

For example consider the process a || b. This process is equal to the following, where the actions a and b are not only interleaved, as there is also a multi-action where a and b happen simultaneously.

a.b + b.a + a|b

Note that parallel behaviour can easily become quite complex. For instance the simple looking parallel process a.b || c.d is equal to the sequential process:

a.(b.c.d+c.(b.d+d.b+b|d)+(b|c).d)) + c.(a.(b.c+c.b+b|c)+c.a.b+(a|c).b) + (a|b).(c.d+d.c+c|d)

One of the major reasons why the analysis of behaviour is complex, lies in exactly this explosion of possibilities of parallel processes. It is virtually impossible to imagine all possible interleavings of actions.

The current implementation of the linearization procedure in mcrl22lps does not support recursive paralellism, e.g. processes like

X=a.(X||X)

cannot be handled. The same holds for the allow, block, hide and communication operators that can not be used within recursive processes.

However, it is possible to use recursive parallelism for for the definition of the parallel composition of n similar processes to compactly denote

P(1)||P(2)||...||P(n)

In order to describe processes of the form:

<nP>(p:Pos,...) = (p>1) -> <P>([p],...)||<nP>(Int2Pos(p-1),...) <> <P>([1],...)

are process names parameterized by Pos, [.] means an optional parameter and ... means any parameters copied to the the rhs. All occurrences of <nP> should be of the form <nP>(<m>,...), where <m>:->Pos is a map, and an equation <m>=<p> for some positive <p>. For example,

eqn m = 10;
 
map m: Pos;
 
proc P(p:Pos)=...
 
proc nP(p:Pos) =
       (p>1) -> P(p)||nP(Int2Pos(p-1))<>P(1);
 
init nP(m);

Is equivalent to

eqn m = 10;
 
map m: Pos;
 
proc P(p:Pos)=...
 
proc nP(p:Pos) = P(10)||P(9)||P(8)||P(7)||P(6)||P(5)||P(4)||P(3)||P(2)||P(1);
 
init nP(m);

The communication and the allow operator

We have seen in the previous section that parallel processes can have many interleavings, and some actions of parallel processes happen simultaneously. So, one process can do a send action and another reads, via a read action:

send || read  =  send.read + read.send + send|read

The intention is that send and read must happen at the same time (i.e. must communicate) and can not happen as single isolated actions. In order to achieve this there are two operators comm and allow.

The comm({a|b ->c}, p) operator says which multi-actions are renamed to a single action. It says that actions a and b must communicate to c in process p. Concretely, in any multi-action of p all occurrences of a|b are replaced by c, provided that the data that a and b carry, match.

The allow({c},p) operator says that besides the empty multi-action tau, only multi-actions consisting of a single c are allowed in p. All other actions are blocked. The allow operator can also permit multi-actions to happen, as in allow({a|b,c|d},p). In such a case the arguments of the allowed multi-actions can differ.

The following expression enforces the desired communication in the example with read and write:

allow({c},comm({send|read->c},send||read))

Transfering data can be done easily in this scheme. So, assume one process sends a natural number n, which is read and processed by another process. This could be specified by:

allow({c},comm({send|read->c}, send(n).p || sum m:Nat.read(m).q(m) ))\

Here, q(m) is the process that uses the value m. The process above actually behaves as

c(n).allow({c},comm({send|read->c}, p || q(n) ))

or in other words, the communication took place and the value n is neatly handed over to q.

More components can be put in parallel. As a larger example we show how the four components of the alternating bit protocol are assembled together. The process S(true) is the sending protocol entity with initial bit true. The process R(true) is the receiving entity, also with initial bit true. The processes K and L model unreliable channels. The actions r1 and s4 are external actions. Actions starting with a c are communications. The action i represents an internal action in the channels that determine whether data is lost or not.

proc allow({r1,s4,c2,c3,c5,c6,i},comm({r2|s2->c2, r3|s3->c3, r5|s5->c5, r6|s6->c6},
                      S(true) || K || L || R(true)));

The complete description of the alternating bit protocol can be found in the file abp.mcrl2 in the directory examples/academic in the distribution of the toolset.

There is a dual operator of the allow operator. This is the encapsulation or block operator that can block single actions. If a single action that is blocked occurs in a multi-action the whole multi-action is renamed to delta. E.g. the expression

block({b},a||b)

is equal to a.delta.

Renaming

A convenient operator that is not used very often is the renaming operator, which allows to rename action labels. E.g. rename({a->b,c->d},p) renames action a in p to b, and action c in p to d. The operator is useful if certain processes must be used several times in a system, and have different communication patterns each time.

Hiding internal behaviour

It is possible to hide actions, which means that they are not visible anymore in multi-actions. E.g. hide({a},a|b) equals b, as a is hidden. Using hiding it is possible to indicate that certain actions can no longer be observed by the outside world. For instance with the alternating bit protocol, it might be useful to indicate that the communications c2, c3, c5, c6 and the internal choice i are not visible. This is done as follows:

proc hide({c2,c3,c5,c6,i},
       allow({r1,s4,c2,c3,c5,c6,i},
         comm({r2|s2->c2, r3|s3->c3, r5|s5->c5, r6|s6->c6},
                     S(true) || K || L || R(true)));

It is important to use hide, allow and comm in this way. Changing the order of these operators will lead to partial hiding of multi-actions, which causes the number of summands in the linear process to grow. This makes analysis and simulation of the process behaviour much harder.

If hiding is applied, the process behaviour can be reduced modulo branching bisimulation. Under the assumption that empty multi-actions (i.e. taus) cannot be observed, the behaviour of a transition system becomes much smaller. For example for the alternating bit protocol the picture below on the left depicts the behaviour before branching bisimulation reduction is applied, and the picture on the right depicts the equivalent reduced behaviour.

Ltsgraph depicts the alternating bit protocol

The ABP modulo branching bisimulation

Time

Using the @ operator it can be expressed at which time an action can take place. In the process

a@1 . b@3 . c@8

we see three actions taking place at time instances 1, 3 and 8. The time labels are positive real numbers, meaning that we use absolute, dense time. If actions do not carry an explicit time, they can take place at any time instance.

Actually, the time operator applies to processes in general. The process p@t represents the process where the first action of p must take place at time t. If timing constraints conflict, e.g. in a@3@5, the process time deadlocks meaning that the time cannot proceed from a certain moment onwards. Although this cannot happen in reality, time deadlocks are a strong tool to investigate that all time constraints in a behavioural specification are consistent. A time deadlock is written as delta@t. More concretely, the process above is equal to delta@3.

Although labelling an action with time is rather straightforward, it is a very versatile tool in the context of conditions and sum operators. For instance, a clock that ticks every second is specified by

Clock(t: Real) = tick@(t+1) . Clock(t+1);

We can make a drifting clock as follows (where epsilon is some small constant):

Clock(t: Real) = sum u: Real. (1-epsilon <= u && u <= 1+epsilon) -> tick@(t+u).Clock(t+u);

A timeout can be specified in much the same way. If the action water must follow within five time units after the action fire this is specified by the following expression

... sum t: Real. fire@t . sum u: Real. (u<=5) -> water@(t+u) ...

Processes with time can be linearised and using the lpsuntime tool time annotation can be removed (preserving the time induced orders on processes). Also checking timed modal formulas is possible. Due to the fact that time ranges over real numbers, it is generally not possible to simulate processes that use explicit time, or to generate their state space.

Linear processes

Within the toolset linear processes play a pivotal role. A linear process is a single process equation with a very simple basic structure. It does not contain parallelism, communication or visibility operators. As such it is a good basic form to base tools upon.

Before being able to do anything with it, any process is first translated to linear form. All subsequent manipulations operate on this linear form. There are tools that translate one linear process to another (e.g. lpsuntime), other tools that translate linear processes to labelled transition systems (lps2lts) and tools that operate directly on linear processes (such as the simulator xsim). In essence any process can be translated to linear form (although the lineariser mcrl22lps puts certain restrictions on its input). Moreover, in practice the resulting linear process is generally fairly small. Translating a parallel process to a linear process is never the bottleneck in the analysis of a system.

The left-hand side of a linear process equation is one single process variable (often P or X) with a number of process parameters. The right hand side of the equation consists of a sequence of summands which contain one sum operator, possibly with zero or more variables, one condition, one action and one invocation of the process P again. The parameters of the process constitute the possible states of the system. The condition indicates whether the action can be done in this particular state, and the invocation indicates the state change. When it comes to process analysis, this summand form occurs in many disguises. It for instance lives under the name condition-action-effect rule.

The specification of a buffer:

proc Buffer = sum m:Nat.read(m).send(m).Buffer;
init Buffer;

is not linear, because there are two actions before the recursive invocation of Buffer. The linear process of a buffer must introduce a boolean b to indicate whether the action read was done. Note that for simple processes, the linear variants are easy to read. For more complex processes this is generally not the case.

proc Buffer(b: Bool, n: Nat) = sum m: Nat. b -> read(m).Buffer(!b,m)
                             + !b -> send(n).Buffer(!b,n);
init Buffer(true,0);

It is possible to linearise processes using the tool mcrl22lps (mCRL2 to Linear Process Specification). The resulting linear process can be inspected using lpspp (Linear Process Specification Pretty Printer). In the recursive invocation, only the variables that are changed are listed. This is because for complex parallel systems the number of parameters of a linear process may be huge, whereas most of the parameters do not change. In a complete parameter list it is very hard to see what is happening.

At some places in a linear process, the values of some process variables are not really relevant. For this purpose free variables are introduced. The meaning of free variables in a linear process is that the behaviour of the linear process, starting in its start state is always the same for any choice of values for the free variables. This allows tools such as lpsconstelm that finds and removes constant process parameters, to choose optimal values for these free variables to remove as many constants as possible. Actually, in the Buffer above, the value of n is irrelevant after the send(n) action. This will be observed during linearisation, and the result will look like:

var freevar:Nat;
proc Buffer(b: Bool, n: Nat) = sum m: Nat. b -> read(m).Buffer(!b,m)
                             + !b -> send(n).Buffer(!b,freevar);
init Buffer(true,0);

For timed processes, a timed tag can be added to the actions during linearisation. Moreover, timed deadlock summands delta@t can show up, indicating that in the linear process time may proceed up till time t.

The main analysis tools

The tools from the toolset can be used using squadt or via the command prompt. All tools have a --help option to compactly explain the options of the tool. On the tool manual pages, many more tools are documented than mentioned below.

The most important tool is the lineariser:

mcrl22lps -v input.mcrl2 output.lps

Using lpsinfo information about output.lps can be obtained. Using lpspp the linear process can be printed in a human readable format. The resulting linear process can be simulated using xsim:

xsim output.lps

Generating a state space can be done by lps2lts:

lps2lts -v output.lps output.svc

The tool ltsinfo provides info and the tool ltsconvert can translate the .svc file to various other formats, while applying various reductions. Translating the .svc file to an .aut file while in the meantime applying a branching bisimulation reduction is done by:

ltsconvert -b output.svc output.aut

The tool ltsgraph can be used to visualize the resulting state space as a graph, provided it is sufficiently small.

ltsgraph output.aut

See also

The tool limitations page lists known limitations of the mCRL2 tools compared to the language.