A \/ B

[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

[Andrew Samokish]

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:

[Markus Kuppe]

Careful: TLC is a model checker, not a runtime. Therefore, you should not rely on PrintT for debugging your specification. Instead, consider using the TLA+ debugger (https://www.youtube.com/playlist?list=PLWLcqZLzY8u9crK5PwTmEyBjgzHCotT60).

Regarding your original question: For 'x=1' to be a final state of your specification, 'A /\ B' must eventually be true. TLC can help you if this condition can be met.

M.

PS: Pay attention to the EXCEPTs.

[Andrew Samokish]

Thank you very much, Markus. Going to see how to install TLA+ debugger.

Amdrew

среда, 24 января 2024 г. в 02:06:07 UTC+1, Markus Kuppe: