------------------------------- MODULE hanoi -------------------------------
EXTENDS Integers, Sequences
VARIABLES a, b, c
Empty(seq) == Len(seq) <= 0
Cons(elem, seq) == << elem >> \o seq
Compare(first, second) == ~Empty(second) /\ Head(first) < Head(second)
AB == /\ ~Empty(a)
/\ Empty(b) \/ Compare(a, b)
/\ a' = Tail(a) /\ b' = Cons(Head(a), b) /\ c' = c
AC == /\ ~Empty(a)
/\ Empty(c) \/ Compare(a, c)
/\ a' = Tail(a) /\ b' = b /\ c' = Cons(Head(a), c)
BA == /\ ~Empty(b)
/\ Empty(a) \/ Compare(b, a)
/\ a' = Cons(Head(b), a) /\ b' = Tail(b) /\ c' = c
BC == /\ ~Empty(b)
/\ Empty(c) \/ Compare(b, c)
/\ a' = a /\ b' = Tail(b) /\ c' = Cons(Head(b), c)
CA == /\ ~Empty(c)
/\ Empty(a) \/ Compare(c, a)
/\ a' = Cons(Head(c), a) /\ b' = b /\ c' = Tail(c)
CB == /\ ~Empty(c)
/\ Empty(b) \/ Compare(c, b)
/\ a' = a /\ b' = Cons(Head(c), b) /\ c' = Tail(c)
Init == /\ a = << 1, 2, 3, 4 >>
/\ b = <<>>
/\ c = <<>>
Next == AB \/ AC \/ BA \/ BC \/ CA \/ CB
Spec == Init /\ [][Next]_<<a, b, c>>
=============================================================================
Please note: the goal was to make it as simple as possible, I've done it together with my son, to show him how math and computers can solve real world problems.