/** Readers - Writers
 *  example for SEG-2106 course by Gregor v. Bochmann
 */

const Number = 3
range Int = 0..Number

READER(I=0) = 
(think_R[I] -> reserve_R[I] -> read[I] -> release_R[I] -> READER).
  
WRITER(I=0) = 
(think_W[I] -> reserve_W[I] -> write[I] -> release_W[I] -> WRITER).
  

RESOURCE(N=0) = R_FREE[N],
// state R_W means that a writer is active
// state R_R means that at least one reader is active
// the parameter r represents the number of active readers. It is always zero for the states R_FREE and R_W
R_FREE[r:Int] = ( reserve_W[0] -> R_W[0] | reserve_W[1] -> R_W[0] | reserve_W[2] -> R_W[0]  // a writer reserves
                | reserve_R[0] -> R_R[r+1] | reserve_R[1] -> R_R[r+1] | reserve_R[2] -> R_R[r+1] ),  // a reader reserves
R_W[r:Int] =  ( release_W[0] -> R_FREE[0] | release_W[1] -> R_FREE[0] | release_W[2] -> R_FREE[0] ), // the writer releases
R_R[r:Int] =  ( when(r>1) release_R[0] -> R_R[r-1] | when(r>1) release_R[1] -> R_R[r-1] | when(r>1) release_R[2] -> R_R[r-1]  // a reader releases
              | when(r<2) release_R[0] -> R_FREE[0] | when(r<2) release_R[1] -> R_FREE[0] | when(r<2) release_R[2] -> R_FREE[0]  // last reader releases
              | reserve_R[0] -> R_R[r+1] | reserve_R[1] -> R_R[r+1] | reserve_R[2] -> R_R[r+1] ).  // another reader reserves

        
||R_W_SYSTEM(N=Number)= 
   forall [i:0..N-1] 
       (READER(i) || WRITER(i) || RESOURCE).