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

*From*: jacky.hoang93@xxxxxxxxx*Date*: Tue, 10 Sep 2019 10:43:07 -0700 (PDT)*References*: <b62bc163-64e5-46be-9c73-f80db1f553a4@googlegroups.com> <CAJSuO-_0BafixqxmSq0MGwS_YE23JfP1UpODzitysOmEGh3GXw@mail.gmail.com>

Thank-you Saksham!

On Tuesday, September 10, 2019 at 1:30:09 PM UTC-4, Saksham Chand wrote:

-- On Tuesday, September 10, 2019 at 1:30:09 PM UTC-4, Saksham Chand wrote:

On Tue, Sep 10, 2019 at 1:03 PM <jacky....@xxxxxxxxx> wrote:Hello,--Suppose I have a function a, that has domain Z. Suppose x and y are in Z.I'm writing an action where both a[x] and a[y] must be changed.I have one line of the following form:

a' = [a EXCEPT ![x] = ...]and another like so:

a' = [a EXCEPT ![y] = ...]How would I be able to write this altogether as one? Having both doesn't seem to work with Model Checking as count = 0 for those lines.I apologize if I'm using the wrong terms to explain my problem.Thanks for any help

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 tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b62bc163-64e5- .46be-9c73-f80db1f553a4% 40googlegroups.com

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/32a00bef-7d23-4f59-9abc-1de391480578%40googlegroups.com.

**References**:**[tlaplus] Merging EXCEPT statements***From:*jacky . hoang93

**Re: [tlaplus] Merging EXCEPT statements***From:*Saksham Chand

- Prev by Date:
**Re: [tlaplus] Merging EXCEPT statements** - Next by Date:
**[tlaplus] Re: Problem about Ad Hoc mode of ToolBox** - Previous by thread:
**Re: [tlaplus] Merging EXCEPT statements** - Next by thread:
**Re: [tlaplus] Merging EXCEPT statements** - Index(es):