问题标签 [tlaps]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
vim - 我如何从 vim 运行 cygwin
TLA 的证明者需要 Cygwin，我想tlapm.exe在 Gvim 中运行它（例如），如何从 vimscript 程序启动 cygwin
在 TLA 工具箱中，按如下方式对其进行评估：
concurrency - 简单并发程序的归纳不变量是什么？
这是Leslie Lamport的文章教学并发中的一个简单的并发程序。
考虑N从 0 到N-1每个进程i执行的进程
并停止，每个x[i]初始等于 0。（每个的读取和写入x[i]都假定是原子的。）
该算法满足以下性质：在每个进程停止后，y[i]至少有一个进程等于 1 i。很容易验证：最后i写入的进程y[i]必须设置为 1。
然后，兰波特评论说
但是该进程没有设置
y[i]为 1，因为它是最后一个 write 进程y。该算法满足此属性，因为它保持一个归纳不变量。你知道那个不变量是什么吗？如果不是，那么您并不完全理解该算法为什么满足此属性。
所以，
并发程序的归纳不变量是什么？
theorem-proving - 如何完成涉及记录的细化映射的 TLAPS 证明？
我在证明涉及记录的细化映射时遇到了一些困难。下面是TLA 规范@github 的简化说明（请注意，这篇文章也在tlaplus-googlegroup 中，还没有回复。）：
SimpleVoting.tla:
它为每个参与者维护maxBal一个自然数。在IncreaseMaxBal(p, b)，maxBal[p]被增加到一个更大的值b。
Record.tla:
它维护一个二维“数组” state，其中state[p][q]是q从视图的状态，p而状态是记录：
State == [maxBal : Nat, maxVBal : Nat]。
在Prepare(p, b)，state[p][p].maxBal被增加到一个更大的值b。
直观地，Record维持as 。因此，我想在以下细化映射下显示细化：maxBal[p]SimpleVotingstate[p][p].maxBalRecordSimpleVoting
但是，<3>2以下证明中的步骤失败。
义务<3>2如下。假设中的不state' = [state EXCEPT ![p] = ...]与结论相同[p_1 \in Participant |-> state[p_1][p_1].maxBal]' ...吗？什么不见了？我的证明有什么问题？