TLC evaluates constant definitions when it starts to avoid having to evaluate them billions of times when model checking the spec. Sometimes, this not what you want it to do. In that case, add an unused argument to the definition--e.g., writing
Def(x) == Expr
even though x does not appear in Expr.
Leslie
On Monday, August 12, 2013 2:27:04 AM UTC-8, Giuliano wrote:
Hello,
I recently got bad performance out of TLC for no apparent reason. Then I found out that my specification contained a definition of the form Def == Expr, where Expr was expensive to evaluate. Def was not used at all in the rest of my specification, however it seemed that TLC evaluated it anyway. After commenting it out, the performance of TLC was back to what I would expect.
So one should comment out unneeded definitions to prevent TLC from evaluating them.
Giuliano