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

*From*: Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>*Date*: Thu, 9 Aug 2018 09:19:59 -0700*References*: <d2137c06-1e1b-47a1-b3d6-9647c02093c2@googlegroups.com>

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**:

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

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