**Contribution of this section**

- use of standard data types, and
- use of simulator.

**New tools**:
lpsxsim.

Two water cans of known capacity, say of `x`

and of `y`

liters, a tap
and a sink are at our disposal. The cans do not have a graduation to
measure their content. The challenge is to pace an exact volume of
water, say of `z`

liter, in one of the cans.

Given the description, there are basically four things one can do with a can:

- to empty the can in the sink, which makes only sense if the can is non-empty;
- to fill the can completely from the tap, a proper thing to do for a can that is not full already
- to pour from the can into the other, provided there is water in the can;
- to fill the can by pouring from the other can, assuming the first is not brimful yet.

So, somehow we need to keep track of the actual content of the water cans, to see if an empty-to-sink action or an pour-to-other action can be done with the can, or that a fill-from-tap action or a fill-from-other action applies.

Processes in mCRL2 may carry one or more parameters. We can
write, for example, `BigCan(3)`

to express that the bigger of
the two watercans contains `3`

liter. In the process definition we need
to declare the parameter, e.g. we write `BigCan(m: Nat) = ...`

to have for `BigCan`

the variable `m`

ranging over the
naturals (including `0`

).

Similary, actions can have parameters. Here, we have occasion to
express that `l`

liters of waters have been poured out. If the
action `lose`

denotes the pouring out, we do this by writing
`lose(l)`

. In the definition of the action `lose`

we need to indicate the parameter, e.g. by writing `lose: Nat`

in the `act`

part of the mCRL2 specification. Thus,
`l`

ranges over non-negative integer values.

For the concrete case of cans of `5`

and `8`

liter to yield `4`

liters, a
first approximation may be as follows (available as
`watercan1.mcrl2`

):

```
act
empty, fill, done;
lose, gain, pour: Nat;
proc
BigCan(m:Nat) =
( m != 4 ) -> (
% some code for the big can
) <> done ;
SmallCan(m:Nat) =
( m != 4 ) -> (
% some code for the small can
) <> done ;
init
allow(
{ empty, fill, pour },
comm(
{ lose|gain -> pour },
BigCan(0) || SmallCan(0)
));
```

In this set-up, a `lose`

action by the one can will synchronize
with a `gain`

action by the other can, together synchronizing
as a `pour`

action. The three actions all carry a parameter of
type `Nat`

, that needs to be equal for synchronization to
succeed.

Another choice made above is the test whether the current content of
the required volume to pace. If no, we do some activity left
unspecified here, if yes we do the action `done`

. The general
form of the if-then-else construction in mCRL2 is `c -> p <> q`

for condition `c`

and processes `p`

and `q`

.

One may wonder in what way the specification for the `BigCan`

process will
differ from that for the `SmallCan`

. It seems more appealling to make the
capacity of the can a parameter too. An incomplete specification of a solution
of the watercan problem is the following (also available as
`watercan2.mcrl2`

). The term `Can(n,m)`

indicates that a can of capacity `n`

is currently holding a volume of `m`

.

```
act
empty, fill, done;
lose, gain, pour: Nat ;
proc
Can(n:Nat,m:Nat) =
( m != 4 ) -> (
%% empty, if non-empty
(m > 0) -> ( empty . Can(n,0) ) +
%% fill, if not full
(m < n) -> ( fill . Can(n,n) ) +
%% pour to other if not empty
(m > 0) -> (
sum l:Nat . (
( (0 < l) && (l <= m) ) -> (
lose(l) . Can(n,Int2Nat(m-l)) ) ) ) +
%% pour from other if not full
(m < n) -> (
sum l:Nat . (
( (0 < l) && (l <= n-m) ) -> (
gain(l) . Can(n,m+l) ) ) )
) <> done ;
init
allow(
{ empty, fill, done, pour },
comm(
{ lose|gain -> pour },
Can(5,0) || Can(8,0)
) ) ;
```

Warning

The default options of mcrl22lps lead to an infinite loop when linearising this specification. The tools warns about this issue through the following output:

