<out.png>
Now I'm trying to add some liveness properties. This one fails immediately in <Intial predicate>:AlwaysTick == []<><<Tick>>_bStateas well as this one:AlwaysTick == []<><<Next>>_bStateCould someone explain why this happens?Help is greatly appreciated.
--
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/b8246fe3-693d-4e49-9315-6946de773bb2%40googlegroups.com.
<out.png>
Stephan
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.