--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0574ac0e-f6f6-4629-af87-063e96a8d62d%40googlegroups.com.
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 Next simpler:
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
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C90472BE-7811-453E-BB36-3E7447A614E2%40gmail.com.