-------------------------- MODULE Readers_Writers --------------------------
EXTENDS Sequences, Naturals, FiniteSets
CONSTANTS Readers, Writers

VARIABLES Resource, Waiting
vars == <<Resource, Waiting>>

Init == /\ Resource = [ Readers |-> {}, Writers |-> {} ]
        /\ Waiting = <<>>

TypeOK == /\ {Resource.Readers} \subseteq SUBSET Readers
          /\ {Resource.Writers} \subseteq SUBSET Writers

Actors == Readers \union Writers
BusyActors == Resource.Readers \union Resource.Writers

Range(S) == { S[i] : i \in DOMAIN S}

\* Actions 
Request(actor) == /\ Len(Waiting) < Cardinality(Actors)
                  /\ actor \notin BusyActors \union Range(Waiting)
                  /\ Waiting' = Append(Waiting, actor)
                  /\ UNCHANGED <<Resource>>

AddToSet(el, Set) == /\ Resource' = [ Resource EXCEPT ![Set] = @ \union {el} ]
                     /\ Waiting' = Tail(Waiting)

Reading == /\ Waiting # <<>>
           /\ Head(Waiting) \in Readers
           /\ Resource.Writers = {}
           /\ AddToSet(Head(Waiting), "Readers")

Writing == /\ Waiting # <<>>
           /\ Head(Waiting) \in Writers
           /\ BusyActors = {}
           /\ AddToSet(Head(Waiting), "Writers")

Stop == LET actor == CHOOSE el \in BusyActors : TRUE
        IN /\ BusyActors # {}
           /\ \/ actor \in Resource.Readers /\ Resource' = [Resource EXCEPT !.Readers = @ \ {actor} ]
              \/ actor \in Resource.Writers /\ Resource' = [Resource EXCEPT !.Writers = @ \ {actor} ]
           /\ UNCHANGED Waiting

Next == \E actor \in Actors : Request(actor) \/ Reading \/ Writing \/ Stop

FairRequest == \A actor \in Actors: SF_vars(Request(actor))
FairReading == \A reader \in Readers: SF_vars(Reading)
FairWriting == \A writer \in Readers: SF_vars(Writing)
FairStop == \A actor \in Actors: SF_vars(Stop)

Fairness == FairReading /\ FairWriting /\ FairStop /\ FairRequest

Spec == Init /\ [][Next]_vars /\ Fairness

\* Safety properties : something bad never happens
Invariants ==
           /\ TypeOK
           \* There can never be an active writer and an active reader at the same time  
           /\ ~( Resource.Writers # {} /\ Resource.Readers # {} ) 
           \* There should be at most one writer
           /\ \A a,b \in Actors : a \in Resource.Writers /\ b \in Resource.Writers => a = b

ReaderShouldBeReading == \A reader \in Readers : [] <> (reader \in Resource.Readers)
WriterShouldBeWriting == \A writer \in Writers : [] <> (writer \in Resource.Writers)
ReadersShouldStop == \A reader \in Readers : reader \in Resource.Readers ~> <> ( reader \notin Resource.Readers )
WritersShouldStop == \A writer \in Writers : writer \in Resource.Writers ~> <> ( writer \notin Resource.Writers )
=============================================================================