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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Sat, 21 Mar 2020 12:19:59 -0500*References*: <0574ac0e-f6f6-4629-af87-063e96a8d62d@googlegroups.com> <C90472BE-7811-453E-BB36-3E7447A614E2@gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:68.0) Gecko/20100101 Thunderbird/68.6.0

Hi,

Once we've done this, we can simplify the spec even further by
moving all of the towers into a single `towers` sequence,
where each indice of `towers `is one of the three
towers. Then we can make

`Init ==
towers = <<
<< 1, 2, 3, 4 >>,
<<>>,
<<>>
>>
Next == \E t1, t2 \in DOMAIN towers:
t1 /= t2 /\ Move(t1, t2)
`

Modifying `Move` is left as an exercise to the reader :)

H

On 3/21/2020 6:30 AM, Stephan Merz
wrote:

Hello,--

the spec looks quite reasonable, and in order to find a solution to the Tower of Hanoi problem you'd check the invariant

c # <<1,2,3,4>>

so that TLC gives you a solution as a counter-example. Two remarks:

1. The operator Compare is used only when the first parameter is non-empty, but you could be more "defensive" by checking this explicitly. I'll redefine it to simplify what follows:

Compare(x,y) ==/\ ~ Empty(x)/\ Empty(y) \/ Head(x) < Head(y)

2. All actions have the same shape, so you could have defined a single action

\* move the head of sequence x to y provided Compare(x,y) holds, and leave z unchangedMove(x,y,z) ==/\ Compare(x,y)/\ x' = Tail(x) /\ y' = Cons(Head(x), y) /\ z'=z

Next ==\/ Move(a,b,c) \/ Move(a,c,b)\/ Move(b,a,c) \/ Move(b,c,a)\/ Move(c,a,b) \/ Move(c,b,a)

Regards,Stephan--

On 21 Mar 2020, at 12:06, Emanuel Koczwara <emanuel.koczwara@xxxxxxxxx> wrote:

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.

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/C90472BE-7811-453E-BB36-3E7447A614E2%40gmail.com.

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/5c8ca10b-ccd6-aea4-52f0-4e83bd0fef58%40gmail.com.

**References**:**[tlaplus] Simple exercise: hanoi***From:*Emanuel Koczwara

**Re: [tlaplus] Simple exercise: hanoi***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Simple exercise: hanoi** - Next by Date:
**[tlaplus] How to identify which temporal property is violated ?** - Previous by thread:
**Re: [tlaplus] Simple exercise: hanoi** - Next by thread:
**[tlaplus] How to identify which temporal property is violated ?** - Index(es):