the first approach that you describe is the standard way to check that a predicate holds throughout the execution except at certain control points. TLC will help you maintain an appropriate definition of the set of exceptions.
Your second suggestion is complementary: it ensures that the predicates are eventually restored . If you've already checked the first property you can also write
\A p \in ProcSet : <> ~(pc[p] \notin InvocationLabels)--
or perhaps even
\A p \in ProcSet : <> ~(pc[p] \notin InvocationLabels)
if violations of the predicate are not recurrent.
 Remember that a safety property is true of an algorithm that does nothing. In particular, checking your invariant won't require any fairness assumption, but the liveness property will.
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/21B1426F-3CCA-422A-A0FA-32C96C9A0C12%40gmail.com.