| 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
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.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e2aa4938-cb32-49b8-980d-fdcb28eee122n%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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C4F85B99-7EF8-420A-AA22-5563410712AB%40gmail.com.
|