[tlaplus] Conjoining a spec with an invariant

[Willy Schultz <will62794@xxxxxxxxx>]

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.

  

-- 
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/9a13721f-eb0e-455c-bb04-befc940d27c9n%40googlegroups.com.