How to use RandomElement

[marc magrans de abril]

Yesterday, I was trying the RandomElement macro of the TLC module, and I found that it was not behaving as I expected. As usual, it was just my lack of understanding of TLA:P 

Still, I would like to know how could I achieve what I initially expected with or without RandomElement.

For example, the specification at the end of the post defines "i==RandomElement(1..100)" within a LET/IN clause. If "i" is used in two different places, then it will be expanded and evaluated twice. This will give to the macro "i" two different values. This seems to be consistent with the TLA+ language.

Notice, that using "i==TLCEval(RandomElement(1..100))" does not help, because the macro is expanded twice.

If I use instead "\E k \in 1..100): i' = k" or "i' = RandomElement(1..100)", it requires an extra variable "i" in the spec.

If I use instead "i == CHOOSE i \in 1..100: TRUE", I will get always the same number.

The questions are:

* How can I use the same RandomElement several times in a given action?

* Is it possible to avoid having another variable in the spec?
* Can I use an alternative mechanism to achieve a similar functionality? 

Thanks for the help!

--------------------------- MODULE RandomElement ---------------------------
EXTENDS Integers,TLC
VARIABLES x,y

Init == /\ x=0
          /\ y=0 
Next == LET i == RandomElement(1..100) 
             IN 
             /\ x' = i 
             /\ y' = i 

Inv == x=y
=============================================================================

[Dominik Hansen]

Hi Marc,

if you want to use the same random element at different places and you want to avoid an action like "Next == x' = RandomElement(1..100) /\ y' = x' " you can bind the random element to a variable of a quantification:

--------------------------- MODULE RandomElement ---------------------------

EXTENDS Integers,TLC 

VARIABLES x,y 

Init == /\ x=0 

        /\ y=0

Next ==  /\ \E i \in { RandomElement(1..100) }: PrintT(i) /\ x' = i /\ y' = i 

Inv == x=y 

=============================================================================

But the behavior of TLC by evaluation the RandomElement operator isn't always obvious. The description of the operator in current-tools.pdf says that "RandomElement(S) = RandomElement(S)" could be evaluated to FLASE.  However, if I substitute the calls of the RandomElement operator by an additional definition it will be always evaluated to TRUE:

i == RandomElement(1..100) 

ASSUME i = i

This behavior is probably caused by the fact that TLC treats the definition "i" as a constant expression and evaluates the definition only once.

TLC's behavior also leads to tiny detail in my specification above: I added the conjunction operator "/\" at the beginning of the Next definition otherwise TLC would evaluate the expression "{RandomElement(1..100)}" only once. In this case the reason is more subtle. In presence of the conjunction operator TLC treats the Next definition as a single action because TLC can't split a conjunction into separate actions. If there is no conjunction TLC tries to split the body of the existential quantification into separate actions and handles the bounded variables in a different way (evaluating the expression only once).

I'm not sure if it is a desired behavior or a bug.

Dominik

[marc magrans de abril]

Hi Dominik,

Still, I do not fully understand the behavior. I'll try to explain my doubts...

1) In the hyperbook it says " In TLA+ , a definition is simply an abbreviation." (p. 21). However, as you point out the following action results in the invariant "x=y":
i==RandomElement(MYSET)
Pair == /\ x' = i
            /\ y' = i

2) In the hyperbook there is also the example definition of RandomRanking(S). This leads to the invariant "(Len(x) = Cardinality(MYSET)) /\ (\E j \in 1..Len(x): x[j] \in MYSET)". This suggests that RandomElement is just evaluated once per recursion level.

RECURSIVE RandomRanking(_)
RandomRanking(S) == IF S = {} THEN 
                                  << >> 
                                  ELSE 
                                  LET e == RandomElement(S) 
                                  IN 
                                  <<e>> \o RandomRanking(S \ {e})
Ranking == x' = RandomRanking(MYSET)

3) Finally, in the initial example I sent the invariant "x=y" fails. In this case RandomElement is evaluated twice.

Next == LET i == RandomElement(1..100) 
             IN 

             /\ x' = i 
             /\ y' = i 

Thanks for your help, 

marc

[Dominik Hansen]

I think the inconsistent behavior of TLC by the evaluating RandomElement operator is caused by TLC's caching techniques.

In the following example the first local definition is evaluated once and the second twice.

ASSUME LET i == IF PrintT("first") THEN RandomElement(1..100) ELSE FALSE IN i = i

ASSUME LET i(j) == IF PrintT("second") THEN RandomElement(1..100) ELSE FALSE IN i(1) = i(1)

As a result the first assumption is always TRUE and the second is almost always FALSE. In the second case the parameter "j" seems to prevent TLC from caching the value of the definition even though the parameter doesn't affect the value.

My explanation for this behavior is that the expression "RandomElement(1..100)" has level 0 (constant-level, cf. 17.2 of Specifying Systems) and underlies TLC's (complex) caching techniques. In my opinion a value of a expression containing the RandomElement operator shouldn't be cached to avoid such an inconsistent behavior.

[TLA Plus]

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

[marc magrans de abril]

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

[TLA Plus]

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

--

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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.