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

*From*: Hengfeng Wei <hengxin0912@xxxxxxxxx>*Date*: Mon, 19 Aug 2019 20:02:11 -0700 (PDT)*References*: <104baa52-4929-42c4-9c5f-dd9ddfe559ae@googlegroups.com> <BA505F11-C0A0-48F8-A2BE-65939F2DA92E@gmail.com>

Hi Stephan,

-- I got it now. Thanks for your help.

Best regards,

hengxin

On Monday, August 19, 2019 at 5:01:31 PM UTC+8, Stephan Merz wrote:

On Monday, August 19, 2019 at 5:01:31 PM UTC+8, Stephan Merz wrote:

Hello Hengxin,please feel free to post a bug report about the malfunctioning proof decomposition.Concerning the failure of step <4>2, you need to invoke the type invariant so that the provers can determine the shape of the function `state'. In particular, you have [f EXCEPT ![x] = ...] = f if x is not an element of DOMAIN f (in your case you have a complicated EXCEPT clause involving a two-dimensional array of records). As a rule of thumb, the type invariant is always necessary when reasoning about EXCEPT expressions.This requires introducing the type invariant in the step simulation part of the proof. Fortunately, you can rely on the type-correctness theorem and PTL checks that this is okay. The refinement proof becomes (see also the attached TLA+ module):THEOREM Spec => SV!Spec

<1>1. Init => SV!Init

BY DEF Init, SV!Init, maxBal, InitState

<1>2. TypeOK /\ [Next]_state => [SV!Next]_maxBal

<2>1. UNCHANGED state => UNCHANGED maxBal

BY DEF maxBal

<2>2. TypeOK /\ Next => SV!Next

<3> ASSUME NEW p \in Participant, NEW b \in Nat,

TypeOK, Prepare(p, b)

PROVE SV!IncreaseMaxBal(p, b) \* SV!Next

<4>1. maxBal[p] < b \* Wrong decomposition: maxBal[p] SV!< b

BY DEF Prepare, maxBal

<4>2. maxBal' = [maxBal EXCEPT ![p] = b]

BY Zenon DEF Prepare, maxBal, TypeOK, State

<4>3. QED

BY <4>1, <4>2 DEF SV!IncreaseMaxBal

<3>1. QED

BY DEF Next, SV!Next

<2>3. QED

BY <2>1, <2>2

<1>3. QED

BY <1>1, <1>2, Invariant, PTL DEF SV!Spec, Specand it is checked by TLAPS. (The explicit invocation of Zenon in step <4>2 is not necessary but it documents which backend found the proof and avoids waiting for SMT to timeout.)Best 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/96605c35-b2a7-454b-8520-e44ede772837%40googlegroups.com.

**References**:

- Prev by Date:
**[tlaplus] Re: Help with a TLAPS proof for a refinement involving records (and a Proof Decomposition bug)** - Next by Date:
**Re: [tlaplus] Any instructions on when and how to explicitly specify backend provers in TLAPS proofs?** - Previous by thread:
**Re: [tlaplus] Help with a TLAPS proof for a refinement involving records (and a Proof Decomposition bug)** - Next by thread:
**[tlaplus] Re: Help with a TLAPS proof for a refinement involving records (and a Proof Decomposition bug)** - Index(es):