[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Simple exercise: hanoi



Hi,

This is my first complete and working specification. I'll be grateful for your comments.


------------------------------- 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.

Best regards,
Emanuel

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0574ac0e-f6f6-4629-af87-063e96a8d62d%40googlegroups.com.