(ovviamente quella seguente non e' l'unica soluzione,
 e tantomeno la migliore)

Il contatore "pending" (realizzato tramite il valore che passa
attraverso un canale omonimo di tipo ^Int) 
fornisce informazioni su
* numero di processi read che stanno ancora in fase di lettura.
  Tale numero, se "pending" > 0,  e' pari a (100 - "pending")
 (dove si suppone che 100 sia un qualsiasi numero maggiore del numero
  massimo di processi read)
* presenza di un processo write in attesa che i processi read attualmente
  in fase di lettura terminino in modo da poter scrivere.
  Tale situazione e' rappresentata dal fatto che "pending" < 0.
  In questo caso "pending" rappresenta il numero di processi read
  che debbono terminare la lettura. Quando "pending" < 0 a nessun
  processo read viene concesso il permesso di leggere, poiche' c'e'
  un processo write in attesa
* presenza di un processo write in attesa di scrittura, ed assenza di
  processi read in lettura. 
 Tale situazione e' rappresentata dal fatto che "pending" = 0.

Il contatore "acks" (realizzato tramite il valore che passa 
attraverso un canale omonimo di tipo ^Int)
rappresenta il numero di processi che hanno segnalato la terminazione
delle loro operazioni (lettura o scrittura).



val [
 #Request                 {- enumeration type representing w/r requests -}
 r-req: Request
 w-req: Request
 samereq: /[Request Request /Bool]
] = [
 #Int                    {- internal representation of type Request -}
 0
 1
 ==
]

new acks   : ^Int

run acks!0              {- representing inizialization "acks" -}


{- no need the following channels to be private  -}

new req: ^Request    {- channel for w/r requests communications -}

new r-grant: ^[]       {- channel to communicate read request qrant -}

new w-grant: ^[]       {- channel to communicate write request qrant -}


def controller [resource: ^T] =  {- we assume a controller to be parametrized with
                                    a channel of a certain, unspecified type to
                                    access the resource -}
 (new pending: ^Int
  run pending!100      {- representing inizialization of "pending" -}
{- a controller is made of an infinite loop -}
  def loop [] =
   pending?n = if (> n 0) then
                 ( acks?k = req?rqst =  if (samereq rqst r-req) then
                                         ( pending!(- (+ n k) 1) 
                                         | r-grant![]
                                         | acks!0
                                         )
                                        else
                                         ( pending!(- (+ n k) 100) 
                                         | acks!0
                                         )
                  | loop![]
                 )
               else
                 if (== n 0) then
                   ( w-grant![]
                   | acks?_ = pending!100
                   | loop![]
                   )
                 else
                   ( acks?k = pending!(+ n k) 
                   | loop![]
                   )
  loop![]
 )





def read-proc [resource: ^T] =
  ( req!r-req
  | r-grant?[] = (new done:^[]
                  ( READING
                  | done?[] = acks?k = acks!(+ k 1)
  )              ))


def write-proc [resource: ^T]
  ( req!w-req
  | w-grant?[] = (new done:^[]
                  ( WRITING
                  | done?[] = acks?_ = acks!1  {- only one writer, acks was 0 -}
  )              ))
               
new resource: /T

( RESOURCE-proc!resource
| controller!resource 
| read-proc!resource | read-proc!resource | ... 
| write-proc!resource | write-proc!resource |...
)