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

[Victor Miraldo <victor.miraldo@xxxxxxxx>]

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.