Re: [tlaplus] About CHOOSE construct

[Stephan Merz <stepha...@xxxxxxxxx>]

The CHOOSE operator is deterministic: you want equality to be reflexive, so

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

has to be true. Use disjunction or existential quantification to express non-determinism in your specification. For example, an action such as

\E v \in {2,3} : x' = v /\ y' = y + 2*v

will explore both branches for v=2 and v=3.

For more information, look at section 6.6 of Specifying Systems.

Regards,
Stephan


> On 24 Jul 2018, at 09:56, myjul...@xxxxxxxxx wrote:
> 
> Sir,
> 
> I'm writing TLA+ specification and I use TLC.
> While I'm using TLC, I'm curious about CHOOSE construct.
> 
> If the statement is as follows,
>  ....
>  CHOOSE v \in {2, 3} : TRUE
>  ....
> 
> the selected value is almost always 2 while model checked it.
> But, the next state depends on which the value is chosen so I want to check all the cases.
> Is it possible to solve with model checking?
> 
> Thanks,
> Juliet
> 
> -- 
> 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 https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.