[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] How does TLC functions work under the hood?
- From: Victor Miraldo <victor.miraldo@xxxxxxxx>
- Date: Fri, 13 Aug 2021 06:12:03 -0700 (PDT)
- Ironport-hdrordr: A9a23:brg6mKN0g0WWT8BcTl6jsMiBIKoaSvp037BL7TEKdfUxSKb0qynApoV+6faZskd3ZJnP8erwTJVpbxvnhOtICMoqTMaftDCPghrbEGga1/qU/9SCIVyEygbpvp0QDZSWdueAdGSS1vyKnzVQeuxIqLL3kpxA492us0uFYjsEV0gK1XYANu/0KDwReOGGbaBJd6Z0JfAom9NjQxgqhnTRPAh3YwEOnbz2fGKMW296O/fv0mn+6A+A2frBChCdmj0eXzlMzbpn0W+AvRf++rzLiYDK9iPh
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.
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.