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?
as already indicated by Andrew, model checking of finite-state systems relies on a reduction of temporal logic properties to the exploration of finite graphs. There are several good textbooks on model checking that explain in detail how that works.
2) Why does TLC not show which properties or invariants fail?
It does indicate which invariant fails but (unfortunately) not for temporal logic properties. I do not think that doing so would be a fundamental problem, but that it's just a limitation of the implementation, but others will know better.
3) Is it correct to say verifying refinement works the same way as verifying properties?
TLA+ does not formally distinguish between properties and system specifications, since both are expressed as temporal logic properties. Both problems are expressed as the validity of implications Spec => F, and the tools help you verify such problems. Note that TLC only handles a subset of temporal logic formulas, but this subset covers specifications in standard form, so you can use TLC to verify refinement.
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?
If all variables are visible then A will not refine B etc.: an observer would see a step that changes three variables, whereas B only allows two of them to change simultaneously. If the third variable is internal to B (expressed in a TLA formula of the form \EE z : ...) then refinement may hold and can be formally proved by introducing a "stuttering variable" [1]. However, TLC does not handle the \EE quantifier.
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?
It is used for verifying ImpliedTemporal, but ignored for verifying the safety part of the property. For machine closed specifications [2], the supplementary property does not affect the safety properties of a specification, and specifications of the form
Init /\ [][Next]_vars /\ L
where L is a conjunction of fairness properties for sub-actions (essentially, disjuncts) of Next are machine closed.
A simple example of a specification that is not machine closed is the following:
Init == x = 0
Next == x=0 /\ (x'=1 \/ x'=2)
Spec == Init /\ [][Next]_x /\ <>(x=2)
You can convince yourself that Spec => [](x # 1) but TLC will not check this.
Stephan
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.