[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Conjoining a spec with an invariant

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.