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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 21 Mar 2020 12:30:23 +0100*References*: <0574ac0e-f6f6-4629-af87-063e96a8d62d@googlegroups.com>

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 unchanged Move(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
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. |

**Follow-Ups**:**Re: [tlaplus] Simple exercise: hanoi***From:*Hillel Wayne

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

- Prev by Date:
**[tlaplus] Simple exercise: hanoi** - Next by Date:
**Re: [tlaplus] Simple exercise: hanoi** - Previous by thread:
**[tlaplus] Simple exercise: hanoi** - Next by thread:
**Re: [tlaplus] Simple exercise: hanoi** - Index(es):