TLA +工具箱錯誤運行模式：重寫值納特

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，因爲它是無限的（另見overridden module Naturals.tla）。通過配置文件替換Nat有限集合是一種可能的解決方法。

這樣做後，事實證明TypeOK是FALSE，因爲DOMAIN Entries = Procs和Procs # SUBSET Nat。換句話說，集合[ (SUBSET Nat) -> Nat]包含各自具有域等於至SUBSET 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追究一個證明。另見Sec。在TLA+ book部分"Don't Reinvent Mathematics"的第234--235頁上的14.2.3。