Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],
but can't enumerate the value of the `val' field:Nat
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 implicationTypeInvariant /\ SafetyProperty /\ Inc => SafetyProperty'but this implication doesn't hold. As a concrete counter-example, consider the statevalX = [ 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 statevalX = [ val |-> 43, ts |-> 28 ]valY = [ val |-> 42, ts |-> 70 ]clock = 28and 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.StephanOn 14 Apr 2021, at 20:22, Smruti Padhy <smruti...@xxxxxxxxx> wrote:Thank you, Stephan for the detailed proof and for pointing the need for the clock invariant for the safety property proof instead of those conditions as enabling conditions. I will go through examples and tutorials again as it seems I might be missing some basic concepts.Regarding MaxNum, I added it to limit the number of Inc actions and in turn, limit the number of states during TLC model checking. I couldn't think of a better way to do that. I agree that SpecAssumption is spurious.Thanks again for the help.Best,SmrutiOn Tuesday, April 13, 2021 at 12:35:03 PM UTC-5 Stephan Merz wrote:Hello,the problem is that your safety property is not an inductive invariant (even with respect to the typing invariant). However, it is easy to see that the time stamps of your variables can never exceed the clock value, and so the extra guard that you added to the Inc action is actually an invariant of your specification. It even happens to be an inductive invariant.The attached TLA+ module contains a proof of the safety property. Please see the TLAPS tutorial or other examples in the distribution for the concept and the importance of inductive invariants.Hope this helps,StephanP.S.: The constant MaxNum is (obviously) unnecessary for the prover – better add a state constraint to the model that you use for TLC instead of adding a spurious precondition in your specification. -s--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d9af2d7a-f150-422f-956a-98b6b69f7843n%40googlegroups.com.