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

I can only really answer the first question. Behaviors are an infinite sequence of states, yes. However, those behaviors run around a finite state space. All temporal formulas, if false of a system, will have as their counterexample a "lasso" of states where the final state returns to a prior state in the behavior. Think of the simple formula <>P; it suffices as a counterexample to find a behavior that can run in an infinite loop of states where P is never satisfied. So TLC looks for lassos. Not all lassos are counterexamples, though; if you declare weak or strong fairness on actions, that can disallow lassos that would have continuously or continually skipped those actions as part of their infinite loop. Weak fairness disallows stuttering counterexamples for example, where stuttering is just a lasso that loops infinitely in the final state. Lassos with a larger "loop" require strong fairness to disallow. Hopefully that makes sense.

On Tuesday, October 19, 2021 at 1:50:53 PM UTC-4 jone...@xxxxxxxxx wrote:

Hello, esteemed colleagues

Having 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 /\ Temporal
Prop == ImpliedInit /\ [][ImpliedAction]_pvars /\ ImpliedTemporal
TLC checks:
Init /\ [][Next]_vars => ImpliedInit /\ [][ImpliedAction]_vars
Spec => ImpliedTemporal
Why does TLC ignore Temporal?

Best regards,
Jones Martins

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