# Re: [tlaplus] Reevaluations of operators in TLC

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

On Friday, 13 May 2022 at 21:51:06 UTC-3 Jones Martins wrote:
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.

On Friday, 13 May 2022 at 14:07:26 UTC-3 Markus Alexander Kuppe wrote:
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

> On May 13, 2022, at 9:58 AM, Jones Martins <jone...@xxxxxxxxx> wrote:
>
> 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

--
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.