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

[tlaplus] Help with a TLAPS proof for a refinement involving records (and a Proof Decomposition bug)



Dear All,

I have some difficutlty in proving a refinement mapping involving records.
Below are the simplified TLA specs (see also the attached files):

SimpleVoting.tla:

It maintains for each participant a `maxBal` which is a natural number.
In IncreaseMaxBal(p, b), maxBal[p] is increased to a larger value b.
---------------------------- MODULE SimpleVoting ----------------------------
EXTENDS
Naturals
-----------------------------------------------------------------------------
CONSTANT
Participant

VARIABLE maxBal

TypeOK == maxBal \in [Participant -> Nat]
-----------------------------------------------------------------------------
Init == maxBal = [p \in Participant |-> 0]

IncreaseMaxBal(p, b) ==
 
/\ maxBal[p] < b
  /
\ maxBal' = [maxBal EXCEPT ![p] = b]
-----------------------------------------------------------------------------
Next == \E p \in Participant, b \in Nat : IncreaseMaxBal(p, b)

Spec == Init /\ [][Next]_maxBal
=============================================================================

Record.tla:
It maintains a 2D array `state`. `state[p][q]` is the State of q from the view of p and a State is a record:
State == [maxBal : Nat, maxVBal : Nat].

In Prepare(p, b): state[p][p].maxBal is increased to a larger value b.
------------------------------- MODULE Record -------------------------------
EXTENDS
Naturals, TLAPS
---------------------------------------------------------------------------
CONSTANTS
Participant  \* the set of partipants

VARIABLES state
\* state[p][q]: the state of q \in Participant from the view of p \in Participant
   
 
State == [maxBal: Nat, maxVBal: Nat]

TypeOK == state \in [Participant -> [Participant -> State]]
---------------------------------------------------------------------------
InitState == [maxBal |-> 0, maxVBal |-> 0]

Init == state = [p \in Participant |-> [q \in Participant |-> InitState]]
 

Prepare(p, b) ==
   
/\ state[p][p].maxBal < b
    /
\ state' = [state EXCEPT ![p][p].maxBal = b]
---------------------------------------------------------------------------
Next == \E p \in Participant, b \in Nat : Prepare(p, b)

Spec == Init /\ [][Next]_state
---------------------------------------------------------------------------

I want to show that Record refines SimpleVoting under the refinement mapping:

maxBal == [p \in Participant |-> state[p][p].maxBal]

SV
== INSTANCE SimpleVoting

However, step <4>2 fails (more details below). (In addition, the proof decomposition (Ctrl+G, Ctrl+D) of <3> generates a buggy formula "maxBal[p] SV!< b" in <4>1, which should be "maxBal[p] < b".)

THEOREM Spec => SV!Spec
 
<1>1. Init => SV!Init
    BY DEF
Init, SV!Init, maxBal, InitState
 
<1>2. [Next]_state => [SV!Next]_maxBal
   
<2>1. UNCHANGED state => UNCHANGED maxBal
      BY DEF maxBal
   
<2>2. Next => SV!Next
     
<3> ASSUME NEW p \in Participant, NEW b \in Nat,
                 
Prepare(p, b)
          PROVE  SV
!IncreaseMaxBal(p, b) \* SV!Next
       
<4>1. maxBal[p] < b \* Wrong decomposition here: maxBal[p] SV!< b
          BY DEF
Prepare, maxBal
       
<4>2. maxBal' = [maxBal EXCEPT ![p] = b]
          BY DEF Prepare, maxBal \* Failed here!!!
        <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, PTL DEF SV!Spec, Spec

The obligation at <4>2 is as follows. Isn't the `state' = [state EXCEPT ![p] = ...]` in the assumption the same as the conclusion `[p_1 \in Participant |-> state[p_1][p_1].maxBal]' ...`? What is wrong with my proof? How should I proceed?
 
ASSUME NEW CONSTANT Participant,
       NEW VARIABLE state
,
       NEW CONSTANT p
\in Participant,
       NEW CONSTANT b
\in Nat,
       
/\ state[p][p].maxBal < b
       /
\ state'
          = [state EXCEPT
               ![p] = [state[p] EXCEPT
                         ![p] = [state[p][p] EXCEPT !.maxBal = b]]]
PROVE  [p_1 \in Participant |-> state[p_1][p_1].maxBal]'

       
= [[p_1 \in Participant |-> state[p_1][p_1].maxBal] EXCEPT ![p] = b]

Best regards,
hengxin

--
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/104baa52-4929-42c4-9c5f-dd9ddfe559ae%40googlegroups.com.

Attachment: Record.tla
Description: Binary data

Attachment: SimpleVoting.tla
Description: Binary data