Re: [tlaplus] Reevaluations of operators in TLC

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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 <jonesmvc@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/32D87D01-98BE-459D-AC00-935DD5C5A58A%40lemmster.de.