[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Qd Wang <wangq...@xxxxxxxxx>*Date*: Thu, 9 Aug 2018 21:30:13 -0700 (PDT)*References*: <d2137c06-1e1b-47a1-b3d6-9647c02093c2@googlegroups.com> <65224663-7217-420f-c431-27f84deb9dc3@lemmster.de>

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)

```

On Friday, August 10, 2018 at 12:20:06 AM UTC+8, Markus Alexander Kuppe wrote:

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

**Follow-Ups**:**Re: [tlaplus] How to make a concrete value from RandomElement?***From:*Markus Kuppe

**References**:**How to make a concrete value from RandomElement?***From:*Qd Wang

**Re: [tlaplus] How to make a concrete value from RandomElement?***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] How to make a concrete value from RandomElement?** - Next by Date:
**Re: [tlaplus] why `init` will invoke twice** - Previous by thread:
**Re: [tlaplus] How to make a concrete value from RandomElement?** - Next by thread:
**Re: [tlaplus] How to make a concrete value from RandomElement?** - Index(es):