| Hi Ognjen, CHOOSE is deterministic, and TLC chooses some fixed value for the function. It may well be the function f such that f[x,y] = 1 for all x \in X and y \in Y, in which case the invariant holds. The outcome will be different if you write either Next == \E f \in [X \X Y -> X], y \in Y : val_x' = f[val_x, y] or VARIABLE val_x, f Init == val_x = 1 /\ f \in [X \X Y -> X] Next == \E y \in Y : /\ val_x' = f[val_x, y] /\ f' = f In the first case, a different function may be chosen at every transition. In the second case, the choice of f is fixed for any given execution, but TLC will explore executions for all possible values of f. As a rule of thumb, use CHOOSE only if there is precisely one value that satisfies the predicate. When there are several choices, you have no control over which value will be chosen, and in particular TLC will not enumerate all possible choices. Use existential quantification for non-deterministic choice. Hope this helps, Stephan
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/93E9F1D1-3676-4B14-8355-355DBE1FA168%40gmail.com. |