; modified by Corina Pasareanu
; sedl file generated from rw21.a

;( procedure readWork  (  ) nil )  ( procedure writeWork  (  ) nil )        
;    ( procedure readWork  
;      (  
;       ( procedure writeWork  
;        (  
;              
          
( task Read_Write_Control  
 ( ( entry Start_Read ) 
   ( entry Stop_Read ) 
   ( entry Start_Write ) 
   ( entry Stop_Write ) 
   ( variable ActiveReaders ( range 0  2 )  ) 
   ( variable WriterPresent (boolean)  nil ) 
   ( variable ErrorFlag  (boolean)  nil ) ) 
 ( ( accept Start_Write  ) 
   ( accept Stop_Write  ) 
   ( loop 
     ( select 
       ( when ( not WriterPresent  )  ( accept Start_Read  ) 
              ( assign ActiveReaders  ( + ActiveReaders  1  ) ) ) 
       ( when t  ( accept Stop_Read  ) 
              ( if ( and WriterPresent  ( or ( = ActiveReaders  1  ) 
                                             ( = ActiveReaders  2  ) ) )  
                   ( ( assign ErrorFlag  t ) ) ) 
              ( assign ActiveReaders  ( - ActiveReaders  1  )  ) ) 
       ( when ( and ( = ActiveReaders  0  )  
                    ( not WriterPresent  )  )  ( accept Start_Write  ) 
              ( assign WriterPresent  t  ) ) 
       ( when t  ( accept Stop_Write  ) 
              ( if ( and WriterPresent  ( or ( = ActiveReaders  1  )  
                                             ( = ActiveReaders  2  )  ) )  
                  ( ( assign ErrorFlag  t   ) ) ) 
              ( assign WriterPresent  nil ) ) 
      ) 
    ) 
  ) 
) 

( task Reader_1  
 ( ) 
 ( ( loop 
     ( call Read_Write_Control  Start_Read   ) 
     ( ( readWork  )  ) 
     ( call Read_Write_Control  Stop_Read   ) 
   ) ) 
) 

( task Reader_2  
  ( ) 
  ( ( loop 
      ( call Read_Write_Control  Start_Read   ) 
      ( ( readWork  )  ) 
      ( call Read_Write_Control  Stop_Read   ) 
    ) ) 
) 

( procedure readWork  (  ) nil )  
     
;;      ) 
;;      ( ( null  ) 
;;      ) ) 

( task Writer_1  
  ( ) 
  ( ( loop 
      ( call Read_Write_Control  Start_Write   ) 
      ( (internal "callwriteWork") ( writeWork )  ) 
      ( call Read_Write_Control  Stop_Write   ) 
    ) ) 
) 

( procedure writeWork  (  ) nil )  
     
;;      ) 
;;      ( ( null  ) 
;;      ) )