Water cans

Contribution of this section

  1. use of standard data types, and
  2. 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
Action State Change
fill s31_Can1 := 2, m_Can11 := 8;
fill s3_Can1 :=2, m_Can1 := 5;
Current state
Parameter Value
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

Previous topic

A Vending Machine

Next topic

Towers of Hanoi