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,