When generating a model for TLC, the Toolbox introduces a new model value Val for every definition of the form
Val == CHOOSE x : x \notin S
and overrides the definition to assign that model value to the operator. (Remember that model values are different from any standard TLA+ values and also different from each other so this does what you want.) It sounds like you are using TLC from another interface (perhaps the command line), and then you will have to do this manually in your configuration file. As the error message says, TLC cannot evaluate unbounded quantification (\A, \E, CHOOSE).
Introducing additional constants in the spec and assigning them model values in the configuration is essentially equivalent.
Regards, Stephan
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.
-- 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/CAMH7Ucf4O%3DroaFOwXvQ%3DSN6L2XgEnaK9LOyGocDC1g1%2Bp0aGfA%40mail.gmail.com.
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/A251A91B-7A12-485C-90BD-E2089E4E4E1A%40gmail.com.
|