It is completely within the spirit of TLA+ to first write a high-level spec and then check that an algorithm refines that spec. For example, you may have a look at the module SyncTerminationDetected at [1] that provides a high-level spec of termination detection for nodes on a ring with synchronous communication, and for which TLC can check that Dijkstra's algorithm from EWD 840 is a refinement.--StephanOn 28 Oct 2021, at 03:08, Jones Martins <jonesmvc@xxxxxxxxx> wrote:Hello,Thanks again, Stephan and Andrew.I believe all my questions have been answered, especially the one about refinement.“Refinement preserves all properties.” is the key!I am fairly new to model checking, so when thinking about refinement, I compared it to “filling in the details.”In the election example, this would be:1) Election begins.2) ??? (Refinement, allowed through stuttering steps)3) Someone is elected.In a two-player game (tic-tac-toe, maybe), this would be:1) Game starts.2) ??? (Refinement, allowed through stuttering steps)3) There's a draw or a winner.Is there any way of specifying systems in such a high level of abstraction, or would it be 'pointless'?Regards,JonesOn Tue, 26 Oct 2021 at 10:25, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:For understanding weak and strong fairness I encourage you to read my original comment more closely. Fairness can be used in to separate ways:
- As assertions/assumptions
- As properties to check
In the first case, asserting or assuming weak fairness disallows certain counterexamples to temporal properties. For example if I have the temporal property <>P and I haven't assumed any fairness properties of the system, there is a counterexample where the system just stutters in the starting state. Asserting weak fairness over all the actions in my spec will disallow such trivial stuttering counterexamples. Asserting weak fairness of an action says "if this action is continuously enabled, then it must eventually be taken" - so the system can't stutter indefinitely in a state where a weakly-fair action exists that will take it out of that state. Strong fairness is similar, but says "if this action is continually enabled, then it must eventually be taken" although the distinction between continual and continuous is often mysterious to people. Imagine a system that can indefinitely oscillate back and forth between the start state and another state. Asserting weak fairness would not stop this from being a counterexample to <>P; you would have to assert strong fairness on an action taking you out of the start state to disallow this counterexample. Usually you use strong fairness to assert that the "happy path" will be taken in a loop where the system can error out then retry, like delivering a message over a lossy network.In the second case, this is generally used in refinement where a lower-level spec performs multiple steps that would be equivalent to a single step in the higher-level spec. You want to check that the lower-level spec will eventually make state progress as it is defined in the higher-level spec, and fairness is a convenient way to do that.AndrewOn Monday, October 25, 2021 at 12:47:42 PM UTC-4 Stephan Merz wrote:Hello,On 25 Oct 2021, at 03:18, Jones Martins <jone...@xxxxxxxxx> wrote:Hi everyone,Thank you, Andrew, Stephan, Travis, and Markus for your responses!I'd like to clarify some of these questions:1) I asked this question because I'm still confused by how WF and SF works (currently, I differentiate them by thinking a WF action has lower priority than an SF action). This confusion led me to find the formal definition of WF and SF in the Hyperbook.Am I right in saying that verification means “breadth-first searching” a state graph until TLC finds a counterexample is found?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.If so, when we search for properties of the form “<>P”, are we saying “There's at least one state in the state graph where P is true, and this spec reaches that state eventually”?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".Now, for invariants of the form “[]P”, are we saying “P is true for all states of a state graph”?Yes, if P is a state predicate. In general, it means "Every suffix of any behavior satisfying Spec must satisfy P".And if those are true, how does TLC deal with composition of operations, such as <>[]?Would you have any book or article recommendations expanding on that?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.2) My mistake. I meant temporal properties. It seems to me an optimization trade-off, as Markus pointed out.I believe finding refinement errors is also rather difficult, but for separate reasons.It sounds like an interesting challenge. Although I don't think I'm ready for it, I'd like to read his pointers.4) My main concern is what is an abstraction (refinement). In my example above I mention 3 specifications, but my explanation is confusing.Here's an example:I am currently dealing with a very simple Bully election algorithm.The most abstracted version (called SpecA) contains three variables:- IsActive (mapping for each processor),- Leader (what process is leader),- PC (system state).All three variables change in all states.Init == ...Next == \E p \in Procs: (ProcessActivates /\ ElectionWhenActivated) \/ (ProcessDeactivates /\ ElectionWhenDeactivated)Spec == Init /\ [Next]_vars /\ LivenessNow I'm writing SpecB, where elections (should) happen AFTER a process' status changes instead of immediately.Would it be possible to SpecB implement SpecA? Or not, it's impossible because three variables always need to change together even in Spec2, Spec3, and so on...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,StephanThank you very much.Regards,Jones MartinsOn Thursday, 21 October 2021 at 19:09:40 UTC-3 Markus Alexander Kuppe wrote:
On 10/21/21 12:09 PM, Travis Allison wrote:
> You mentioned, "There are several good textbooks on model checking that
> explain in detail how that works." Care to give some titles of textbooks
> you think are good?
Hi Travis,
studying the tableau method shown in "Temporal Verification of Reactive
Systems" [1] in addition to "Verifying arbitrary temporal formulas in
the temporal logic of actions" [2] would enable you to understand TLC's
liveness implementation. More generally, "Principles of Model Checking"
[3] is a good introduction.
By the way, Stephan is absolutely right. The fact that TLC does not
name the violated properties is due to a highly optimized
implementation. I'm happy to give pointers if somebody has the time to
address this shortcoming.
Markus
[1] https://www.springer.com/gp/book/9780387944593
[2] http://wischik.com/lu/research/verify-tla-report.pdf
[3] https://mitpress.mit.edu/books/principles-model-checking--
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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/121ff5a5-5dcc-479a-8f8c-ecbd9d1e1606n%40googlegroups.com.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/eG7SZsKDwIE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a9fc145a-ce80-4e46-9ff3-efe4f7a5c9cfn%40googlegroups.com.
--
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/CABW84KyUdUDSHjCbL0AKuZ83JiG0z4FiMeki-wqpUQ5d6UicsA%40mail.gmail.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/eG7SZsKDwIE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B0ED6E04-E15F-470C-B3DB-6C3053FEBD3D%40gmail.com.