[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] A CHOOSE+TLC conundrum



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.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2372af21-7cd8-45c2-94b7-84e5b39ad16cn%40googlegroups.com.