uses Stack(Int)

automaton Hanoi
  signature
    internal putOnA(d: Int), putOnB(d: Int), putOnC(d: Int)
    internal start
  states
    stackA : Stack[Int] := empty,
    stackB : Stack[Int] := empty,
    stackC : Stack[Int] := empty
  transitions
    internal start                                 % initialize
      pre
        stackA = empty /\ stackB = empty /\ stackC = empty
      eff
        stackB := push(1, push(2, push (3, push (4, push(5, empty)))))
    internal putOnA(d: Int)                        % put disc d onto stack A
      pre (stackA = empty \/ top(stackA) > d) /\
          ((stackB ~= empty /\ d = top(stackB)) \/ (stackC ~= empty /\ d = top(stackC)))
      eff
        stackA := push(d, stackA);
        if (stackB ~= empty /\ d = top(stackB)) then stackB := pop(stackB)
        else stackC := pop(stackC)
        fi
    internal putOnB(d: Int)                        % put disc d onto stack B
      pre (stackB = empty \/ top(stackB) > d) /\
          ((stackA ~= empty /\ d = top(stackA)) \/ (stackC ~= empty /\ d = top(stackC)))
      eff
        stackB := push(d, stackB);
        if (stackA ~= empty /\ d = top(stackA)) then stackA := pop(stackA)
        else stackC := pop(stackC)
        fi
    internal putOnC(d: Int)                        % put disc d onto stack C
      pre (stackC = empty \/ top(stackC) > d) /\
          ((stackA ~= empty /\ d = top(stackA)) \/ (stackB ~= empty /\ d = top(stackB)))
      eff
        stackC := push(d, stackC);
        if (stackA ~= empty /\ d = top(stackA)) then stackA := pop(stackA)
        else stackB := pop(stackB)
        fi

schedule                                           % move 5 discs to stack A
  do
    fire internal start;
    fire internal putOnA(1); fire internal putOnC(2); fire internal putOnC(1);
    fire internal putOnA(3);
    fire internal putOnB(1); fire internal putOnA(2); fire internal putOnA(1);
    fire internal putOnC(4);
    fire internal putOnC(1); fire internal putOnB(2); fire internal putOnB(1);
    fire internal putOnC(3);
    fire internal putOnA(1); fire internal putOnC(2); fire internal putOnC(1);
    fire internal putOnA(5);
    fire internal putOnB(1); fire internal putOnA(2); fire internal putOnA(1);
    fire internal putOnB(3);
    fire internal putOnC(1); fire internal putOnB(2); fire internal putOnB(1);
    fire internal putOnA(4);
    fire internal putOnA(1); fire internal putOnC(2); fire internal putOnC(1);
    fire internal putOnA(3);
    fire internal putOnB(1); fire internal putOnA(2); fire internal putOnA(1)
  od