Re: [tlaplus] How to make a concrete value from RandomElement?

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 09.08.2018 00:24, Qd Wang wrote:
> ```
> LET x == RandomElement(1..20)
> IN PrintT(<<x, x>>)
> ```
> 
> we will get two different x.
> 
> 
> How to make the two x in PrintT to be the same value?
> 
> Now, I'm using 
> 
> ```
> LET x == RandomElement(1..20)
>        Inside(z) == PrintT(<<z, z>>)
> IN Inside(x)
> ```
> 
> In this situation, the two z is the same.
> 
> Don't know if there is a shorter way to do this?

You are observing the effects of lazy evaluation and that an operator
definition has its operands evaluated eagerly. Also note:

RandomElement
=============
The TLC module defines

RandomElement(S) = CHOOSE x \in S : TRUE

so RandomElement(S) is an arbitrarily chosen element of the set S.
However, contrary to what the definition says, TLC actually makes an
independent choice every time it evaluates RandomElement(S), so it could
evaluate RandomElement(S) = RandomElement(S) to equal false.

When TLC evaluates RandomElement(S), it chooses the element of S
pseudo-randomly with a uniform probability distribution. This feature
was added to enable the computation of statistical properties of a
specification's executions by running TLC in simulation mode. We haven't
had a chance to do this yet; let us know if you try it.

(copied from https://lamport.azurewebsites.net/tla/current-tools.pdf page 6)



Unless you are really interested in the interplay of RandomElement,
PrintT, and lazy evaluation, what is it you are actually trying to
specify? What's the bigger picture here?

Thanks
Markus