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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 25 Oct 2021 18:47:39 +0200*References*: <61176d59-aab7-462f-ab73-d711b470fba3n@googlegroups.com> <A8D783A1-DE61-4349-874E-D1C16D893228@gmail.com> <CAEJ64taoPJKxucG5QDN5jrUKxhuMXq8JFVh0QowbHc61xeeqEA@mail.gmail.com> <16f4ac23-7f35-004c-920a-a0e997b69fec@lemmster.de> <121ff5a5-5dcc-479a-8f8c-ecbd9d1e1606n@googlegroups.com>

Hello,
TLC explores the state graph in a breadth-first search. When it encounters a state that violates an invariant, it reports the invariant violation and stops. (Temporal) properties are evaluated periodically during the construction of the state graph and again at the end when the entire graph has been computed, so it is not guaranteed that TLC will stop at the earliest possible point, and counter-examples to temporal properties are also not guaranteed to be of minimal length.
We are saying "Every behavior that satisfies Spec has a suffix for which P is true". If P happens to be a state predicate, then this is the same as saying "Every behavior that satisfies Spec will eventually reach a state where P is true".
Yes, if P is a state predicate. In general, it means "Every suffix of any behavior satisfying Spec must satisfy P".
Unlike CTL model checking, LTL / TLA model checking doesn't work by recursively checking the sub-formulas of a formula, and in fact it doesn't make sense to say that a state satisfies a property of the form []P since temporal formulas are evaluated over sequences of states, not states. Markus already provided pointers to the literature, the textbooks by Baier/Katoen [1] and by Clarke, Grumberg et al. [2] are probably the most comprehensive ones.
If the activation status of processes and the leader (i.e., the result of election) are externally observable and your high-level spec says that election happens immediately when the activation status changes then refinements must also do this. Otherwise, an external observer could detect a difference between the behavior of the low-level system (where first the activation status changes and later a process is elected) and the high-level system (where the two happen simultaneously). For example, you might prove an invariant of the high-level spec that asserts that the leader is always active, and that invariant could be violated in the lower-level spec where the current leader gets deactivated before a new leader is elected. Refinement preserves all properties. Hope this helps, Stephan
-- 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/E3422E8F-6EA5-4307-A2C8-0658F349AB5B%40gmail.com. |

**Follow-Ups**:

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

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Stephan Merz

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

**Re: [tlaplus] Verifying fairness | TLC Errors | Refinement | Verifying properties***From:*Markus Kuppe

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

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