[tlaplus] Re: Conjoining a spec with an invariant

To your point about SpecStrong2 not being exactly equivalent to SpecStrong1: in my particular spec it's more or less trivial to see that the initial states satisfy Safety (regardless of whether C1 holds or not), so I was less worried about constraining the initial states to satisfy C1. But thank you for pointing it out. I will indeed be careful to include C1 in the initial state predicate if I want to ensure that SpecStrong2 is exactly equivalent to SpecStrong1.

On Wednesday, November 25, 2020 at 11:43:03 AM UTC-5 Leslie Lamport wrote:

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.