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

[tlaplus] TLC error when choosing an arbitrary value

Hello folks,

When I try to choose an arbitrary value User like so:

User == CHOOSE Whatever : Whatever \notin Workers
Archivist == CHOOSE Whatever : Whatever \notin (Workers \union {User})

(where Workers is constant, a set of model values)

TLC complains with:

I'm confused. It looks similar to the "NoVal ≜ ..." statement in the caching memory example of Specifying Systems (here) and to the pattern described in this topic:
Null ≜ CHOOSE Null : Null ∉ Result

What am I missing? Valid TLA+/TLAPS statement but inivalid TLC?

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/8ab3cb5f-03c6-4dfe-88f7-cbeace798806n%40googlegroups.com.