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

*From*: myjul...@xxxxxxxxx*Date*: Tue, 24 Jul 2018 03:09:31 -0700 (PDT)*References*: <d8000fb8-777c-4059-a9e9-41d1d27a1f22@googlegroups.com> <BDC267C8-BA70-435D-88E5-828AC8BFE352@gmail.com>

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.

**References**:**About CHOOSE construct***From:*myjul . . .

**Re: [tlaplus] About CHOOSE construct***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Error in spec** - Next by Date:
**Error in spec Reg / Loop structure** - Previous by thread:
**Re: [tlaplus] About CHOOSE construct** - Next by thread:
**Error in spec Reg / Loop structure** - Index(es):