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

*From*: Andrew Samokish <asam.mail@xxxxxxxxx>*Date*: Wed, 24 Jan 2024 05:16:10 -0800 (PST)*References*: <ae6e7be5-6a5d-408e-8782-f75dfb225a82n@googlegroups.com> <33724b18-04cb-4702-a47b-b8b49e701eeen@googlegroups.com> <4CB24A91-CAA2-47C4-BD8B-06CE4ADC4AF2@lemmster.de>

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

Amdrew

среда, 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

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/ce94f1a2-ab40-4d4f-bb0e-50b53b20bddbn%40googlegroups.com.

**References**:**[tlaplus] A \/ B***From:*Andrew Samokish

**[tlaplus] Re: A \/ B***From:*Andrew Samokish

**Re: [tlaplus] A \/ B***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] A \/ B** - Next by Date:
**Re: [tlaplus] Re: Draft of New TLA Book** - Previous by thread:
**Re: [tlaplus] A \/ B** - Next by thread:
**[tlaplus] Action A can only be followed by Action B** - Index(es):