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

*From*: Ognjen Maric <ognjen.maric@xxxxxxxxx>*Date*: Wed, 13 Sep 2023 02:00:08 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] A CHOOSE+TLC conundrum***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] question about invariant and random numbers** - Next by Date:
**Re: [tlaplus] A CHOOSE+TLC conundrum** - Previous by thread:
**Re: [tlaplus] question about invariant and random numbers** - Next by thread:
**Re: [tlaplus] A CHOOSE+TLC conundrum** - Index(es):