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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 8 Apr 2019 09:21:37 +0200*References*: <CAFteovLcZfO682KYJ=Kefb+1sV2U_X5yvDdQ9M2qc-ytXwfrFQ@mail.gmail.com>

Hello, there are two problems: the fundamental one is that what you are trying to prove is not true. Use TLC to check the temporal property [][\A p \in P : v[p] # NV /\ Next => v = v']_v (which is what step <1>3 asserts) for sets of model values P <- {pp, qq} and V <= {a, b} and have a look at the counter-example. It is all too easy to get carried away by what looks like a good idea; use TLC as extensively as you can to make sure that what you are trying to prove actually has a chance of being true. The second one is that you wrongly identify the peer p that appears in the invariant and the peer pp that appears in the definition of Act1. That's why TLAPS rejects the proof of step <2>q – you showed the assertion only for Act1!(p,vv), but you need to prove it for Act1!(pp,vv), for some arbitrary pp \in P. Below is a proof of your invariant. I needed to assume the type correctness invariant so that the proof for the EXCEPT _expression_ went through. For your reduction to work, you'll also have to establish that NV \notin V – the TLAPS module contains a utility lemma to that effect. Regards, Stephan ––– THEOREM TypeOK => StableIndInv
-- <1>1. SUFFICES ASSUME NEW p \in P, v[p] # NV, Next, TypeOK PROVE v[p] = v'[p] BY DEF StableIndInv <1>4. CASE Act1 <2>1. ASSUME NEW pp \in P, NEW vv \in V, Act1!(pp,vv) PROVE v[p] = v'[p] <3>1. CASE p = pp BY <3>1, <2>1, <1>1 <3>2. CASE p # pp BY <3>2, <2>1, <1>1 DEF TypeOK <3>q. QED BY <3>1, <3>2 <2>q. QED BY <1>4, <2>1 DEF Act1 <1>5. CASE Act2 BY <1>5 DEF Act2 <1>q. QED BY <1>1, <1>4, <1>5 DEF Next LEMMA NV_not_V == NV \notin V BY NoSetContainsEverything DEF NV
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

**Follow-Ups**:**Re: [tlaplus] TLAPS, first steps***From:*Karolis Petrauskas

**References**:**[tlaplus] TLAPS, first steps***From:*Karolis Petrauskas

- Prev by Date:
**[tlaplus] TLAPS, first steps** - Next by Date:
**Re: [tlaplus] TLAPS, first steps** - Previous by thread:
**[tlaplus] TLAPS, first steps** - Next by thread:
**Re: [tlaplus] TLAPS, first steps** - Index(es):