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

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



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

On Sunday, October 4, 2020 at 9:54:57 AM UTC-7 Stephan Merz wrote:
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

On 4 Oct 2020, at 18:47, Bin Wang <wbi...@xxxxxxxxx> wrote:


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.
在2020年10月4日星期日 UTC-4 下午12:32:22<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

On 4 Oct 2020, at 18:28, Bin Wang <wbi...@xxxxxxxxx> wrote:


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!

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

--
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/ff795752-17b2-4e6f-9f22-cd1e3975e503n%40googlegroups.com.