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

*From*: Victor Miraldo <victor.miraldo@xxxxxxxx>*Date*: Wed, 25 Aug 2021 03:01:31 -0700 (PDT)*References*: <13e01362-450b-43b6-aa74-bb0118ab6757n@googlegroups.com> <fec7ccd3-fbef-f08b-1ec5-6336cf2cace6@lemmster.de> <c6b53357-4f82-403a-856b-ff36a08360b3n@googlegroups.com>

After some back and forth between different encodings, I got to learn a little more TLA+ and would like to document my findings here.

> 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`?

As a good rule of thumb, avoiding TLA+ functions as much as possible is good. Doing that for generated code might involve working around the mutually recursive higher order operators in TLA+ problem.

Turns out that as long as your recursive calls do not change the higher-order operator being passed around, nested LET expressions work well:

entrypoint(Op(_,_),x,...) ==

LET RECURSIVE f1(...)

RECURSIVE f2(...)

f1(...) == ... Op(f2(....), ...)

f2(...) == ... Op(f1(...), ...)

IN f1(a,b,c,...)

I guess we're yet another person using the "feature" of recursive higher order operators in: https://github.com/tlaplus/tlaplus/issues/57 :)

Cheers,

Cheers,

Victor

On Monday, August 16, 2021 at 2:22:59 PM UTC+2 Victor Miraldo wrote:

Hello Markus,Thank you for the pointers! I'll follow through and try to understand what is going on.CheersVictorOn Saturday, August 14, 2021 at 12:25:35 AM UTC+2 Markus Alexander Kuppe wrote:

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/5ecd0134-241a-491f-a486-be32c43e3567n%40googlegroups.com.

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

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

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

- Prev by Date:
**Re: [tlaplus] Help with trivial spec: set generation** - Next by Date:
**[tlaplus] Model checker and GPU** - Previous by thread:
**Re: [tlaplus] How does TLC functions work under the hood?** - Next by thread:
**[tlaplus] Usage of brackets in TLC config file** - Index(es):