| Hello again, my initial message was perhaps a little cryptic, so let me explain the rationale behind it. You were effectively trying to prove the implication TypeInvariant /\ SafetyProperty /\ Inc => SafetyProperty' but this implication doesn't hold. As a concrete counter-example, consider the state valX = [ val |-> 42, ts |-> 23 ] valY = [ val |-> 42, ts |-> 70 ] clock = 27 (I'm omitting the variable n because it is unimportant for this discussion.) Observe that this state satisfies both TypeInvariant and SafetyProperty. In particular, the latter holds trivially because the left-hand side of the implication is false. Now, Inc will lead you to the state valX = [ val |-> 43, ts |-> 28 ] valY = [ val |-> 42, ts |-> 70 ] clock = 28 and SafetyProperty is false for that state. This shows that SafetyProperty is not inductive (relative to TypeInvariant). However, the first state is actually not reachable in your specification, and one way to rule it out is to observe that time stamps cannot exceed the clock value. This observation leads to asserting the invariant ClockInv, which makes the proof go through. Now, in general there is no guarantee that the additional predicate is an inductive invariant: you may have to iterate the process and successively add more information about reachable states in order to obtain an inductive invariant that you can prove with a proof assistant such as TLAPS. As for model checking, you are completely right that you need to bound the state space that TLC will explore. One standard way to do this is to add a state constraint where you bound the value of clock. Stephan
--
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/A085D874-3F90-4D91-B89C-28C06ED3AB4D%40gmail.com. |