Re: [tlaplus] How does TLC functions work under the hood?

[Victor Miraldo <victor.miraldo@xxxxxxxx>]

After some back and forth between different encodings, I got to learn a little more TLA+ and would like to document my findings here.

> When I write [ x \in TypeX |-> f(x) ], is TLC generating all elements in `TypeX` then computing their image under `f` or does it wait until its called with an argument `m` to compute its image under `f`?

Yes, TLA+ does enumerate the domain of functions before computing the point in the image. This incurred a ridiculous overhead. We've seen a speedup from 4m46s to 12s to check a silly invariant. :)

As a good rule of thumb, avoiding TLA+ functions as much as possible is good. Doing that for generated code might involve working around the mutually recursive higher order operators in TLA+ problem.

Turns out that as long as your recursive calls do not change the higher-order operator being passed around, nested LET expressions work well:

entrypoint(Op(_,_),x,...) ==

  LET RECURSIVE f1(...)

          RECURSIVE f2(...)

          f1(...) == ... Op(f2(....), ...)

          f2(...) == ... Op(f1(...), ...)

    IN f1(a,b,c,...)

I guess we're yet another person using the "feature" of recursive higher order operators in: https://github.com/tlaplus/tlaplus/issues/57  :)

Cheers,

Victor

On Monday, August 16, 2021 at 2:22:59 PM UTC+2 Victor Miraldo wrote:

Hello Markus,

Thank you for the pointers! I'll follow through and try to understand what is going on.

Cheers

Victor

On Saturday, August 14, 2021 at 12:25:35 AM UTC+2 Markus Alexander Kuppe wrote:

On 8/13/21 6:12 AM, Victor Miraldo wrote:
> I have some TLA+ spec that makes heavy use of functions and TLC takes a
> long time (minutes) to check that even the simplest property, i.e.,
> `[](FALSE)`, doesn't hold. This made me question how TLC handles
> functions, but I can't find information elsewhere.
>
> When I write [ x \in TypeX |-> f(x) ], is TLC generating all elements in
> `TypeX` then computing their image under `f` or does it wait until its
> called with an argument `m` to compute its image under `f`?
>
> Is there a way to make TLA+ lazy, preventing it from ever generating
> `TypeX` in its entirety? Unfortunately we have some very large `TypeX`s
> in our generated code, such as the type of functions that receive lists
> and return lists.
>
> Unfortunately, I can't use operators here because these need to be
> passed as arguments to mutually recursive operators.



Hi Victor,

I'd suggest to debug TLC [1] (look for tlc2.value.impl.FcnRcdValue), but
the Toolbox's profiler [1] might be good enough to find out what is
going on. Also, the TLA+ debugger [3] could help you introspect.

Btw. for "very large sets", TLC usually errors with:

Evaluating assumption line ... module ... failed.
Attempted to construct a set with too many elements (>1000000).

Since doesn't error out on you, you should ensure you're not chasing a
red herring.

M.

[1] https://github.com/tlaplus/tlaplus/tree/master/general/ide
[2] https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/profiling.html
[3] https://youtu.be/6oMQYHogQek

-- 
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/5ecd0134-241a-491f-a486-be32c43e3567n%40googlegroups.com.