[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: TLC may waste time evaluating unneeded operator definitions

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.

On Monday, August 12, 2013 2:27:04 AM UTC-8, Giuliano wrote:
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.