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

Dear Leslie,

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

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.

Leslie

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.

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.