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

Re: [tlaplus] A predictable choice

On 18.11.2015 16:44, fl wrote:
> I suppose it is a question that has already been answered and I
> apologize but if
> somebody could enlighten me anyway.
> If I have a:
> and in the model if I have
> GETC(x) <- CHOOSE y \in { A, NEWLINE, NULL } : TRUE
> and if I launch TLC
> then I always get NULL
> why ?

Hi Frederic,

you might want to read section 13.5 "The choose Operator" of the hyperbook:

"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.".