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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Wed, 24 Jul 2019 09:44:22 -0500*References*: <fd9c65b6-68c6-418e-9436-ab4e5cacf99a@googlegroups.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1

Hi Juliet, We can rewrite
q' = [q EXCEPT !["a1"] = Append(@,
x)] ELSE IF x = 2 THEN q' = [q EXCEPT !["a2"] =
Append(@, x)]ELSE UNCHANGED q In practice that will be /\ q' = [q EXCEPT !["a2"] = Append(@,
2)]From Init, that will be equivalent to
q' = [a1 |->
<<>>, a2 |-> <<2>>, a3 |->
<<>>]
So we have two different values for There are a few different ways you can get what you want, but the simplest is to probably make it explicit:
/\ q' = [x \in DOMAIN q |-> IF Map(x) \in {1, 2} THEN Append(q[x], Map(x)) ELSE q[x]] H On 7/24/19 4:02 AM, juliet kim wrote: -- 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/b5d3149e-0c47-e6a2-cc83-3cf5acd237ee%40gmail.com. |

**References**:**[tlaplus] for all, the transition condition is true?***From:*juliet kim

- Prev by Date:
**[tlaplus] for all, the transition condition is true?** - Next by Date:
**[tlaplus] Proving INV1** - Previous by thread:
**[tlaplus] for all, the transition condition is true?** - Next by thread:
**[tlaplus] Proving INV1** - Index(es):