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

*From*: "'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Thu, 11 Feb 2021 10:55:35 +0100*References*: <407236e0-4a88-4ced-b3f2-629a252ddba9n@googlegroups.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.0

Hello, Just a remark if you are designing your Next state relation: this is often written as a disjunction of actions (which makes non-determinism possible). What you might want to write could be along the lines of: \/ (x /\ y /\ z' = 42) \/ (x /\ ~y /\ z' = 11) \/ (~x /\ z' = 23) This amounts to stating "if x and y hold, then the next value of z is 42, if x but not y holds, then the next value of z is 11; if x does not hold then the next value of z is 23". In this example all cases are mutually exclusive but that's not necessary (e.g. just remove the /\ y from the first line). hope this helps! kind regards, Martin On 2/10/21 9:31 PM, Anshu ranjan wrote: > Hi, I have a beginner's question: > If I want to write the following clause: > > IF x=true and y=true > THEN do z > > How can write this in TLA+? Specifically how do I write the and operator? > > -- > 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+unsubscribe@xxxxxxxxxxxxxxxx > <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/tlaplus/407236e0-4a88-4ced-b3f2-629a252ddba9n%40googlegroups.com > <https://groups.google.com/d/msgid/tlaplus/407236e0-4a88-4ced-b3f2-629a252ddba9n%40googlegroups.com?utm_medium=email&utm_source=footer>. -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f45c168d-721a-b4ed-8297-db0a1cfcee57%40gmail.com.

**Follow-Ups**:**Re: [tlaplus] AND operator***From:*Anshu ranjan

**References**:**[tlaplus] AND operator***From:*Anshu ranjan

- Prev by Date:
**[tlaplus] How to append to a chain?** - Next by Date:
**Re: [tlaplus] Latex** - Previous by thread:
**Re: [tlaplus] AND operator** - Next by thread:
**Re: [tlaplus] AND operator** - Index(es):