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

*From*: Victor Miraldo <victor.miraldo@xxxxxxxx>*Date*: Fri, 13 Aug 2021 06:12:03 -0700 (PDT)

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

--

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/13e01362-450b-43b6-aa74-bb0118ab6757n%40googlegroups.com.

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

- Prev by Date:
**Re: [tlaplus] Mutually Recursive Higher Order Terms Syntax Error** - Next by Date:
**Re: [tlaplus] How does TLC functions work under the hood?** - Previous by thread:
**Re: [tlaplus] Mutually Recursive Higher Order Terms Syntax Error** - Next by thread:
**Re: [tlaplus] How does TLC functions work under the hood?** - Index(es):