[tlaplus] Re: Conjoining a spec with an invariant

As you suspected, your specification SpecStrong1 is perfectly fine TLA+, but TLC does not handle it correctly. It is considering the formula []C1 part of a liveness specification, so if you had it check a liveness property P it would actually be checking the property []C1 => P. SpecStrong2 is almost equivalent to SpecStrong1. The equivalent specification is

Init /\ C1 /\ [][Next /\ C1']_vars

assuming that vars includes all the variables in C1. That's the best way to write your spec. Using it as a state constraint wouldn't quite work because, if I recall correctly, TLC does not look for successor states to a state not satisfying the constraint, but it does do invariance checking on that state.

On Wednesday, November 25, 2020 at 6:52:05 AM UTC-8 will...@xxxxxxxxx wrote:

I am working on a spec, call it Spec, that I expect to violate some safety property, call it Safety, but I want to demonstrate that under a certain stronger assumption C1 (which is a state predicate), Spec does satisfy safety. That is:

C1 == (* some state predicate *)
Spec == Init /\ [][Next]_vars
SpecStrong1 == Spec /\ []C1

THEOREM ~(Spec => Safety)
THEOREM SpecStrong1 => Safety

I was not sure if TLC would correctly handle the form of specification used for SpecStrong1, though. I also tried writing this as:

SpecStrong2 == Init /\ [][Next /\ C1']_vars

which seemed to work correctly i.e. the model checker returned no invariant violation which matched my expectations.

I also considered specifying C1 as a state constraint during model checking but I'm not sure if that would achieve my goal correctly. My understanding is that, from a pure TLA+ perspective, SpecStrong1 is a valid formula with a sensible meaning, it just may not be handled by TLC. Any thoughts or suggestions on this would be appreciated.

tlaplus+unsubscribe@xxxxxxxxxxxxxxxx

https://groups.google.com/d/msgid/tlaplus/1eb911e2-4e51-48d0-a98b-0038334e6e48n%40googlegroups.com