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?