```
$ mcrl22lps watercan2.mcrl2 | lps2lts
[16:05:05.505 warning] generated 100 new internal processes. A possible unbounded loop can be avoided by using `regular2' or `stack' as linearisation method.
[16:05:07.994 warning] generated 500 new internal processes. A possible unbounded loop can be avoided by using `regular2' or `stack' as linearisation method.
```

As the tool indicates, this can be overcome by using an alternative
linearisation strategy, by passing the option `lregular2`

to mcrl22lps. This issue is caused by the possibility
of successful termination in case the `done`

action is performed.

An LTS generated by mcrl22lps and lps2lts has 72 states and 335 transitions:

```
$ mcrl22lps -lregular2 watercan2.mcrl2 | lps2lts -v
...
[15:53:12.299 verbose] done with state space generation (6 levels, 73 states and 335 transitions)
```

Note

Currently, the size of the state space is not printed when the `-v`

flag is not passed to the tool.

It is possible to do the `done`

action. This is confirmed by model checking
the following µ-calculus formula (available as
`watercan2.mcf`

).

```
% The done action can be reached
<true*.done> true
```

The commands for this verification can be summarised as:

```
$ mcrl22lps -lregular2 watercan2.mcrl2 | lps2pbes -f watercan2.mcf | pbes2bool
true
```

We can get some more feedback on what is going on by using the
simulator lpsxsim with which we can step through the LTS and
follow the the values of parameters. Calling at the command line the
lpsxsim tool with the linear process
`watercan2.lps`

, produced by the mcrl22lps tool from
the mCRL2-specification `watercan2.mcrl2`

,
by typing:

```
$ lpsxsim watercan2.lps
```

opens an application with two smaller windows, the top one listing possible transitions, the bottom one listing the values of the parameters in the current state. Parameters have symbolic names as a result of the linearization process. It looks similar to

Transitions ActionState Change`fill`

`s31_Can1 := 2, m_Can11 := 8;`

`fill`

`s3_Can1 :=2, m_Can1 := 5;`

Current stateParameterValue`s3_Can1`

1 `n_Can1`

5 `m_Can1`

0 `s31_Can1`

1 `n_Can11`

8 `m_Can11`

0

By double clicking on a transition, the transition can be taken. For
example, clicking on the top `fill`

transition yields a new
list of transitions and an update current state. Now, besides a
`fill`

action also the actions `empty`

, `pour(1)`

to `pour(5)`

are possible. The state now holds, e.g., the
value``8`` for the contents `m_Can11`

for the bigger
can, as a result of the `fill`

action.

The simulator reveals that we have made a mistake. Given a full can of 8 liter and an empty can of 5, the only volume we can pour from the bigger can into the smaller can is the volume of 5 liters, as no measure is available on the cans. Our specification, however, allows for all volumes from 1 upto 5 liters. Pacing 4 liters would then be easy, just pour 4 liters into the smaller can.

We can restrict the possible volumes that are poured over, by noting that either (i) the complete content of a can is poured into the other provided the latter can can hold, (ii) an amount of water is poured from a can into the other such that the other can is brimful. Hence, the minimum of the content of the from-can and the remaining capacity of the to-can determines the amount of water that is going from the one can to the other by pouring.

The basic idea then is to distinguish between an action
`lose_all`

and an action `lose_some`

for pouring into
the other can, and between an action `gain_all`

and
`gain_some`

for getting from the other can. These actions will
have a parameter for the amount of water involved. An action
`lose_all(m)`

synchronizes with the action
`gain_some(m)`

, with `m`

liters in the first can; the
action `lose_some(n-m)`

matches the action
`gain_all(n-m)`

, now with `n`

liters and
`m`

liters as capacity and current content of the second can,
respectively. As synchronization function we will then have
`lose_all | gain_some -> pour`

as well as
`lose_some | gain_all -> pour`

. So, `pour`

actions can be the result of
two pairings of actions, `lose_all`

with `gain_some`

and `lose_some`

with `gain_all`

. This process is described in the following
specification (also available as `watercan3.mcrl2`

).

```
sort
Name = struct A | B ;
act
empty, fill, done: Name ;
lose_all, gain_some, lose_some, gain_all, pour: Name # Name # Nat ;
map
sizeA, sizeB, target: Nat;
eqn
sizeA = 5;
sizeB = 8;
target = 4;
proc
Can(N:Name,n:Nat,m:Nat) =
( m != target ) -> (
%% empty, if non-empty
(m > 0) -> ( empty(N) . Can(N,n,0) ) +
%% fill, if not full
(m < n) -> ( fill(N) . Can(N,n,n) ) +
%% pour all to other if not empty
(m > 0) -> (
sum M:Name . (
lose_all(N,M,m) . Can(N,n,0) ) ) +
%% pour some to other if not empty
(m > 0) -> (
sum l:Nat,M:Name . (
( (0 < l) && (l <= m) ) -> (
lose_some(N,M,l) . Can(N,n,Int2Nat(m-l)) ) ) ) +
%% pour all from other if not full
(m < n) -> (
sum M:Name . (
gain_all(M,N,Int2Nat(n-m)) . Can(N,n,n) ) ) +
%% pour some from other if not full
(m < n) -> (
sum l:Nat,M:Name . (
( (0 < l) && (l <= Int2Nat(n-m)) ) -> (
gain_some(M,N,l) . Can(N,n,m+l) ) ) )
) <> done(N) ;
init
allow(
{ empty, fill, done, pour },
comm(
{ lose_all|gain_some -> pour, lose_some|gain_all -> pour },
Can(A,sizeA,0) || Can(B,sizeB,0)
));
```

In the specifcation above a further modification has been done.
The names `A`

and `B`

have been introduced for the cans. At
the start of the specification a new sort is introduced, viz. the
sort name. It is an enumeration sort, following the format

```
<sort name> = struct entity 1 | entity 2 | ... | entity k ;
```

Here we have two entities, the name `A`

and the name `B`

, hence `k`

equals
2. The new actions have been added, but also they can carry the name or names of
cans involved. E.g., the action `empty(A)`

indicates that can `A`

has been
emptied, `done(B)`

indicates that the target value has been left in can `B`

,
whereas `lose_all(B,A,3)`

represent that all of the current content of can
`B`

, apparently 3 liters, will be poured into can `A`

. Therefore, the sort
of the actions `empty`

and `done`

is `Name`

, as they take a name as
parameter, the sort of the action `lose_all`

is `Name # Name # Nat`

