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

*From*: TLA Plus <tlapl...@xxxxxxxxx>*Date*: Sun, 16 Jun 2013 01:40:55 -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> <CAAWQ4M5_JH23tLtf_mUWXq29C5FwOTubyG6VCah_goSQ_8HeqA@mail.gmail.com> <e1891167-1c0a-4052-b77e-cfa564cbedbb@googlegroups.com>

Hi Marc and Dominik,

Section 19.3 of the hyperbook is about how TLC evaluates expressions.

As explained in the secion of Specifying Systems that describes how TLC

computes behaviors, TLC does not simply evaluate the next-state action.

(How could it, when the next-state action contains primed variables and

TLC is trying to compute possible values of the primed variables?)

To see what's going on, try these two next-state actions:

Next == /\ x' = LET i == RandomElement(1..10)

IN <<i, i>>

/\ PrintT(x)

Next == LET i == RandomElement(1..10)

IN /\ x' = <<i, i>>

/\ PrintT(x)

Leslie

On Sat, Jun 15, 2013 at 1:53 PM, marc magrans de abril <marcmagra...@xxxxxxxxx> wrote:

Hi Leslie and Dominik,Now I understand better the limits and applicability of the RandomElement. I will try to avoid it from the specs when possible and use instead the existential quantification (e.g. as pointed out earlier, an alternative could be something like "\E k \in MYSET: x' = k").

Regarding the TLCEval operator, I was already aware of it (Leslie posted the link to the current-tools.pdf in another thread). Unfortunately, when I used the operator in combination with RandomElement, it didn't behave as I expected.For example, I have defined an action either like:

Pair == LET i==RandomElement(MYSET)

IN

/\ x' = TLCEval(i)

/\ y' = TLCEval(i)

or like:

Pair == LET i==RandomElement(MYSET)

IN

/\ x' = TLCEval(i)

/\ y' = TLCEval(i)In both cases the invariant "x=y" fails.Should this behavior be considered as a strange interaction between the optimization heuristics and the RandomElement operator? If I read by the letter the section 19.3 of the hyperbook it does not seem so:>>If multiple instances of the same subexpression occur in an _expression_ e , TLC will evaluate that subexpression multiple times when evaluating e . This multiple evaluation can be avoided by using a LET to replace those instances by a single symbol.This comment seems to imply that LET should not behave like a macro mechanism, but like a local assignment that is only evaluated once.

In any case, I hope that the comments above didn't sound as a complain. The process of understanding TLA+ and the toolbox are helping me to think more precisely about concurrency and distributed systems.I really appreciate the toolset and the effort you are putting on it.--Cheers,marcOn Saturday, June 15, 2013 7:17:00 PM UTC+2, Leslie Lamport wrote:

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 formidentifier == 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

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+u...@xxxxxxxxxxxxxxxx.

To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

Visit this group at http://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/groups/opt_out.

**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

**Re: [tlaplus] Re: How to use RandomElement***From:*TLA Plus

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

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