| Hello,
what you have done so far looks good. In order for TLC to check the invariant, "setInvariant" should be added to the invariants to be verified (with the box checked) in "Model Overview" -> "What to check?" -> "Invariants".
If that doesn't help, could you explain what doesn't work and perhaps share your specification?
Regards, Stephan
Hi All,
I'm currently learning TLA+ and I met a problem that how can I check set emptiness?.
I have two sets A and B.
In every step, A∩B should be an empty set. So after writing TLA specification, I would like to add this as an Invariant property. For doing this I wrote following code. But it doesn't work :-(
setInvariant == A \cap B = {}
-Regards
Nikhila K N
--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|