[tlaplus] A CHOOSE+TLC conundrum

[Ognjen Maric <ognjen.maric@xxxxxxxxx>]

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3caab352-1bd8-4335-bbc1-5568ce7782b6n%40googlegroups.com.