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

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

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/fec7ccd3-fbef-f08b-1ec5-6336cf2cace6%40lemmster.de.