среда, 24 января 2024 г. в 02:06:07 UTC+1, 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.
> On Jan 23, 2024, at 3:53 PM, Andrew Samokish <asam...@xxxxxxxxx> wrote:
>
> 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