as the
actions takes two names and a natural number as parameter. The summations in the
mCRL2 specification, now quantify over the name of the other can, called `M`

,
and exclude to pour from the can in itself by demanding `M != N`

.

We also have occasion to introduce constants. The is a specific use of the
facilities of mCRL2 in supporting abstract data types. Here, after the keyword
`map`

we introduce three constants over the natural numbers, called `sizeA`

,
`sizeB`

and `target`

. Next, following the keyword `eqn`

, we define them to
hold the values `5`

, `8`

and `4`

, respectively. The corresponding LTS has
35 states and 108 transitions. This number is obtained by the following command:

```
$ mcrl22lps -lregular2 watercan3.mcrl2 | lps2lts -v
...
[16:18:13.877 verbose] done with state space generation (15 levels, 35 states and 108 transitions)
```

The LTS of a smaller example, can sizes 4 and 3
and target volume 2 (available as `watercan3-small.mcrl2`

)
has 18 states and 46 transitions after reduction modulo strong bisimulation.
This information was obtained using the following commands:

```
$ mcrl22lps -lregular2 watercan3-small.mcrl2 watercan3-small.lps
$ lps2lts watercan3-small.lps watercan3-small.lts
$ ltsconvert -ebisim watercan3.lts watercan3.bisim.lts
$ ltsinfo watercan3.bisim.lts
Number of states: 18
Number of state labels: 0
Number of action labels: 11
Number of transitions: 46
Does not have state labels.
Has action labels.
LTS is deterministic.
```

You can open the state space in ltsgraph if you want to study it:

```
$ ltsgraph watercan3.bisim.lts
```

If you want to verify that one of the cans can eventually perform a `done`

action, you need to modify the modal formula to include a parameter.

Exercise

Modify the µ-calculus formula in `watercan2.mcf`

such that the formula holds if a `done(N)`

action is reachable for some
name `N`

. Verify that the property holds for `watercan3.mcrl2`

.

Solution

The following formula (available as `watercan3.mcf`

)
describes this property.

```
% The done action can be reached
exists N: Name . <true*.done(N)> true
```

It can be verified to hold for the specification using:

```
$ mcrl22lps -lregular2 watercan3.mcrl2 | lps2pbes -f watercan3.mcf | pbes2bool
true
```