CHOOSE is arbitrary according to the reference, but should be deterministic?

[shuhaowu]

In the appendix, the reference section claims:

(CHOOSE x \in {1, 2, 3} : x <= 2) = \* 1 or 2, arbitrary

However, looking at this thread, I'm lead to believe that CHOOSE will always return the same value, which I believe should be 1 if evaluated by TLC.

Maybe the point from the hyperbook should be emphasized:

In mathematics, there is no such thing as a nondeterministic operator or a nondeterministic function. If some expression equals 42 today, then it equaled 42 yesterday and it will still equal 42 next year. [...] The semantics of TLA + do not specify which value in 1.. 10; but it is the same one every time.

[shuhaowu]

I see that this is emphasized in the main text, but in the appendix this is not made clear on that spot. Perhaps a link to the main text should be provided here.

[hwayne]

Good idea, I'll update it tonight to make it more explicit.

[hwayne]

Updated.