How Can I Specify a State Can Be Reachable in TLC?

[Bin Wang]

Hi,

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.

Thanks!

[Stephan Merz]

If I understand correctly, you are trying to check if a certain is reachable. You can state an invariant that asserts that (a predicate characterizing) the state is always false, and TLC will display a counter-example if the state can be reached. If you have a different property in mind, an example would help.

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/952408be-1165-4f6a-a37f-d0ddac456afcn%40googlegroups.com.

[Bin Wang]

Hi Stephan,

This is a good idea. But I still have two concerns:

1. If I also want to check other invariant, will this error early break other checks? If so, I may need to run it multiple times with different invariant.

2. If I integrate it into CI or share the model with someone else, this may seems not very intuitive and require addition explanation.

[Stephan Merz]

Hello again,

on your first question: TLC will indeed stop at the first error, so you probably want to perform the reachability check separately from verifying other invariants.

About the second item, I can only encourage you to document your specifications, including the properties that are checked. In a CI context, you can indicate which outcome is considered an error. For checking reachability, you want to invert the standard interpretation and consider "successful verification" an error.

Regards,

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e2aa4938-cb32-49b8-980d-fdcb28eee122n%40googlegroups.com.

[Leslie Lamport]

There is an alternative approach.  You can add a fairness property that ensures that the desired state must be reached, and have TLC check the liveness property that the state is eventually reached.  See my paper Proving Possibility Properties.

Leslie