On Tuesday, February 23, 2021 at 10:58:53 AM UTC+1 Younes wrote:
Hello,1 - I've written the specs below for the Reader-Writer Problem, and I'm wondering if the Liveness conditions I have set are right. I considered that the liveness conditions are :
- Every reader in the community of Readers will eventually be reading
- Every writer in the community of Writer will eventually be writing
-------------------------- MODULE Readers_Writers --------------------------EXTENDS FiniteSetsCONSTANTS Readers, WritersVARIABLES Resourcevars == ResourceInit == Resource = [ Readers |-> {}, Writers |-> {} ]Actors == Readers \union WritersBusyActors == Resource.Readers \union Resource.WritersFreeActors == Actors \ BusyActorsReading(actor) == /\ actor \in Readers/\ actor \notin BusyActors/\ Cardinality(Resource.Writers) = 0/\ Resource' = [Resource EXCEPT !.Readers = @ \union {actor} ]Writing(actor) == /\ actor \in Writers/\ actor \notin BusyActors/\ Cardinality(BusyActors) = 0/\ Resource' = [Resource EXCEPT !.Writers = @ \union {actor }]StopActivity(actor) == /\ actor \in BusyActors/\ \/ actor \in Resource.Readers /\ Resource' = [Resource EXCEPT !.Readers = @ \ {actor} ]\/ actor \in Resource.Writers /\ Resource' = [Resource EXCEPT !.Writers = @ \ {actor} ]ReaderShouldBeReading == \A reader \in Readers : [] <> (reader \in Resource.Readers)WriterShouldBeWriting == \A writer \in Writers : [] <> (writer \in Resource.Writers)Liveness == ReaderShouldBeReading /\ WriterShouldBeWritingNext == \E actor \in Actors : Reading(actor) \/ Writing(actor) \/ StopActivity(actor)Spec == Init /\ [][Next]_vars /\ Liveness=============================================================================2 - I have also realized that whether I include the Liveness conditions or not in my Spec, the results, after the model checking, are the same. Why?3 - Why does the action StopActivity has 0 distinct state? Does that mean TLC doesn't explore it at all? Why is that?I will also gladly take any comments about the specs for improvement.Thank you!