среда, 24 января 2024 г. в 00:32:45 UTC+1, Andrew Samokish:
Hello Everyone.I`m new to TLA+, sorry for trivial questions ...
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