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

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

Dear Leslie,

Thanks for your reply.
Now I understand "SV!<".

So, the real bug here is that the Toolbox (Version 1.6.0 of 10 July 2019) reports a parse error on `maxBal[p] SV!< b`; see the attached .png file (I failed to insert it in the text here.)

See also the attached TLA+ Specs files (SimpleVoting.tla, Record.tla) for the line numbers referred to in the error message.

Best regards,

On Tuesday, August 20, 2019 at 12:59:21 AM UTC+8, Leslie Lamport wrote:

 Stephan wrote:

   please feel free to post a bug report about the malfunctioning proof decomposition.

I do not see any malfunction of the proof decomposition command.  The command is expanding the 
definition of  SV!IncreaseMaxBal(p, b).  The definition of IncreaseMaxBal in module SimpleVoting
uses the operator < (imported from the Naturals module), which is imported by the INSTANCE statement 
as the operator SV!< .  Since the module containing the theorem also imports the Naturals module,
the operator SV!< happens to equal the operator < of the current module.  Please replace < by SV!< 
in the proof and check that it still works.  If it doesn't, please report this as a TLAPS bug.  

Because the definition of < is imported into the instantiated module from a standard module, and 
that same definition is imported into the instantiating module from the same standard module, a
user would almost always prefer that the Decompose Proof command replace SV!< by < .  This should
be straightforward to implement and we would be grateful if someone would volunteer to do it.


On Wednesday, August 14, 2019 at 9:26:22 PM UTC-7, Hengfeng Wei wrote:
Dear All,

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


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 ----------------------------


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

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 -------------------------------
Naturals, TLAPS
Participant  \* the set of partipants

\* 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]

== 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?
       NEW VARIABLE state
\in Participant,
\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,

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/2f6de7b9-964f-4976-a1a2-1d9eeba61f2c%40googlegroups.com.

Attachment: tlaps-proof-decomposition-parse-error.png
Description: PNG image

Attachment: SimpleVoting.tla
Description: Binary data

Attachment: Record.tla
Description: Binary data