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