1

几天来，在各种情况下，我一直在 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
4

1 回答 1

3

TLC 无法评估 set 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 进行涉及无限集的证明。另见秒。14.2.3 在TLA+的第234--235 页上的“不要重新发明数学”部分。

于 2017-10-15T23:05:42.703 回答