Towers of Hanoi
---------------
**Contribution of this section**
#. use of lists,
#. use of functions,
#. use of data µ-calculus formulae.
**New tools**:
:ref:`tool-mcrl2xi`.
The Towers of Hanoi is a classic mathematical puzzle that involves three pegs
(numbered 1, 2 and 3) and ```N >= 1`` discs. Every disc has a unique
diameter and has a hole in the center so that it can slide onto any of the pegs.
The discs are numbered 1 to ``N`` increasingly with their sizes. Initially,
all discs are stacked onto peg 1 in increasing size from top to bottom (see the
figure below where ``N = 6``). The puzzle is solved when all discs are on
peg 3 in the same order. Discs can be moved from one peg to any other, as long
as the following rules are obeyed:
#. Only one disc can be moved at a time.
#. Only the topmost disc on a peg can be moved.
#. A disc cannot be placed on top of a smaller disc.
.. image:: img/hanoi.*
:align: center
Over the next exercises we gradually construct an mCRL2 specification of the
Towers of Hanoi puzzle. For this, we shall specify a ``Peg`` process to
represent a peg and we shall use a list to represent the contents of a peg.
The list data structure is predefined in mCRL2. All elements in a list must be
of the same type. This type is determined by the list's type declaration, which
consists of the word ``List`` followed by the type of its elements between
parentheses. For example, a list ``l`` of natural numbers is declared by
``l:List(Nat)``. Lists can be explicitly enumerated, so that ``[]``, ``[1]``,
and ``[2,3,5]`` are all valid list expressions, representing the empty list, the
list with single element 1 and the list with elements 2, 3 and 5, respectively.
Furthermore, the following operations on lists are provided:
* cons ``|>``: insert an element at the front of a list, e.g. ``1 |> [2]`` gives
``[1,2]``;
* snoc ``<|``: insert an element at the back of a list, e.g. ``[2] <| 1`` gives
``[2,1]``;
* head: return the first element of a list, e.g. ``head([1,2])`` gives ``1``;
* tail: return a list without its first element, e.g. ``tail([1,2,3])`` gives
``[2,3]``.
Note that the head and tail of an empty list are undefined, so that mCRL2 will
not further reduce the terms ``head([])`` and ``tail([])``.
The mCRL2 language supports more operations on lists, but they are not used in
this section. For the complete overview consult the
:ref:`language reference `.
We shall use lists to represent stacks of discs, such that the head of the list
corresponds with the top of the stack. A disc is represented by a positive
natural number, which is an element of the predefined data sort ``Pos``.
Consider the following, incomplete data specification (available for download
as :download:`stack-holes.mcrl2 `:
.. literalinclude:: files/stack-holes.mcrl2
:language: mcrl2
This defines the ``Stack`` data sort as lists of positive numbers and declares
the functions (or *maps*) ``empty``, ``push``, ``pop`` and ``top`` as operations
on stacks. These functions have to be defined using equations, in which
variables can be used to represent any term of a certain type. For example, the
second equation defines ``push(x,s)`` for any positive number ``x`` and any
stack ``s``, where variables ``x`` and ``s`` have been declared above the
``eqn``-block. Equations can also have *guards* which limit the set of terms to
which that equation applies. For example, the last equation defines ``top(s)``
only for stacks ``s`` for which the guard ``!empty(s)`` holds, i.e. non-empty
stacks ``s``.
.. admonition:: Exercise
Complete the specification for the ``Stack`` data sort using the list
operations introduced above.
.. admonition:: Solution
:class: collapse
A possible solution to this exercise is the following (also available as
:download:`stack.mcrl2 `):
.. literalinclude:: files/stack.mcrl2
:language: mcrl2
Observe that in this solution a number of choices have been made. Every
stack operation is directly mapped onto a predefined function on lists. As
``pop`` is mapped to ``tail``, ``pop`` is not defined on the empty stack.
An alternative would have been the following set of equations for ``pop``:
.. code-block:: mcrl2
var s: Stack;
x: Pos;
eqn pop([]) = [];
pop(x |> s) = s;
This definition does allow popping the empty stack. Observe how we used
pattern matching in the left hand side of the equation for the non-empty
stack.
.. admonition:: Exercise
Your specification for the Towers of Hanoi puzzle has to be
parameterized by the number of discs ``N``, such that changing the
value of ``N`` requires a change in one place of your specification only.
For this, introduce the following maps:
* ``N: Pos``, which holds the value of ``N``;
* ``build_stack: Pos # Pos -> Stack``, which creates a stack of discs.
Define equations for the function ``build_stack`` such that
``build_stack(x,y)`` returns the stack ``[x , x+1, ..., y]`` for any positive
numbers ``x`` and ``y``. For example, ``build_stack(1,4)`` should return
``[1,2,3,4]``. For now, define ``N`` to be equal to 3.
.. admonition:: Solution
:class: collapse
This can be achieved using the following mCRL2 code:
.. code-block:: mcrl2
map N: Pos;
build_stack: Pos # Pos -> Stack;
var x, y: Pos;
eqn N = 3;
(x == y) -> build_stack(x, y) = [x];
(x < y) -> build_stack(x, y) = x |> build_stack(x+1, y);
The stack specification, extended with ``N`` and ``build_stack`` is available
as :download:`stack2.mcrl2 `.
You can verify that the behaviour of the ``Stack`` data type, and the functions
defined on it, is as expected by opening the file in :ref:`tool-mcrl2xi`. As
:ref:`tool-mcrl2xi` expects a specification that includes a process as input
it is required to add the line
.. code-block:: mcrl2
init delta;
to your specification (specifying the initial process). Now pushing the
:guilabel:`Parse and type check` button will parse and typecheck the
specifications. Any errors that occur will be reported. If your specification
parses and typechecks correctly, you can test the rewrite rules in your
specification. Enter e.g. ``build_stack(1,4)`` in the
:guilabel:`Rewrite Data expression` field, and press :guilabel:`Rewrite`. If
all is well, the tool reports the following in the :guilabel:`Output` window::
[08:34:30.908 info] Result: "[1, 2, 3, 4]"
.. admonition:: Exercise
Specify the ``Peg`` process in mCRL2. It should have two parameters:
* ``id: Pos``, the peg's number;
* ``stack: Stack``, the peg's stack of discs.
What actions can a single peg perform? What data parameters must these actions
have? Declare the actions first and then define the ``Peg`` process in mCRL2.
.. admonition:: Solution
:class: collapse
A peg can ``receive`` a disc from another peg, and it can ``send`` a disc
to another peg. The actions have three parameters:
* a disc, the disc that is being moved,
* the peg that the disc is *moved from*, and
* the peg that the disc is *moved to*.
This results in the following declaration:
.. code-block:: mcrl2
act receive, send: Pos # Pos # Pos;
A possible specification of the ``Peg`` process is the following.
.. literalinclude:: files/hanoi1.mcrl2
:language: mcrl2
:lines: 24-29
.. admonition:: Exercise
Specify the initial process. Use the ``allow`` and ``comm``
operators to enforce communication between the ``Peg`` processes.
.. admonition:: Solution
:class: collapse
The complete specification is given below, where the following actions are used:
* ``move(d,p,q)``: disc ``d`` is moved from peg ``p`` to peg ``q``;
* ``receive(d,p,q)``: peg ``q`` receives disc ``d`` from peg ``p``;
* ``send(d,p,q)``: peg ``p`` sends disc ``d`` to peg ``q``.
A ``move`` action is the result of synchronizing a ``send`` and a ``receive``
action.
.. literalinclude:: files/hanoi1.mcrl2
:language: mcrl2
When generating the state spaces for ``N = 1,..., 6``, we find that the
number of states is precisely ``3^N``.
The state space for ``N=3`` is depicted in Figure :ref:`fig-hanoi3`.
.. _fig-hanoi3:
.. figure:: img/hanoi3.*
:align: center
:width: 100%
State space of the Hanoi puzzle for 3 discs
The above state space can be reproduced by the following commands::
$ mcrl22lps hanoi1.mcrl2 hanoi1.lps
$ lps2lts hanoi1.lps hanoi1.lts
$ ltsgraph hanoi1.lts
We use the tool :ref:`tool-lps2lts` to see if there are any deadlocks by passing
the ``-D`` option::
$ lps2lts -D hanoi1.lps
No deadlocks are reported. This implies that this specification allows to
continue moving discs when the solution has already been obtained. We disallow
this by strengthening the guard for the ``send`` action in the ``Peg`` process
to:
.. code-block:: mcrl2
!empty(stack) && !(#stack == N && id == 3)
This ensures that the system deadlocks when all discs are on peg 3. The
specification with this extension is available as :download:`hanoi2.mcrl2
`.
When checking for deadlocks of the new specification we find precisely
one, as expected. We save a trace to this deadlock in a file by adding the ``-t``
option. The contents of the file can be printed using :ref:`tool-tracepp`.
This is summarised by the following command execution::
$ mcrl22lps hanoi2.mcrl2 hanoi2.lps
$ lps2lts -D -t hanoi2.lps
deadlock-detect: deadlock found and saved to 'hanoi2.lps_dlk_0.trc' (state index: 26).
$ tracepp hanoi2.lps_dlk_0.trc
move(1, 1, 3)
move(2, 1, 2)
move(1, 3, 2)
move(3, 1, 3)
move(1, 2, 1)
move(2, 2, 3)
move(1, 1, 3)
This is a sequence of moves leading towards the solution. It consists of 7
moves. Because the default exploration strategy of :ref:`tool-lps2lts` is
breadth first search, we know that there is no shorter path to the solution.
We now also prove that there is no shorter path to the solution using the
µ-calculus. In fact, we shall prove two properties:
#. There is a sequence of :math:`2^N-1` moves to a deadlock.
#. There is no shorter sequence of moves to a deadlock.
These properties are captured by the following µ-calculus formulae:
#. :math:`(\mu X(n \colon \mathbb{N}) ~.~ (n = 2^N -1 \land [\top] \bot) \,\lor\, (n < 2^N-1 \land \langle \top \rangle X(n+1)))(0)`
In ASCII syntax, this is represented as follows (available in
:download:`hanoi1.mcf `
.. literalinclude:: files/hanoi1.mcf
:language: mcrl2
#. :math:`(\nu X(n \colon \mathbb{N}) ~.~ n \geq 2^N-1 \,\land\, ([\top] X(n+1) \lor \langle\top\rangle\top))(0)`
In ASCII syntax, this is represented as follows (available in
:download:`hanoi2.mcf `
.. literalinclude:: files/hanoi2.mcf
:language: mcrl2
We check the formula on the specification by generating and solving PBESes as
follows::
$ mcrl22lps hanoi2.mcrl2 | lps2pbes -f hanoi1.mcf | pbes2bool
true
$ mcrl22lps hanoi2.mcrl2 | lps2pbes -f hanoi2.mcf | pbes2bool
true
This yields *true* for both formulae, so both properties hold. Check these
properties for various values of ``N``.
Optimal strategy
^^^^^^^^^^^^^^^^
It is known that the shortest sequence of moves for solving the Hanoi puzzle
with ``N`` discs, is precisely the sequence that we obtain by repeatedly
alternating the following two moves until all discs are on peg 3:
#. Move the smallest disc one peg to the left if ``N`` is odd, and to the right
if ``N`` is even.
#. Perform the move that does not involve the smallest disc.
For move 1 we consider peg 1 to be right of peg 3 and peg 3 to be left of peg 1.
Observe that move 2 exists and is uniquely defined, except for the initial and
final situations of the puzzle.
We now adapt our mCRL2 specification to model this optimal strategy only. In
other words, the state space of our model will only consist of the shortest
sequence of moves that leads to the solution. For this we first introduce a
function ``next`` that yields the next peg to which the smallest disc has to
move, according to move 1:
.. literalinclude:: files/hanoi3.mcrl2
:language: mcrl2
:lines: 31-34
Our strategy for enforcing that only move 1 and move 2 occur alternatingly is to
add a fourth process to the model that allows precisely those moves only. This
process will take part in the synchronization of the ``send`` and ``receive``
actions with an ``allowed`` action to produce a ``move`` action. We then rely on
the fact that *all* actions that participate in a synchronous communication have
to be present in order for that communication to succeed. This way, a ``move``
can *only* occur if ``send``, ``receive`` and ``allowed`` happen at the same
time, with the same parameter values.
The process that performs the ``allowed`` actions is actually modelled by two
processes: ``AllowSmall`` that allows move 1 and ``AllowOther`` that allows move
2. After performing an ``allowed`` action, every process then calls the other
process to ensure that move 1 and move 2 alternate indeed. Below are the action
declaration of ``allowed`` and the process definitions:
.. literalinclude:: files/hanoi3.mcrl2
:language: mcrl2
:lines: 36-42
Now, we enforce the aforementioned synchronization in the initial process
definition. Because move 1 comes first, we call ``AllowSmall`` in the parallel
composition.
.. literalinclude:: files/hanoi3.mcrl2
:language: mcrl2
:lines: 44-
The full specification is available as :download:`hanoi3.mcrl2
`.
Generating the state space via :ref:`tool-mcrl22lps` and :ref:`tool-lps2lts`
yields 8 states and 7 transitions for ``N=3``, obtained using the following
command sequence::
$ mcrl22lps hanoi3.mcrl2 hanoi3.lps
$ lps2lts -v hanoi3.lps hanoi3.lts
...
[12:38:30.547 verbose] done with state space generation (8 levels, 8 states and 7 transitions)
In general, the state space has :math:`2^N` states and :math:`2^N-1`
transitions, as may be expected after our model-checking exercises on the
complete model in the previous section. The action trace can be visualized by
loading the state space into :ref:`tool-ltsgraph`, or it can be simulated by
loading the LPS into :ref:`tool-lpsxsim`.