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 eitherNext == \E f \in [X \X Y -> X], y \in Y : val_x' = f[val_x, y]orVARIABLE val_x, fInit == val_x = 1 /\ f \in [X \X Y -> X]Next == \E y \in Y :/\ val_x' = f[val_x, y]/\ f' = fIn 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,StephanOn 13 Sep 2023, at 11:00, Ognjen Maric <ognjen...@xxxxxxxxx> wrote:TLC successfully verifies the X_Never_2 invariant below. I think it shouldn't, but I wouldn't be the first person to misunderstand the semantics of CHOOSE.---- MODULE Test_Choose ----
X == {1, 2}
Y == {"a", "b"}
VARIABLE
val_x
F(x, y) == (CHOOSE f \in [X \X Y -> X] : TRUE)[<<x, y>>]
Init ==
val_x = 1
Next == \E y \in Y: val_x' = F(val_x, y)
Spec == /\ Init /\ [][Next]_<<val_x>>
X_Never_2 == val_x # 2
====
If it's not clear, I'd like TLC to check the spec for any choice of F with the appropriate domain/codomain. Obviously I can work around this by introducing a state variable for F and defining the Init predicate appropriately.--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3caab352-1bd8-4335-bbc1-5568ce7782b6n%40googlegroups.com.