A predictable choice

[fl]

 

Hi everybody,

 

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 ?

 

--

FL

[Stephan Merz]

Hello Frédéric,

CHOOSE represents deterministic choice. In particular, it satisfies

  (CHOOSE x : P(x)) = (CHOOSE y : P(y))

and more generally

  (\A x : P(x) <=> Q(x)) => (CHOOSE x : P(x)) = (CHOOSE x : Q(x))

TLC has some implementation of this deterministic operator and therefore returns the same value.

It is a frequent mistake in specifications to confuse CHOOSE (deterministic choice) and \E in actions. For example,

HandleRequestDet == CHOOSE req \in Requests : ...    vs.

HandleRequestND == \E req \in Requests : ...

In a state where Requests is non-empty, the first form will produce precisely one successor state during model checking, and the second form Card(Requests) successor states. Typically it is the latter that you want. Also note that the PlusCal statement

    (with x \in S) { ...}

translates to existential quantification.

Best regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Markus Alexander Kuppe]

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

[fl]

> Typically it is the latter that you want. (Stephan)

 

> ... but it is the same one every time. (Markus)
 

OK. Thank you Stephan. Thank you Markus.

 

--

FL