Re: [tlaplus] Reevaluations of operators in TLC

[Jones Martins <jonesmvc@xxxxxxxxx>]

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/78460308-0c77-47a9-886c-a188dfabe82dn%40googlegroups.com.