Re: How to use RandomElement

[Dominik Hansen <do.han...@xxxxxxxxxxxxxx>]

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