How does TLC functions work under the hood?

[Victor Miraldo]

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

Thanks,

Victor

[Markus Kuppe]

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

[Victor Miraldo]

Hello Markus,

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

Cheers

Victor

[Victor Miraldo]

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