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