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

*From*: marc magrans de abril <marcmagra...@xxxxxxxxx>*Date*: Fri, 14 Jun 2013 14:37:13 -0700 (PDT)*References*: <ad7864c5-38a0-495a-9fa5-bc4d92d86fac@googlegroups.com> <49911de5-80b6-49a3-b932-4fc8e158e0dd@googlegroups.com>

Hi Dominik,

Still, I do not fully understand the behavior. I'll try to explain my doubts...

i==RandomElement(MYSET)

Pair == /\ x' = i

/\ y' = i

2) In the hyperbook there is also the example definition of RandomRanking(S). This leads to the invariant "(Len(x) = Cardinality(MYSET)) /\ (\E j \in 1..Len(x): x[j] \in MYSET)". This suggests that RandomElement is just evaluated once per recursion level.

RECURSIVE RandomRanking(_)

RandomRanking(S) == IF S = {} THEN

<< >>

ELSE

LET e == RandomElement(S)

IN

<<e>> \o RandomRanking(S \ {e})

Ranking == x' = RandomRanking(MYSET)

3) Finally, in the initial example I sent the invariant "x=y" fails. In this case RandomElement is evaluated twice.

Next == LET i == RandomElement(1..100)

IN

/\ x' = i

/\ y' = i

Thanks for your help,

IN

/\ x' = i

/\ y' = i

Thanks for your help,

marc

On Friday, June 14, 2013 1:02:07 PM UTC+2, Dominik Hansen wrote:

Hi Marc,if you want to use the same random element at different places and you want to avoid an action like "Next == x' = RandomElement(1..100) /\ y' = x' " you can bind the random element to a variable of a quantification:

--------------------------- MODULE RandomElement ---------------------------

EXTENDS Integers,TLC

VARIABLES x,y

Init == /\ x=0

/\ y=0

Next == /\ \E i \in { RandomElement(1..100) }: PrintT(i) /\ x' = i /\ y' = i

Inv == x=y

==============================

============================== =================

But the behavior of TLC by evaluation the RandomElement operator isn't always obvious. The description of the operator in current-tools.pdf says that "RandomElement(S) = RandomElement(S)" could be evaluated to FLASE. However, if I substitute the calls of the RandomElement operator by an additional definition it will be always evaluated to TRUE:

i == RandomElement(1..100)

ASSUME i = i

This behavior is probably caused by the fact that TLC treats the definition "i" as a constant _expression_ and evaluates the definition only once.

TLC's behavior also leads to tiny detail in my specification above: I added the conjunction operator "/\" at the beginning of the Next definition otherwise TLC would evaluate the _expression_ "{RandomElement(1..100)}" only once. In this case the reason is more subtle. In presence of the conjunction operator TLC treats the Next definition as a single action because TLC can't split a conjunction into separate actions. If there is no conjunction TLC tries to split the body of the existential quantification into separate actions and handles the bounded variables in a different way (evaluating the _expression_ only once).

I'm not sure if it is a desired behavior or a bug.

Dominik

**Follow-Ups**:**Re: How to use RandomElement***From:*Dominik Hansen

**References**:**How to use RandomElement***From:*marc magrans de abril

**Re: How to use RandomElement***From:*Dominik Hansen

- Prev by Date:
**Re: How to use RandomElement** - Next by Date:
**Re: How to use RandomElement** - Previous by thread:
**Re: How to use RandomElement** - Next by thread:
**Re: How to use RandomElement** - Index(es):