# Re: [tlaplus] for all, the transition condition is true?

 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 On 7/24/19 4:02 AM, juliet kim wrote: Hello,  Here is a simple specification. I wonder whether the Next is enabled. -------------------------------- Variable q SetA == {"a1", "a2", s3} Init == q = [a \in  SetA |-> <<>>] Next = \A x \ {1,2} :                           LET m = IF x = 1 THEN "a1"                                         ELSE                                                   IF x = 2 THEN "a2"                                                  ELSE "a3"                          IN                                 q' = [q EXCEPT  ![m] = Append(@, x)] Spec = Init /\ [][Next]_q For all x, Next can be true? When I use TLC, it doesn't seem to be true. For example, for 1, it's true at first but next 2 is not true. Ideally, I expected that q's state is like [a1 |-> <<1>>, a2 |-> <<2>>, a3 |-> <<>>], but Next action is not enabled. I want q's field value to be changed for all x values. I need your advice. Thanks, -- 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/fd9c65b6-68c6-418e-9436-ab4e5cacf99a%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/b5d3149e-0c47-e6a2-cc83-3cf5acd237ee%40gmail.com.