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

Re: [tlaplus] A predictable choice

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,

On 18 Nov 2015, at 16:44, fl <freder...@xxxxxxxxxxx> wrote:

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:
and in the model if I have
and if I launch TLC
then I always get NULL
why ?

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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.