hanoi.tla

------------------------------- MODULE hanoi -------------------------------
EXTENDS Integers, Sequences
\* Towers of hanoi problem
VARIABLES tower1, tower2, tower3
\* Initiallize the towers
Init == /\ tower1 = <<3,2,1,0>>
        /\ tower2 = <<0>>
        /\ tower3 = <<0>>

\* Transition rules
move(from,to,helper) == 
      IF Len(from) /= 0 /\ Len(to) /= 0 THEN
               IF Head(from) > Head(to) 
               THEN /\ to' = <<Head(from)>> \o to
                    /\ from' = Tail(from)
                    /\ helper' = helper
               ELSE to' = to /\ from' = from /\ helper' = helper
      ELSE to' = to /\ from' = from /\ helper' = helper
               
          
\* Next states
Next == \/ move(tower1,tower2,tower3)
        \/ move(tower2,tower1,tower3)
        \/ move(tower1,tower3,tower2)
        \/ move(tower3,tower1,tower2)
        \/ move(tower3,tower2,tower1)
        \/ move(tower2,tower3,tower1)

\* Terminal state
TerminalState == tower3 /= <<3,2,1,0>> 

=============================================================================