If I get it right, then NoVal actually has to be defined by the model/spec user. In which case, how do I ensure that the value is coherent with regards to other values?
I just wanted to assign it to a quite large subset of "anything" so that the spec user doesn't have to bother.
But I ended up with two new constants, User and Archivist, and two more assumptions:
/\ User \notin Workers
/\ Archivist \notin (Workers \union {User})
as guardrails.
It works but if there's a more "idiomatic" way to do this I would like to know.
Thanks.
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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/03gjm_PrQiM/unsubscribe.
To unsubscribe from this group and all its topics, 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.