Thank you for the pointers! I'll follow through and try to understand what is going on.
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