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

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


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"
                                                 IF x = 2 THEN "a2"
                                                 ELSE "a3"
                                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.


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.