天道酬勤,学无止境

tlaps

如何完成涉及记录的细化映射的 TLAPS 证明?(How to finish the TLAPS proof for a refinement mapping involving records?)

问题 我很难证明涉及记录的细化映射。 以下是 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'

2021-10-25 06:50:43    分类:技术分享    theorem-proving   tla+   tlaps

How to finish the TLAPS proof for a refinement mapping involving records?

I have some difficulty in proving a refinement mapping involving records. Below are the simplified illustrating TLA specs@github (Note that this post is also in tlaplus-googlegroup, without replies yet.): 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

2021-09-29 14:58:35    分类:问答    theorem-proving   tla+   tlaps