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.