[tlaplus] Composing two specs with a shared variable in an non-interleaving way

[jack malkovick <sillymouse333@xxxxxxxxx>]

First lets consider the interleaving setup

AllowZtoChange == z' = z + 4

NextX ==
    \/  /\ x' = x + 1
        /\ z' = z + 2 
    \/  /\ UNCHANGED x
        /\ AllowZtoChange
           
NextY ==
    \/  /\ y' = y + 1
        /\ z' = z + 4 
    \/  /\ UNCHANGED y
        /\ ~AllowZtoChange

Next == NextX /\ NextY

Are the below updates to the specs a correct example of non-interleaving composition? The idea would be to allow simultaneous exclusive x, y updates.

NextX ==
    \/  /\ x' = x + 1
        /\ z' = z + 2 \/ UNCHANGED z
    \/  /\ UNCHANGED x
        /\ AllowZtoChange
           
NextY ==
    \/  /\ y' = y + 1
        /\ z' = z + 4 \/ UNCHANGED z
    \/  /\ UNCHANGED y
        /\ ~AllowZtoChange

They seem to be, but I'm not sure. Is there another solution?

-- 
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/506aade9-4d53-42d4-8d85-4cfcbb926926n%40googlegroups.com.