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

*From*: Smruti Padhy <smruti.padhy@xxxxxxxxx>*Date*: Wed, 14 Apr 2021 11:22:02 -0700 (PDT)*Ironport-hdrordr*: A9a23:kK2H/KvDucbWVXroiZNQSmvO7skC2YMji2hD6mlwRA09T+WzkceykPMHkSLlkTp5YgBdpfmsGomlBUnd+5l8/JULMd6ZNmTbkUahMY0K1/qH/xTOACv7n9QtsptIU687M9HoCEg/sMCS2njBL/8EwMObtIiyj+bf0HsFd3AdV4hE7x1lTieWF1QefngwObMdFICAouprzgDQCkg/S8SgGz09WfLfzue74K7ORB4dGloa7xOThimj877wH3Gjr14jehdu5ZtnzmTfiQz+4cyYwoyG4zvV12rS6JoTndv617J4dbyxo+wYMC/lhArtRIkJYcz6gBkNu+2k5Fsnl9PByi1QTvhb0H/acmGrrRaF4WCJu0dN11bYxVCVmnflq8DiLQhKcPZpvo5Bdwuc1kxIhqAD7Itw02WVu4E/N3z9tR7g7NvFXQwCrDvPnVMel4co/hpieLpbQ7NcqrEf8FhYea1wfx7S2cQIFK1LANvH7PhbNWmGZ23U11MA/PWcGlo0GBmCTgwumOywlwJXkndw0lcCyKUk8ksoxdYSTZ9L4uiBHL9viKgLbsJ+V9MJOM4xBeWwDGLJTVb3NH+KZW7gCLoMNxv2yqLf0fES/+GleJsByd8JlJPNXEgwjx9MR2veTfaD1pFK7RzBKV/cLFHQ4/Ab3YFwvvnXRbbgMyGPDHAo1+W6pekHa/erKcqOBA==*References*: <90b306a3-c413-4b09-810e-98aedb44d91fn@googlegroups.com> <BA49039D-022B-486C-B57A-D7DFC676F265@gmail.com>

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,

Smruti

On 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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d9af2d7a-f150-422f-956a-98b6b69f7843n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] TLAPS proof of increment and update***From:*Stephan Merz

**References**:**[tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

**Re: [tlaplus] TLAPS proof of increment and update***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] meaning of the lead to (~>) operator** - Next by Date:
**Re: [tlaplus] meaning of the lead to (~>) operator** - Previous by thread:
**Re: [tlaplus] TLAPS proof of increment and update** - Next by thread:
**Re: [tlaplus] TLAPS proof of increment and update** - Index(es):