In fact, TLC checks neither of the two implications that you indicate but verifiesLET f == CHOOSE f \in F : TRUEIN Spec => InvAssuming that F is non-empty, this is implied by\A f \in F : Spec => Invand it implies\E f \in F : Spec => InvThe actual choice of f is fixed by the interpretation in which the formula is evaluated (and which includes a choice operator mapping every non-empty set to some element of that set). TLC does not enumerate the possible choice operators but conceptually implements a fixed one. [1]Stephan[1] In full detail, it's more complicated than that because it is only possible to implement an approximation of a choice operator, which does not ensure that two non-empty sets that are equal but represented differently are mapped to the same element, see section 14.6 of Specifying Systems.On 13 Sep 2023, at 15:07, Ognjen Maric <ognjen...@xxxxxxxxx> wrote:Hi Stephan,
Thank you for the response. I understand that CHOOSE is deterministic, but it's still not clear to me that TLC's response is correct. Logically, TLC successfully verified the implication:
Spec(CHOOSE f: f \in F) => Inv (let's call this Imp)
You seem to be saying that, since
\E f \in F: Spec(f) => Inv
(which is true) then TLC was right to declare (Imp) as verified? That doesn't seem correct to me. Or am I misunderstanding what you're saying?
I'd expect that, given that F # {}, we'd have to prove
\A f \in F: Spec(f) => Inv
instead. Though I'm not sure if this is equivalent to (Imp) (I think it's stronger than Imp, given that F # {}, but not sure about equivalence).
Cheers,
OgnjenOn Wednesday, September 13, 2023 at 1:09:35 PM UTC+2 Stephan Merz wrote: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.--
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/2372af21-7cd8-45c2-94b7-84e5b39ad16cn%40googlegroups.com.