On 19 Oct 2021, at 19:50, Jones Martins <jone...@gmail.com> wrote:Hello, esteemed colleaguesHaving read Specifying Systems twice and a large part of the Hyperbook, I still have some doubts concerning how TLC works. I am not perfect, so it's possible I might have missed or misunderstood key concepts.I have a few questions. I'd be able to separate them in different "conversations" if required.1) Since Weak and Strong Fairness are based on the “eventually” and “always” operators, I'd like to know how TLC verifies them. More specifically, since behaviors are an infinite sequence of states, how can the model checker guarantee something eventually or always happens? Wouldn't that be impossible? What am I missing here?
2) Why does TLC not show which properties or invariants fail?
3) Is it correct to say verifying refinement works the same way as verifying properties?
4) Is it possible to refine three (or more) specifications (C implements B, which implements A) such that:A changes three variables atomically.B changes two of those atomically and another one in the next step.C changes each one in a different step.My rationale is that C contains B steps, and B contains A steps.Having read this: https://www.hillelwayne.com/post/refinement/Hillel says this: “We couldn’t write a spec which sets the lock and updates tmp as two separate actions.” Why?
5) From 14.1 of Specifying Systems, when verifying properties:Spec == Init /\ [][Next]_vars /\ TemporalProp == ImpliedInit /\ [][ImpliedAction]_pvars /\ ImpliedTemporalTLC checks:Init /\ [][Next]_vars => ImpliedInit /\ [][ImpliedAction]_varsSpec => ImpliedTemporalWhy does TLC ignore Temporal?
Best regards,Jones Martins--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/61176d59-aab7-462f-ab73-d711b470fba3n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A8D783A1-DE61-4349-874E-D1C16D893228%40gmail.com.
On 25 Oct 2021, at 03:18, Jones Martins <jone...@gmail.com> wrote:Hi everyone,Thank you, Andrew, Stephan, Travis, and Markus for your responses!I'd like to clarify some of these questions:1) I asked this question because I'm still confused by how WF and SF works (currently, I differentiate them by thinking a WF action has lower priority than an SF action). This confusion led me to find the formal definition of WF and SF in the Hyperbook.Am I right in saying that verification means “breadth-first searching” a state graph until TLC finds a counterexample is found?
If so, when we search for properties of the form “<>P”, are we saying “There's at least one state in the state graph where P is true, and this spec reaches that state eventually”?
Now, for invariants of the form “[]P”, are we saying “P is true for all states of a state graph”?
And if those are true, how does TLC deal with composition of operations, such as <>[]?Would you have any book or article recommendations expanding on that?
2) My mistake. I meant temporal properties. It seems to me an optimization trade-off, as Markus pointed out.I believe finding refinement errors is also rather difficult, but for separate reasons.It sounds like an interesting challenge. Although I don't think I'm ready for it, I'd like to read his pointers.4) My main concern is what is an abstraction (refinement). In my example above I mention 3 specifications, but my explanation is confusing.Here's an example:I am currently dealing with a very simple Bully election algorithm.The most abstracted version (called SpecA) contains three variables:- IsActive (mapping for each processor),- Leader (what process is leader),- PC (system state).All three variables change in all states.Init == ...Next == \E p \in Procs: (ProcessActivates /\ ElectionWhenActivated) \/ (ProcessDeactivates /\ ElectionWhenDeactivated)Spec == Init /\ [Next]_vars /\ LivenessNow I'm writing SpecB, where elections (should) happen AFTER a process' status changes instead of immediately.
Would it be possible to SpecB implement SpecA? Or not, it's impossible because three variables always need to change together even in Spec2, Spec3, and so on...
Thank you very much.Regards,Jones MartinsOn Thursday, 21 October 2021 at 19:09:40 UTC-3 Markus Alexander Kuppe wrote:
On 10/21/21 12:09 PM, Travis Allison wrote:
> You mentioned, "There are several good textbooks on model checking that
> explain in detail how that works." Care to give some titles of textbooks
> you think are good?
Hi Travis,
studying the tableau method shown in "Temporal Verification of Reactive
Systems" [1] in addition to "Verifying arbitrary temporal formulas in
the temporal logic of actions" [2] would enable you to understand TLC's
liveness implementation. More generally, "Principles of Model Checking"
[3] is a good introduction.
By the way, Stephan is absolutely right. The fact that TLC does not
name the violated properties is due to a highly optimized
implementation. I'm happy to give pointers if somebody has the time to
address this shortcoming.
Markus
[1] https://www.springer.com/gp/book/9780387944593
[2] http://wischik.com/lu/research/verify-tla-report.pdf
[3] https://mitpress.mit.edu/books/principles-model-checking
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/121ff5a5-5dcc-479a-8f8c-ecbd9d1e1606n%40googlegroups.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/eG7SZsKDwIE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a9fc145a-ce80-4e46-9ff3-efe4f7a5c9cfn%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABW84KyUdUDSHjCbL0AKuZ83JiG0z4FiMeki-wqpUQ5d6UicsA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B0ED6E04-E15F-470C-B3DB-6C3053FEBD3D%40gmail.com.