TLA+ toolbox error running model: overridden value Nat

Question

I've been hitting the following error in TLA+ toolbox for a few days now in various contexts:

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

The following is the simplest module that I've come up with that will reproduce the issue. I've seen some mention of overridden values, but I can't see how I'm doing something in the spec to cause this issue.

Does anyone see the error, or can explain what I'm missing?

-------------------------------- 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 ] ]

=============================================================================

When setting TypeOK to the invariant, I get the full error

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

Answer 1

TLC cannot evaluate the set Nat, because it is infinite (see also the overridden module Naturals.tla). Replacing Nat with a finite set via the configuration file is one possible workaround.

After doing so, it turns out that TypeOK is FALSE, because DOMAIN Entries = Procs, and Procs # SUBSET Nat. In other words, the set [ (SUBSET Nat) -> Nat] contains functions each of which has domain equal to SUBSET Nat. Instead, what was probably intended is the set of functions with domain equal to some subset of Nat. This is done below with 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
=============================================================================

and the configuration file foo.cfg:

INIT Init
NEXT Next

CONSTANTS Nat <- NatMock
INVARIANT TypeOKChanged

The output is

$ 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)

A proof involving the infinite set Nat can be pursued with the theorem prover TLAPS. See also Sec. 14.2.3 on pages 234--235 of the TLA+ book the section "Don't Reinvent Mathematics".