Модель запуска ошибки 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. Смотрите также гл. 14.2.3 на страницах 234-235 книги TLA+ раздел "Не переизобретай математику".