| Hello, before attempting to verify liveness properties, always verify some safety properties. In your case, the canonical property to verify is that there can always be at most one writer and that there can never be active readers and writers at the same time. In order to make sure that your specification is not vacuous, it is also recommended to verify as many non-properties as you can think of and make sure that the counter-examples that TLC returns conform to your intuition. For example, claim that no reader can ever be active or that no writer can ever be active. In order to answer your questions: (1) I presume your formula "Liveness" defines the property that you expect your specification to ensure. But then you shouldn't make it part of the definition of Spec, otherwise you just verify a triviality. And you haven't made it clear how you intend to implement the liveness property in your system. Typically, one assumes being able to ensure (weak or strong) fairness conditions on actions, based on appropriate schedulers. So you could define \* assume that for every actor, if some action is forever enabled, it must eventually be taken FairRead == \A a \in Readers : WF_vars(Reading(a)) FairWrite == \A a \in Writers : WF_vars(Writing(a)) FairStop == \A a \in Actors : WF_vars(StopActivity(a)) Fairness == FairRead /\ FairWrite /\ FairStop and add Fairness to your Spec, instead of Liveness. When you now attempt to verify the liveness property for readers (formula ReaderShouldBeReading), TLC will produce a counter-example where some writer repeatedly accesses the resource but no reader ever reads. Take the time that is needed to understand why this execution satisfies the above fairness conditions. We can ensure the liveness condition for readers by changing WF to SF in the definition of FairRead, and TLC will confirm this. Again make sure you understand why this is the case. Turning to checking liveness for writers (formula WriterShouldBeWriting), TLC will produce a more elaborate counter-example that shows you why this property does not hold, even if you replace WF by SF in the definition of FairWrite. Take the time necessary to understand why this counter-example is fair. Now you'll have to come up with a mechanism that ensures liveness for writers, and this will require more than adding fairness conditions. The attached module contains the above definitions. (2) The statistics that TLC outputs at the end of a run reflect properties of the state graph such as the numbers of states and distinct states. The graph is the same whether you check safety or liveness properties, so these numbers are the same as well. (3) In the breadth-first exploration that TLC performs, the action StopActivity always loops back to a state that TLC has encountered before, that's why it doesn't produce new "distinct states". 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/2C3CE438-E2BE-48AE-9204-F509B90BC0DA%40gmail.com. |
Attachment:
ReadersWriters.tla
Description: Binary data
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/2C3CE438-E2BE-48AE-9204-F509B90BC0DA%40gmail.com. |