[tlaplus] A \/ B

Hello Everyone.

I`m new to TLA+, sorry for trivial questions ...

studying session 7 in PlusCal Tutorial https://lamport.azurewebsites.net/tla/tutorial/session7.html i got TLA+ code.

In short words:

init: x = 0

A == /\ pc[3] = "a"

/\ x' = x + 1
/\ pc' = [pc EXCEPT ![3] = "Done"]

B == /\ pc[-7] = "b"
/\ x' = x + 1
/\ pc' = [pc EXCEPT ![-7] = "Done"]

Next = A \/ B \/ Terminating

processes executed once, and the resulting value of x is 2

From my point of view, it could be 1 if both processes worked and finished in parallel, but it doesn`t happen.

Can you please tell me what is the checker logic for this code?

it executes both A and B, but the last executed overwrites pc, so first is obliged to be executed second time?

or after executing first, it even doesn`t try to run second, because this condition doesn't stay: pc' = [pc EXCEPT ![-7] = "Done"] ?

Sincerely yours, Andrew

--
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/ae6e7be5-6a5d-408e-8782-f75dfb225a82n%40googlegroups.com.