[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Fri, 13 Aug 2021 15:25:22 -0700*References*: <13e01362-450b-43b6-aa74-bb0118ab6757n@googlegroups.com>

On 8/13/21 6:12 AM, Victor Miraldo wrote:

I have some TLA+ spec that makes heavy use of functions and TLC takes along time (minutes) to check that even the simplest property, i.e.,`[](FALSE)`, doesn't hold. This made me question how TLC handlesfunctions, 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 itscalled 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`sin our generated code, such as the type of functions that receive listsand return lists.Unfortunately, I can't use operators here because these need to bepassed as arguments to mutually recursive operators.

Hi Victor,

Btw. for "very large sets", TLC usually errors with: Evaluating assumption line ... module ... failed. Attempted to construct a set with too many elements (>1000000).

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.

**Follow-Ups**:**Re: [tlaplus] How does TLC functions work under the hood?***From:*Victor Miraldo

**References**:**[tlaplus] How does TLC functions work under the hood?***From:*Victor Miraldo

- Prev by Date:
**[tlaplus] How does TLC functions work under the hood?** - Next by Date:
**Re: [tlaplus] How does TLC functions work under the hood?** - Previous by thread:
**[tlaplus] How does TLC functions work under the hood?** - Next by thread:
**Re: [tlaplus] How does TLC functions work under the hood?** - Index(es):