Re: How to use RandomElement

[marc magrans de abril <marcmagra...@xxxxxxxxx>]

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

On Friday, June 14, 2013 1:02:07 PM UTC+2, Dominik Hansen wrote:

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