Re: [tlaplus] A \/ B

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.mail@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

-- 
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/4CB24A91-CAA2-47C4-BD8B-06CE4ADC4AF2%40lemmster.de.