ReadWrite.csp

-----------------------------------------------------------------------------------------
-----------------------------------------------------------------------------------------
-- ReadWrite.csp
--
-- AUTHORS:   Ling Shi, Yang Liu, Jun Sun, Jin Song Dong and Gustavo Carvalho 	
-- DATE:      2012            
-- PUBLISHED: An Analytical and Experimental Comparison of CSP Extensions and Tools. 
--            The 14th International Conference on Formal Engineering Methods (ICFEM 2012).
--            Experiments on www.comp.nus.edu.sg/˜pat/compare               
-- DESCRIPTION
-- This problem deals with situations in which many threads must access the same shared 
-- memory at one time, some reading and some writing, with the natural constraint that 
-- no process may access the share for reading or writing while another process is in the 
-- act of writing to it. In particular, it is allowed for two readers to access the share 
-- at the same time. In this model, a controller is used to guarantee the correct coordination 
-- among multiple readers/writers.
-----------------------------------------------------------------------------------------
-----------------------------------------------------------------------------------------

-----------------------------------------------------------------------------------------
-- SOURCE CODE (adapted version)
-----------------------------------------------------------------------------------------
channel startwrite, stopwrite, startread, stopread, error

Writer 	= startwrite -> stopwrite -> Writer

Writers(0) = Writer
Writers(1) = Writer
Writers(2) = Writer

Reader 	= startread -> stopread -> Reader

Readers(0) = Reader
Readers(1) = Reader
Readers(2) = Reader

Reading(0) = Controller
Reading(1) = startread -> Reading(2) [] stopread -> Reading(0)
Reading(2) 	= stopread -> Reading(1) 

Controller 	= startread -> Reading(1)
	 	 	 	 [] stopread -> error -> Controller
	 	 	 	 [] startwrite -> (stopwrite -> Controller [] stopread -> error -> Controller)

ReadersWriters = Controller 
	            [|{|startwrite, stopwrite, startread, stopread|}|] 
		        ((Readers(0) ||| Writers(0)) 
		         ||| 
		        (Readers(1) ||| Writers(1)) 
		         ||| 
		        (Readers(2) ||| Writers(2)))

MAIN = ReadersWriters