[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 21 Oct 2021 10:38:09 +0200*References*: <61176d59-aab7-462f-ab73-d711b470fba3n@googlegroups.com>

Hello,
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.
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.
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.
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.
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 [1] Auxiliary Variables in TLA+, http://lamport.azurewebsites.net/pubs/pubs.html#auxiliary [2] The Existence of Refinement Mappings, http://lamport.azurewebsites.net/pubs/pubs.html#abadi-existence
-- 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/A8D783A1-DE61-4349-874E-D1C16D893228%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Travis Allison

**References**:**[tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Jones Martins

- Prev by Date:
**[tlaplus] Re: Verifying fairness | TLC Errors | Refinement | Verifying properties** - Next by Date:
**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties** - Previous by thread:
**[tlaplus] Re: Verifying fairness | TLC Errors | Refinement | Verifying properties** - Next by thread:
**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties** - Index(es):