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

*From*: TLA Plus <tlapl...@xxxxxxxxx>*Date*: Sat, 15 Jun 2013 09:17:00 -0800*References*: <ad7864c5-38a0-495a-9fa5-bc4d92d86fac@googlegroups.com> <49911de5-80b6-49a3-b932-4fc8e158e0dd@googlegroups.com> <d13fbfd5-07f1-48d7-a635-0537474c87f4@googlegroups.com> <528ad9b4-0daa-4c33-938c-1332d9a006f8@googlegroups.com>

Hi Marc,

TLC was written to evaluate TLA+ specifications.

It uses various optimizations that take advantage

of mathematical properties--for example, that

no matter how many times an _expression_ is

evaluated, it always returns the same result. For

various reasons, certain hacks have been added to

make TLC act as if it were not evaluating

mathematics and were instead executing a

programming language. These interact in strange

ways with TLC's optimizations. While there were

good reasons to add these hacks, they are not good

enough to subvert TLC's main purpose: to evaluate

TLA+ specifications as efficiently as possible.

When using those hacks, you will just have to

learn to live with their strange behavior.

Dominik Hansen has explained one of TLC's

optimizations: trying to compute constant

expressions only once. It therefore (usually)

precomputes definitions of the form

identifier == constant _expression_

I'm not sure if it does the same thing for LET

definitions, or only computes the value with the

first use of the definition. You can experiment

to find out what it does for LETs. As Dominik

pointed out, you can prevent this once-only

computation by giving the defined operator an

argument.

Another thing that TLC often does is lazy

evaluation, not evaluating an _expression_ until it

needs the _expression_'s value. For recursive

definitions, this can be a pessimization. It

could also lead to problems when trying to use

RandomElement. The operator TLCEval has been

added to the TLC module to cause eager evaluation.

See its description in the document "Current

Versions of the TLA+ Tools".

Leslie

**Follow-Ups**:**Re: [tlaplus] Re: How to use RandomElement***From:*marc magrans de abril

**References**:**How to use RandomElement***From:*marc magrans de abril

**Re: How to use RandomElement***From:*Dominik Hansen

**Re: How to use RandomElement***From:*marc magrans de abril

**Re: How to use RandomElement***From:*Dominik Hansen

- Prev by Date:
**Re: How to use RandomElement** - Next by Date:
**Re: [tlaplus] Re: How to use RandomElement** - Previous by thread:
**Re: How to use RandomElement** - Next by thread:
**Re: [tlaplus] Re: How to use RandomElement** - Index(es):