Water cans
----------

**Contribution of this section**

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

**New tools**:
:ref:`tool-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
:download:`watercan1.mcrl2 <files/watercan1.mcrl2>`):

.. literalinclude:: files/watercan1.mcrl2
   :language: mcrl2

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
:download:`watercan2.mcrl2 <files/watercan2.mcrl2>`). The term ``Can(n,m)``
indicates that a can of capacity ``n`` is currently holding a volume of ``m``.

.. literalinclude:: files/watercan2.mcrl2
   :language: mcrl2

.. warning::

   The default options of :ref:`tool-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 :ref:`tool-mcrl22lps`. This issue is caused by the possibility
   of successful termination in case the ``done`` action is performed.

An LTS generated by :ref:`tool-mcrl22lps` and :ref:`tool-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)
   
.. this said 46 states and 265 transitions in an earlier version (JK).

.. 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
:download:`watercan2.mcf <files/watercan2.mcf>`).

.. literalinclude:: files/watercan2.mcf
   :language: mcrl2
   
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 :ref:`tool-lpsxsim` with which we can step through the LTS and
follow the the values of parameters. Calling at the command line the
:ref:`tool-lpsxsim` tool with the linear process 
:file:`watercan2.lps`, produced by the :ref:`tool-mcrl22lps` tool from
the mCRL2-specification :download:`watercan2.mcrl2 <files/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 :download:`watercan3.mcrl2 <files/watercan3.mcrl2>`).

.. literalinclude:: files/watercan3.mcrl2
   :language: mcrl2

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

.. code-block:: mcrl2

  <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 :download:`watercan3-small.mcrl2 <files/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 :ref:`tool-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.

.. admonition:: Exercise

   Modify the µ-calculus formula in :download:`watercan2.mcf <files/watercan2.mcf>`
   such that the formula holds if a ``done(N)`` action is reachable for some
   name ``N``. Verify that the property holds for :file:`watercan3.mcrl2`.
   
.. admonition:: Solution
   :class: collapse
   
   The following formula (available as :download:`watercan3.mcf <files/watercan3.mcf>`)
   describes this property.
   
   .. literalinclude:: files/watercan3.mcf
      :language: mcrl2

   It can be verified to hold for the specification using::
   
     $ mcrl22lps -lregular2 watercan3.mcrl2 | lps2pbes -f watercan3.mcf | pbes2bool
     true