TLA+ 工具箱运行模型时出错:覆盖值 Nat

Question

几天来，我在各种上下文中一直在TLA+工具箱中遇到以下错误：

"Attempted to compute the number of elements in the overridden value Nat.".

以下是我想出的最简单的模块，它将重现该问题。我已经看到一些被覆盖值的提及，但我看不出我如何在规范中做一些事情来导致这个问题。

有没有人看到错误，或者可以解释我错过了什么？

-------------------------------- MODULE foo --------------------------------
EXTENDS Naturals
VARIABLE Procs
Init == Procs = 1..5
Next == / Procs' = 1..5
Entries == [ i in Procs |-> [ j in {} |-> 0] ]
TypeOK == Entries in [ Procs -> [ (SUBSET Nat) -> Nat ] ]
=============================================================================

将 TypeOK 设置为不变量时，我收到完整的错误

Attempted to compute the number of elements in the overridden value Nat.
While working on the initial state:
Procs = 1..5

Answer 1

TLC不能计算集合Nat，因为它是无限的（另见被覆盖的模块Naturals.tla）。通过配置文件将Nat替换为有限集是一种可能的解决方法。

这样做之后，事实证明TypeOK FALSE，因为DOMAIN Entries = Procs，Procs # SUBSET Nat。换句话说，集合[ (SUBSET Nat) -> Nat]包含函数，每个函数的域等于SUBSET Nat。相反，可能打算的是域等于Nat的某个子集的函数集。这是在下面用TypeOKChanged完成的。

-------------------------------- MODULE foo --------------------------------
EXTENDS Naturals
VARIABLE Procs
Init == Procs = 1..5
Next == Procs' = 1..5
Entries == [ i in Procs |-> [ j in {} |-> 0] ]
TypeOK == Entries in [ Procs -> [ (SUBSET Nat) -> Nat ] ]
TypeOKChanged == Entries in [ Procs -> UNION {[Dom -> Nat]:  Dom in SUBSET Nat} ]
NatMock == 0..6
=============================================================================

和配置文件foo.cfg：

INIT Init
NEXT Next
CONSTANTS Nat <- NatMock
INVARIANT TypeOKChanged

输出为

$ tlc2 foo.tla
TLC2 Version 2.09 of 10 March 2017
Running in Model-Checking mode with 1 worker.
Parsing file foo.tla
Parsing file ~/tlatools/tla/tla2sany/StandardModules/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module foo
Starting... (2017-10-15 16:00:06)
Computing initial states...
Finished computing initial states: 1 distinct state generated.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 5.4E-20
  based on the actual fingerprints:  val = 1.1E-19
2 states generated, 1 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
Finished in 03s at (2017-10-15 16:00:09)

涉及无限集合Nat的证明可以用定理证明器TLAPS进行。另见TLA+书第234--235页第14.2.3节"不要重新发明数学"一节。