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

*From*: Anshu ranjan <a.ranjan.cool@xxxxxxxxx>*Date*: Fri, 12 Feb 2021 10:07:38 -0800 (PST)*References*: <407236e0-4a88-4ced-b3f2-629a252ddba9n@googlegroups.com> <f45c168d-721a-b4ed-8297-db0a1cfcee57@gmail.com>

Thank you all for the help. I ended up using IF .. THEN .. ELSE TRUE, which seemed easiest.

On Thursday, February 11, 2021 at 4:55:39 AM UTC-5 martin...@xxxxxxxxxxxxxx wrote:

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+u...@xxxxxxxxxxxxxxxx

> <mailto:tlaplus+u...@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/de0b74ce-a274-4a94-86dd-55da7c7c2d40n%40googlegroups.com.

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

**Re: [tlaplus] AND operator***From:*'Martin' via tlaplus

- Prev by Date:
**[tlaplus] Set within a set** - Next by Date:
**Re: [tlaplus] Set within a set** - Previous by thread:
**Re: [tlaplus] AND operator** - Next by thread:
**Re: [tlaplus] Latex** - Index(es):