Re: [tlaplus] Re: How to use RandomElement

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,
marc

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

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