[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:
"Start"
"Finish"
"Start"
"Finish"
"Start"
"Finish"
"Finish"
"Start"
"Finish"

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.