# Re: [tlaplus] A CHOOSE+TLC conundrum

Thank you, what you're saying makes sense and clears things up for me. Still, I'm a bit surprised, as I expected TLC to quantify over all interpretations when checking the formula, as I'd expect we define a formula to be true only if it's true in all interpretations. I expected that check to be possible given that TLC only supports bounded CHOOSE/quantifiers, but maybe it's not?

Cheers,
Ognjen

On Wednesday, September 13, 2023 at 3:25:58 PM UTC+2 Stephan Merz wrote:
In fact, TLC checks neither of the two implications that you indicate but verifies

LET f == CHOOSE f \in F : TRUE
IN  Spec => Inv

Assuming that F is non-empty, this is implied by

\A f \in F : Spec => Inv

and it implies

\E f \in F : Spec => Inv

The 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,
Ognjen
On 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 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

On 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.