Re: [tlaplus] A predictable choice

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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:
>  
> CONSTANT GETC(_)
>  
> 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.".

Cheers
Markus