Re: How to use RandomElement

[Dominik Hansen <do.han...@xxxxxxxxxxxxxx>]

I think the inconsistent behavior of TLC by the evaluating RandomElement operator is caused by TLC's caching techniques.

In the following example the first local definition is evaluated once and the second twice.

ASSUME LET i == IF PrintT("first") THEN RandomElement(1..100) ELSE FALSE IN i = i

ASSUME LET i(j) == IF PrintT("second") THEN RandomElement(1..100) ELSE FALSE IN i(1) = i(1)

As a result the first assumption is always TRUE and the second is almost always FALSE. In the second case the parameter "j" seems to prevent TLC from caching the value of the definition even though the parameter doesn't affect the value.

My explanation for this behavior is that the _expression_ "RandomElement(1..100)" has level 0 (constant-level, cf. 17.2 of Specifying Systems) and underlies TLC's (complex) caching techniques. In my opinion a value of a _expression_ containing the RandomElement operator shouldn't be cached to avoid such an inconsistent behavior.