--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ca126b11-a19f-4cb2-b67c-fcd9df861299n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c46bd513-edfa-41cf-aca1-00b4aa3e669fn%40googlegroups.com.
For (x > 0) ~> (y = 5), x is set to 1 in state
2, meaning y = 5 must be true in a future state from 2.
The error trace includes the step where x = -1 due to an
implementation detail of TLC: based on how it calculates liveness,
it doesn't guarantee that a liveness-violating trace will be the
shortest one possible.
Re the FALSE ~> (y = 5), no idea. Think it might be a bug? [](FALSE => <>TRUE) also fails, which doesn't seem right.
H
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c46bd513-edfa-41cf-aca1-00b4aa3e669fn%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/84c27c0d-ecc1-7b8d-13c6-32bd48f81a07%40gmail.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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/531db585-55d1-b729-0961-8c0d1877d8d4%40lemmster.de.