[tlaplus] TLC error when choosing an arbitrary value

[Arnaud Bos <mail@xxxxxxxxxxxxx>]

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:

• TLC attempted to evaluate an unbounded CHOOSE.
  Make sure that the _expression_ is of form CHOOSE x \in S: P(x).
  line 31, col 14 to line 31, col 54 of module Archivist_V2
  The error occurred when TLC was evaluating the nested
  expressions at the following positions:
  0. Line 867, column 9 to line 887, column 77 in Archivist_V2
  ...

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.