|A property P is valid if it holds in every run. In other words, P is not valid if and only if there exist runs that do not satisfy P (i.e., satisfy ~P). This does not mean that all runs satisfy ~P.|
In your example, TLC tells you that there are some runs that satisfy Prop_1 / Prop_2 and some that do not.--
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/B46B8446-3AC7-4F6F-A8B9-655AD9BB1333%40gmail.com.