Conjoining a spec with an invariant

[Willy Schultz]

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.

  

[Leslie Lamport]

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.

[Willy Schultz]

Great, thank you, that makes sense. 

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.