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

[tlaplus] Re: A \/ B

another question with the same example:
i did change the 'next': Next == PrintT("Start") /\ (A \/ B \/ Terminating) /\ PrintT("Finish")
resulting output is:

how is it possible, that I have 5 'finish' and only 4 'start' ?
среда, 24 января 2024 г. в 00:32:45 UTC+1, Andrew Samokish:
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/33724b18-04cb-4702-a47b-b8b49e701eeen%40googlegroups.com.