Re: [tlaplus] About CHOOSE construct

[myjul...@xxxxxxxxx]

Thank you for your comments.

I looked at section 6.6 of Specifying Systems many times but I didn't understand well. 
You mean that CHOOSE operator is deterministic and both 2 and 3 can't be explored with it.
Actually I want to specify that one of values is always chosen and the selected value is assigned to a variable.
It's exactly like  
    [s EXCEPT !.x = (CHOOSE v \ {2,3} : TRUE) ]
and this statement is used in recursive function to find the changed s.
If I want to make my specification stand the meaning of the above statement(exploring both 2 and 3), how can I make it non-deterministic?

Thanks,
Juliet

2018년 7월 24일 화요일 오후 5시 3분 41초 UTC+9, Stephan Merz 님의 말:
> 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.