-------------------------- MODULE Readers_Writers --------------------------
\* https://en.wikipedia.org/wiki/Readers%E2%80%93writers_problem
EXTENDS FiniteSets
CONSTANTS Readers, Writers
VARIABLES Resource
vars == Resource
Init == Resource = [ Readers |-> {}, Writers |-> {} ]
Actors == Readers \union Writers
BusyActors == Resource.Readers \union Resource.Writers
FreeActors == Actors \ BusyActors
Reading(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 /\ WriterShouldBeWriting
Next == \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!