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

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

On 09.08.2018 21:30, Qd Wang wrote:
> In my situation, I was trying to use a random value twice based one the
> same random value.
> 
> Like this:
> ```
> X == [1 |-> "a", 2 |-> "b", 3 |-> "c"...26 |-> "z"]
> LET n == RandomElement(1..26)
>         Xn == X[n]
> IN
> /\ USE_X_1(Xn)
> /\ USE_X_2(Xn)

Hi,

have you considered CHOOSE to deterministically pick an element from
DOMAIN X? Please also read
https://groups.google.com/d/msg/tlaplus/EIXeHddYI0I/OveKSIi_BwAJ

Thanks
Markus