After adding new operator that uses CHOOSE, like
NullData == CHOOSE x : x \notin Data
TLC Model Checker may report type invariant violations in existing models. The problem is that TLC Model Checker does not pick up new NullData operator. To fix the problem, NullData needs to be added by hand to Definition Overrides with Model Value set as NullData's value.
NullData == CHOOSE x : x \notin Data
TLC Model Checker may report type invariant violations in existing models. The problem is that TLC Model Checker does not pick up new NullData operator. To fix the problem, NullData needs to be added by hand to Definition Overrides with Model Value set as NullData's value.
