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