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

[Jones Martins <jonesmvc@xxxxxxxxx>]

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

-- 
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/61176d59-aab7-462f-ab73-d711b470fba3n%40googlegroups.com.