--------------------------- MODULE ReadersWriters --------------------------- 
EXTENDS FiniteSets, Sequences, Naturals
CONSTANTS Client 

Request == {"enter_read", "exit_read", "enter_write", "exit_write"}

State == [rdrs : SUBSET Client, wrtrs : SUBSET Client]

InitialState == [rdrs |-> {}, wrtrs |-> {}]

NewState(c, v, s, q) ==
  CASE v = "enter_read"  -> [s EXCEPT !.rdrs  = @ \cup {c}]
    [] v = "exit_read"   -> [s EXCEPT !.rdrs  = @ \ {c}]
    [] v = "enter_write" -> [s EXCEPT !.wrtrs = @ \cup {c}]
    [] v = "exit_write"  -> [s EXCEPT !.wrtrs = @ \ {c}]

RequestEnabled(c, v, s, q) ==
  CASE v = "enter_read"  -> \/ s.wrtrs = {}
                            \/ c \in s.wrtrs \cup s.rdrs
    [] v = "exit_read"   -> TRUE
    [] v = "enter_write" -> \/ /\ s.wrtrs = {}
                               /\ \A i \in 1..Len(q) : q[i][2] # "enter_read"
                            \/ c \in s.wrtrs \cup s.rdrs
    [] v = "exit_write"  -> TRUE

ResponseVal(c, v, s, q) == 
  CASE v \in {"enter_read", "enter_write" } 
         -> IF c \notin (s.rdrs \cup s.wrtrs) THEN "OK" ELSE "ERROR"  
    [] v = "exit_read" -> IF c \in s.rdrs THEN "OK" ELSE "ERROR"
    [] v = "exit_write"-> IF c \in s.wrtrs THEN "OK" ELSE "ERROR"

BddSeq(S) == UNION{[1..n -> S]: n \in 0..Cardinality(Client)}

VARIABLES sstate, cstate, pendingQ, iFace

INSTANCE MultiClientServer
=============================================================================