Reevaluations of operators in TLC

[Jones Martins]

Hi everyone,

When evaluating operators, does TLC memoize its results?

For example, the classic Fibonacci, we'd have recursive operators:

RECURSIVE Fibonacci(_)

Fibonacci(N) ==

  IF N <= 1

  THEN 1

  ELSE Fibonacci(N - 1) + Fibonacci(N - 2)

Or, between actions:

Next1 == 

  /\ SlowOperator()

  /\ FALSE

  /\ ...

Next2 ==

  /\ SlowOperator()

  /\ TRUE

  /\ ...

Next == Next1 \/ Next2

This is an absurd example. I just wanted to have SlowOperator be applied in different actions.

Jones

[Markus Kuppe]

Hi Jones,

the TLA+ Toolbox profiler [1] can answer questions like this.

Markus

[1] https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/profiling.html

[Jones Martins]

Thanks, Markus!

And to answer my question in case anyone's curious:

The closest thing to memoizing is using a function instead of an operator.

I suppose memoizing manually might be a good choice, although I haven't tested its performance compared to the other approaches.

[Jones Martins]

In case anyone else reads this thread, the closest thing to memoization while model checking is the TLCEval operator in the TLC module.

I had a model check go from 20 minutes to 6 minutes just by using TLCEval in a couple of spots.

But to know such spots, I had to profile first, as Markus recommended: https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/profiling.html 

TLC module: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLC.tla