[tlaplus] Confusion on document about definition override

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bb7fb92a-9ac5-4d42-a70b-ed03f0c1ff53%40googlegroups.com.