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

Re: [tlaplus] TLC error when choosing an arbitrary value



I just found this : https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/CachingMemory/MCInternalMemory.cfg#L24-L27

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.

On Tue, Nov 24, 2020 at 2:54 PM Arnaud Bos <mail@xxxxxxxxxxxxx> wrote:

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 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.