Hi Juliet,
We can rewrite Next as:
Next == \A x \in {1, 2}:
IF x = 1 THEN q' = [q EXCEPT !["a1"] = Append(@,
x)]
ELSE IF x = 2 THEN q' = [q EXCEPT !["a2"] =
Append(@, x)]
ELSE UNCHANGED q
In practice that will be
Next ==
/\ q' = [q EXCEPT !["a1"] = Append(@, 1)]
/\ q' = [q EXCEPT !["a2"] = Append(@,
2)]
From Init, that will be equivalent to
Next ==
/\ q' = [a1 |-> <<1>>, a2
|-> <<>>, a3 |-> <<>>]
/\ q' = [a1 |->
<<>>, a2 |-> <<2>>, a3 |->
<<>>]
So we have two different values for q', which is impossible, so Next is never enabled.
There are a few different ways you can get what you want, but the simplest is to probably make it explicit:
\* Sequences are functions with domain 1..Len(seq)
Map == <<"a1", "a2", "a3">>
Next ==
/\ q' = [x \in DOMAIN q |->
IF Map(x) \in {1, 2}
THEN Append(q[x], Map(x))
ELSE q[x]]
H
--
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/fd9c65b6-68c6-418e-9436-ab4e5cacf99a%40googlegroups.com.