31 views

Skip to first unread message

Sep 10, 2019, 1:03:20 PM9/10/19

to tlaplus

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

Sep 10, 2019, 1:30:09 PM9/10/19

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

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

Sep 10, 2019, 1:33:07 PM9/10/19

to tla...@googlegroups.com

Hi,

Saksham already pointed out how to update a function at several argument positions. Writing

/\ a' = [a EXCEPT ![x] = foo]

/\ a' = [a EXCEPT ![y] = bar]

implies that

[a EXCEPT ![x] = foo] = [a EXCEPT ![y] = bar]

which is unlikely to be true, which explains why you see line count 0 in TLC.

Stephan

Sep 10, 2019, 2:23:59 PM9/10/19

to tlaplus

Thank-you Saksham!

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....@gmail.com> 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.

Sep 10, 2019, 2:23:59 PM9/10/19

to tlaplus

Thanks for your explanation Stephan!

On Tuesday, September 10, 2019 at 1:33:07 PM UTC-4, Stephan Merz wrote:

Hi,Saksham already pointed out how to update a function at several argument positions. Writing/\ a' = [a EXCEPT ![x] = foo]/\ a' = [a EXCEPT ![y] = bar]implies that[a EXCEPT ![x] = foo] = [a EXCEPT ![y] = bar]which is unlikely to be true, which explains why you see line count 0 in TLC.

Stephan

On 10 Sep 2019, at 09:51, jacky....@gmail.com 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.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu