Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties

[Jones Martins <jonesmvc@xxxxxxxxx>]

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 /\ Liveness

Now 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 Martins

On 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/121ff5a5-5dcc-479a-8f8c-ecbd9d1e1606n%40googlegroups.com.