Confusion on document about definition override

[Shiyao MA]

Per here:

https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/model-values.html#values

The Toolbox will create the appropriate entry in that section when it creates a model if it finds a definition having the precise syntax above or the syntax
NotANat == CHOOSE n : ~(n \in Nat)

What does the above mean? Why does the toolbox create such an entry, why emphasize such an action? How is it related to model value?

Best, 

Thanks. 

[Andrew Helwer]

These "null" value definitions are very common in TLA+. They also aren't compatible with TLC, the finite model checker. You have to add a definition override which reassigns the null value label to a model value, basically a meaningless singleton object value which can only be checked for equality and is only equal to itself. Since it would be annoying to manually perform this definition override in every new model, the toolbox detects definitions of this type and automatically adds a definition override for these null values.

[Shiyao MA]

Thanks for your reply.

I would rather manually write in the cfg file with:

CONSTANT

NoValue = NoValue

Relying on the toolbox for that trick seems some extra redundant work.

[Andrew Helwer]

You are free to write the cfg file manually. This feature is only available to those using the toolbox.