How to use RandomElement

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

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