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

[tlaplus] A CHOOSE+TLC conundrum

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"}


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.