theorem-proving - 如何完成涉及记录的细化映射的 TLAPS 证明？

Question

我在证明涉及记录的细化映射时遇到了一些困难。下面是TLA 规范@github 的简化说明（请注意，这篇文章也在tlaplus-googlegroup 中，还没有回复。）：

---

SimpleVoting.tla:

它为每个参与者维护maxBal一个自然数。在IncreaseMaxBal(p, b)，maxBal[p]被增加到一个更大的值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:

它维护一个二维“数组” state，其中state[p][q]是q从视图的状态，p而状态是记录： State == [maxBal : Nat, maxVBal : Nat]。

在Prepare(p, b)，state[p][p].maxBal被增加到一个更大的值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
---------------------------------------------------------------------------

---

直观地，Record维持as 。因此，我想在以下细化映射下显示细化：maxBal[p]SimpleVotingstate[p][p].maxBalRecordSimpleVoting

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

SV == INSTANCE SimpleVoting

但是，<3>2以下证明中的步骤失败。

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> SUFFICES ASSUME NEW p \in Participant, NEW b \in Nat,
                          Prepare(p, b)
                   PROVE  SV!IncreaseMaxBal(p, b)
        BY DEF Next, SV!Next
      <3>1. maxBal[p] < b
        BY DEF Prepare, maxBal
      <3>2. maxBal' = [maxBal EXCEPT ![p] = b] \* failed here!
        BY DEF Prepare, maxBal
      <3>3. QED
        BY <3>1, <3>2 DEF SV!IncreaseMaxBal
    <2>3. QED
      BY <2>1, <2>2
  <1>3. QED

义务<3>2如下。假设中的不state' = [state EXCEPT ![p] = ...]与结论相同[p_1 \in Participant |-> state[p_1][p_1].maxBal]' ...吗？什么不见​​了？我的证明有什么问题？

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]

标签： theorem-provingtla+tlaps