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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 26 Feb 2021 17:37:43 +0100*References*: <26ce7a92-f4cc-43a3-a846-6dd01c03bc23n@googlegroups.com> <a2c3a96f-bc21-4be2-8bc9-11fd7b4cc0ean@googlegroups.com> <EE130A6F-1D19-43EB-BDF8-05A074CACEFA@gmail.com> <1c9424ed-1eb5-449b-99fd-064987e317f2n@googlegroups.com>

Hello, you did the right thing when you used TLC to get confident that your invariant is indeed inductive. However, even if you have an inductive invariant, there is no guarantee that the prover will be able to show automatically that it is preserved by the next-state relation. If it isn't, you have to decompose the proof and find out what is needed. I did this for one of the conjuncts whose preservation is not proved automatically (Inv0') and found that the automatic proof fails for two actions. I then looked at one of those actions (ex2) and tried to understand why the invariant is preserved. Without knowing the algorithm or its pencil-and-paper proof, this took me quite a while even on paper. The essence is a counting argument, and if there is any automatic theorem prover that can find this proof, I'd like to hear about it. Attached is the TLAPS proof of that particular step. (It could probably be shortened somewhat.) The proof uses two unproved lemmas: - The first one asserts the existence of a minimal element in any set of natural numbers. This is fairly easy to prove from the theorems in the library module NaturalsInduction, and should indeed be provided by this module. - The second one asserts that for two positive natural numbers m and M such that m \in M-N+1 .. M-1 (where N is the constant from the specification), one cannot have m % N = M % N. Unfortunately, Z3 does not seem to know this (modulus arithmetic is not part of the decision procedure underlying Z3 but is handled heuristically). I don't know if the remaining steps are equally hard, you may want to give it a try if you are interested. Regards, 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/2BB6CDD6-7E28-4680-848A-8F49479372E7%40gmail.com. |

**Attachment:
AndersonMutex.tla**

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/2BB6CDD6-7E28-4680-848A-8F49479372E7%40gmail.com. |

**References**:**[tlaplus] Proving Mutual Exclusion of a simple algorithm using TLAPS***From:*Ugur Yagmur Yavuz

**[tlaplus] Re: Proving Mutual Exclusion of a simple algorithm using TLAPS***From:*Leslie Lamport

**Re: [tlaplus] Proving Mutual Exclusion of a simple algorithm using TLAPS***From:*Stephan Merz

**Re: [tlaplus] Proving Mutual Exclusion of a simple algorithm using TLAPS***From:*Ugur Yagmur Yavuz

- Prev by Date:
**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC** - Next by Date:
**Re: [tlaplus] Re: Temporal properties and index out of bounds** - Previous by thread:
**Re: [tlaplus] Proving Mutual Exclusion of a simple algorithm using TLAPS** - Next by thread:
**[tlaplus] TLC error** - Index(es):