```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  Towers of Hanoi
//
//  There is a tower of discs of different sizes. The problem is to move
//  the tower to another place, where only one disc can be moved in each
//  step. Moreover, it is not allowed to put a larger disc on a smaller
//  one. Finally, there is only a limited number of places where to put
//  the discs. These places are called towers, since the discs are stapled
//  to towers at these places.
//
//  Clearly, the less towers and the more discs, the more movements are
//  required to move the initial tower to another place.
//
// **************************************************************************

macro towers = 3;
macro discs = 4;

module Hanoi(
nat{towers} ?FromTW, ?ToTW,
[towers][discs()]nat{discs()+1} TW,
[towers]nat{discs()+1} DiscsOnTW,
event !error, !moved
) {
// Initialization: all discs are on tower 0
DiscsOnTW[0] = discs;
for(i=0..discs-1)
TW[0][i] = discs-i;
pause;
// play the game
always {
if(FromTW!=ToTW)
if(FromTW<towers and ToTW<towers())
if(DiscsOnTW[FromTW]>0)
if(DiscsOnTW[ToTW]==0) {
next(TW[ToTW][0]) = TW[FromTW][DiscsOnTW[FromTW]-1];
next(TW[FromTW][DiscsOnTW[FromTW]-1]) = 0;
next(DiscsOnTW[ToTW])   = 1;
next(DiscsOnTW[FromTW]) = DiscsOnTW[FromTW]-1;
emit (moved);
} else if(TW[FromTW][DiscsOnTW[FromTW]-1]<TW[ToTW][DiscsOnTW[ToTW]-1]) {
next(TW[ToTW][DiscsOnTW[ToTW]]) = TW[FromTW][DiscsOnTW[FromTW]-1];
next(TW[FromTW][DiscsOnTW[FromTW]-1]) = 0;
next(DiscsOnTW[ToTW])   = DiscsOnTW[ToTW]+1;
next(DiscsOnTW[FromTW]) = DiscsOnTW[FromTW]-1;
emit (moved);
}
}
} satisfies {
DiscsOnTW_correct: assert
A G forall(i=1..discs)
forall(j=0..discs-1)
forall(toTW=0..towers-1)
forall(fromTW=0..towers-1)
((ToTW==toTW) & (FromTW==fromTW) & (DiscsOnTW[FromTW]==i) & (DiscsOnTW[ToTW]==j) & moved
-> A X ((DiscsOnTW[fromTW]==i-1) & (DiscsOnTW[toTW]==j+1)));
Ordered: assert
A G forall(i=0..towers-1)
forall(j=0..discs-2)
((j<DiscsOnTW[i]) -> (TW[i][j]>TW[i][j+1]));
Goal [DisProveA]: assert
A G (DiscsOnTW[1]!=discs);
}
```