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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 25 May 2022 13:01:01 +0200*References*: <672137231.2107000.1653476007745.ref@mail.yahoo.com> <672137231.2107000.1653476007745@mail.yahoo.com>

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

**Follow-Ups**:**Re: [tlaplus] Checking reachability***From:*'Chris' via tlaplus

**References**:**[tlaplus] Checking reachability***From:*'Chris' via tlaplus

- Prev by Date:
**[tlaplus] Checking reachability** - Next by Date:
**Re: [tlaplus] Checking reachability** - Previous by thread:
**[tlaplus] Checking reachability** - Next by thread:
**Re: [tlaplus] Checking reachability** - Index(es):