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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Tue, 23 Jan 2024 17:05:57 -0800*References*: <ae6e7be5-6a5d-408e-8782-f75dfb225a82n@googlegroups.com> <33724b18-04cb-4702-a47b-b8b49e701eeen@googlegroups.com>

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.

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

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

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

- Prev by Date:
**[tlaplus] Re: A \/ B** - Next by Date:
**Re: [tlaplus] A \/ B** - Previous by thread:
**[tlaplus] Re: A \/ B** - Next by thread:
**Re: [tlaplus] A \/ B** - Index(es):