// **************************************************************************
//
//    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);
}