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

[tlaplus] How Can I Specify a State Can Be Reachable in TLC?


I'm writing a specification. I want to check if a state can be reachable from Init in all the state space.

I have a work around to do it for now: I define this behavior as part of Next step. If TLC find it's never enabled, it will report some warnings. I'm wondering if there is a way to define this as a property of the specification and let TLC report error if it's never enabled.


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/952408be-1165-4f6a-a37f-d0ddac456afcn%40googlegroups.com.