Readers–writers problem

Readers_Writers.tla

-------------------------- MODULE Readers_Writers --------------------------
\*https://en.wikipedia.org/wiki/Readers%E2%80%93writers_problem
EXTENDS Sequences, Naturals, FiniteSets
CONSTANTS Readers, Writers

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

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

Init == 
    /\ Resource = [ Readers |-> {}, Writers |-> {} ]
    /\ Waiting =  <<>>
    /\ semR = Cardinality(Readers) - 1
    /\ semW = FALSE

TypeOK ==
    /\ Resource \in [ Readers : SUBSET Readers, Writers : SUBSET Writers ]
    /\ \A w \in Range(Waiting) : w \in Nat
    /\ semR \in 0..Cardinality(Readers)
    /\ semW \in BOOLEAN

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

\* Actions 
Reading(actor) == 
    /\ Waiting # <<>>
    /\ actor \in Readers
    /\ actor = Head(Waiting)
    /\ semR < Cardinality(Readers)
    /\ semR > 0
    /\ semW = FALSE
    /\ Resource' = [Resource EXCEPT !.Readers = @ \union {actor} ]
    /\ Waiting' = Tail(Waiting)
    /\ semR' = semR - 1
    /\ UNCHANGED semW

Writing(actor) ==
    /\ Waiting # <<>>
    /\ actor \in Writers
    /\ actor = Head(Waiting)
    /\ semR = Cardinality(Readers) - 1
    /\ semW = FALSE
    /\ Resource' = [Resource EXCEPT !.Writers = @ \union {actor} ]
    /\ Waiting' = Tail(Waiting)
    /\ semW' = TRUE
    /\ UNCHANGED semR

Request(actor) ==
    /\ actor \notin BusyActors
    /\ actor \notin Range(Waiting)
    /\ Len(Waiting) < 4
    /\ Waiting' = Append(Waiting, actor)
    /\ UNCHANGED <<semR, Resource, semW>>

Stop(actor) ==
    /\ actor \in BusyActors
    /\ \/ actor \in Resource.Readers /\ Resource' = [Resource EXCEPT !.Readers = @ \ {actor} ] /\ semR' = semR + 1 /\ UNCHANGED semW
       \/ actor \in Resource.Writers /\ Resource' = [Resource EXCEPT !.Writers = @ \ {actor} ] /\ semW' = FALSE /\ UNCHANGED semR
    /\ UNCHANGED Waiting              

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

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

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

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

\* Safety properties:
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

THEOREM Invariants => []Spec

\* Liveness Properties
\* Every reader should eventually be reading
ReaderShouldBeReading   == \A reader \in Readers : ENABLED Reading(reader) => <> (reader \in Resource.Readers)
\* Every writer should eventually be writing
WriterShouldBeWriting   == \A writer \in Writers : ENABLED Writing(writer) => <> (writer \in Resource.Writers)
\* Every reader who is reading should eventually stop reading
ReadersShouldStop       == \A reader \in Readers : reader \in Resource.Readers ~> <> ( reader \notin Resource.Readers )
\* Every writer who is writing should eventually stop writing
WritersShouldStop       == \A writer \in Writers : writer \in Resource.Writers ~> <> ( writer \notin Resource.Writers )

=============================================================================