A Vending Machine
Contribution of this section
specifying processes,
linearisation,
state space exploration,
visualisation of state spaces,
comparison/reduction using behavioural equivalences, and
verification of modal mucalculus properties.
New tools: mcrl22lps, lps2lts, ltsgraph, ltscompare, ltsconvert, lps2pbes, pbes2bool.
Our first little step consists of number of variations on the good old
vending machine, a user User
interacting with a machine Mach
. By
way of this example we will encounter the basic ingredients of
mCRL2. In the first variation of the vending machine, a very
primitive machine and user, are specified. Some properties are
verified. In the second variation nondeterminism is considered and,
additionally, some visualization and comparison tools from the toolset
are illustrated. The third variation comes closer to a rudimentary
prototype specification.
First variation
After inserting a coin of 10 cents, the user can push the button for an apple. An apple will then be put in the drawer of the machine. See Figure Vending machine 1.
Vending machine 1 can be specified by the following mCRL2, also
included in the file vm01.mcrl2
.
act
ins10, optA, acc10, putA, coin, ready ;
proc
User = ins10 . optA . User ;
Mach = acc10 . putA . Mach ;
init
allow(
{ coin, ready },
comm(
{ ins10acc10 > coin, optAputA > ready },
User  Mach
) ) ;
The specification is split in three sections:
act
, a declaration of actions of 6 actions,proc
, the definition of 2 processes, andinit
, the initialization of the system.
The process User
is recursively defined as doing an ins10
action, followed by an optA
action, followed by the process User
again. The process Mach
is similar, looping on the action acc10
followed by the action putA
. Note, only four actions are used in
the definition of the processes. In particular, the action coin
and
ready
are not referred to.
The initialization of the system has a typical form. A number of
parallel processes, in the context of a communication function, with a
limited set of actions allowed. So, 
is the parallel
operator, in this case putting the processes User
and Mach
in
parallel. The communication function is the first argument of the
comm
operator. Here, we have that synchronization of an
ins10
action and an acc10
action yields the action coin
,
whereas synchronization of optA
and putA
yields ready
. The
actions of the system that are allowed, are mentioned in the first
argument of the allow operator allow
. Thus, for our first
system only coin
and ready
are allowed actions.
We compile the specification in the file vm01.mcrl2
to a socalled linear process, saved in the file vm01.lps
. This
can be achieved by running:
$ mcrl22lps vm01.mcrl2 vm01.lps
on the command line. The linear process is the internal representation
format of mCRL2, and is not meant for human inspection. However, from
vm01.lps
a labeled transition system, LTS for short, can be
obtained by running:
$ lps2lts vm01.lps vm01.lts
which can be viewed by the ltsgraph facility, by typing:
$ ltsgraph vm01.lts
at the prompt. Some manual beautifying yields the picture in Figure LTS of vending machine 1.
Apparently, starting from state 0 the system shuttles between state
0 and 1 alternating the actions coin
and ready
. Enforced by
the allow operator, unmatched ins10
, acc10
,
optA
and putA
actions are excluded. The actions synchronize
pairwise, ins10
with acc10
, optA
with putA
, to produce
coin
and ready
, respectively.
As a first illustration of model checking in mCRL2, we consider some
simple properties to be checked against the
specification vm01.mcrl2
. Given the LTS of the
system, the properties obviously hold.

