# How does TLC functions work under the hood?

62 views

### Victor Miraldo

Aug 13, 2021, 9:12:03 AMAug 13
to tlaplus
Hello all,

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

Thanks,
Victor

### Markus Kuppe

Aug 13, 2021, 6:25:35 PMAug 13
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

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

### Victor Miraldo

Aug 16, 2021, 8:22:59 AMAug 16
to tlaplus
Hello Markus,

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

Cheers
Victor

### Victor Miraldo

Aug 25, 2021, 6:01:31 AMAug 25
to tlaplus
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