% always, eventually a ready is possible (true) [ true* ] < true* . ready > true
In this property,
[true*]
represents all finite sequences of actions starting from the initial state.<true*.ready>
expresses the existence of a sequence of actions ending with the actionready
. The last occurence oftrue
in this property is a logical formula to be evaluated in the current state. Thus, if the property is satisfied by the system, then after any finite sequence of actions,[true*]
, the system can continue with some finite sequence of actions ending withready
,<true*.ready>
, and reaches a state in which the formulatrue
holds. Sincetrue
always holds, this property states that a nextready
is always possible. 
% a ready is always possible (false) [ true* ] < ready > true
This property is less liberal than property (a). Here,
<ready> true
requires aready
action to be possible for the system, after any finite sequence,[true*]
. This property does not hold. Aready
action is not immediately followed by aready
action again. Also,ready
is not possible in the initial state. 
% after every ready only a coin follows (true) [ true* . ready . !coin ] false
This property uses the complement construct.
!coin
are all actions different fromcoin
. So, any sequence of actions withready
as its one but final action and ending with an action different fromcoin
, leads to a state wherefalse
holds. Since no such state exists, there are no path of the formtrue*.ready.!coin
. Thus, after anyready
action, any action that follows, if any, will becoin
. 
% any ready is followed by a coin and another ready (true) [ true* . ready . !coin ] false && [ true* . ready . true . !ready ] false
This property is a further variation involving conjunction
&&
.
Model checking with mCRL2 is done by constructing a socalled
parameterised boolean equation system or PBES from a linear process
specification and a modal \(\mu\)calculus formula. For example, to
verify property (a) above, we call the lps2pbes
tool. Assuming property (a) to be in file vm01a.mcf
, running:
$ lps2pbes vm01.lps f vm01a.mcf vm01a.pbes
creates from the system in linear format and the formula in the file
vm01.mcrl2
right after the f
switch, a PBES
in the file vm01a.pbes
. On calling the PBES solver on
vm01a.pbes
:
$ pbes2bool vm01a.pbes
the mCRL2 tool answers:
true
So, for vending machine 1 it holds that action ready
is always
possible in the future. Instead of making separate steps explicity,
the verification can also be captured by a single, pipeline command:
$ mcrl22lps vm01.mcrl2  lps2pbes f vm01a.mcf  pbes2bool
Running the other properties yields the expected results. Properties (c) and (d) do hold, property (b) does not hold, as indicated by the following snippet:
$ mcrl22lps vm01.mcrl2  lps2pbes f vm01b.mcf  pbes2bool
false
$ mcrl22lps vm01.mcrl2  lps2pbes f vm01c.mcf  pbes2bool
true
$ mcrl22lps vm01.mcrl2  lps2pbes f vm01d.mcf  pbes2bool
true
Second variation
Next, we add a chocolate bar to the assortment of the vending machine. A chocolate bar costs 20 cents, an apple 10 cents. The machine will now accept coins of 10 and 20 cents. The scenarios allowed are (i) insertion of 10 cent and purchasing an apple, (ii) insertion of 10 cent twice or 20 cent once and purchasing a chocolate bar. Additionally, after insertion of money, the user can push the change button, after which the inserted money is returned. See Figure Vending machine 2.
Exercise
Extend the following mCRL2 specification (vm02holes.mcrl2
)
to describe the vending machine sketched above, and save the resulting
specification as vm02.mcrl2
. The actions that are involved,
and a possible specification of the Mach
process have been given.
The machine is required to perform a prod
action for administration
purposes.
act
ins10, ins20, acc10, acc20, coin10, coin20, ret10, ret20 ;
optA, optC, chg10, chg20, putA, putC, prod,
readyA, readyC, out10, out20 ;
proc
User =
*1*
Mach =
acc10.( putA.prod + acc10.( putC.prod + ret20 ) + ret10 ).Mach +
acc20.( putA.prod.ret10 + putC.prod + ret20 ).Mach ;
init
*2* ;
Linearise your specification using mcrl22lps, saving the LPS
as vm02.lps
.
Solution
A sample solution is available in vm02.mcrl2
.
This can be linearised using:
$ mcrl22lps vm02.mcrl2 vm02.lps
A visualization of the specified system can be obtained by first converting the linear process into a labeled transition system (in socalled SVCformat) by:
$ lps2lts vm02.lps vm02.lts
and next loading the SVC file vm02.lts
into the ltsgraph tool
by:
$ ltsgraph vm02.lts
The LTS can be beautified (a bit) using the start
button in the
optimization panel of the user interface. Manual manipulation by
dragging states is also possible. For small examples, increasing
the natural transition length may provide better results.
Exercise
Prove that your specification satisfies the following properties:
no three 10ct coins can be inserted in a row,
no chocolate after 10ct only, and
an apple only after 10ct, a chocolate after 20ct.
Solution
Each of the properties can be expressed as a µcalculus formula. Possible
solutions are given as vm02a.mcf
,
vm02b.mcf
, and
vm02c.mcf
.
Each of the properties can be checked using a combination of mcrl22lps, lps2pbes and pbes2bool. The following is a sample script that performs the verification:
$ mcrl22lps vm02.mcrl2 vm02.lps
$ lps2pbes vm02.lps f vm02a.mcf  pbes2bool
true
$ lps2pbes vm02.lps f vm02b.mcf  pbes2bool
true
$ lps2pbes vm02.lps f vm02c.mcf  pbes2bool
true
So the conclusion of the verification is that all three properties hold.
The file vm02taus.mcrl2
contains the
specification of a system performing coin10
and coin20
actions as well
as socalled \(\tau\)steps. Using the ltscompare tool you can
compare your model under branching bisimilarity with the LTS of the system
vm02taus
, after hiding the actions readyA
, readyC
, out10
,
out20
, prod
using the following command:
$ ltscompare ebranchingbisim tau=out10,out20,readyA,readyC,prod vm02.lts vm02taus.lts
Note
You first need to generate the state space of vm02taus.mcrl2
using mcrl22lps and lps2lts.
Using ltsconvert, the LTS for vm02.mcrl2
can be minimized
with respect to branching bisimulation after hiding the readies and returns:
$ ltsconvert ebranchingbisim tau=out10,out20,readyA,readyC,prod vm02.lts vm02min.lts
Exercise
Compare the LTSs vm02min.lts
and vm02taus.lts visually using
ltsgraph.
Third variation
A basic version of a vending machine with parametrized actions is available
in the file vm03basic.mcrl2
.
Exercise
Modify this specification such that all coins of denomination 50ct, 20ct, 10ct and 5ct can be inserted. The machine accumulates upto a total of 60 cents. If sufficient credit, an apple or chocolate bar is supplied after selection. Money is returned after pressing the change button.