The readers/writers problem describes a protocol for coordination of N readers and N writers accessing a shared resource.
The CSP definition of Readers-Writers Problem of size N is defined as follows.
The property to verify is reachability of an erroneous situation (i.e., wrong readers/writers coordination).
[]<>error
The following defintion is the MS example with size 2.
====================Process Definitions====================
Reading0()=Controller;
Reading1()=((startread->Reading2)[](stopread->Reading0));
Reading2()=(stopread->Reading1);
Writing()=((stopwrite->Controller)[](stopread->(error->Writing)));
Writer0()=(startwrite->(stopwrite->Writer0));
Writer1()=(startwrite->(stopwrite->Writer1));
Reader1()=(startread->(stopread->Reader1));
Reader0()=(startread->(stopread->Reader0));
Controller()=((startread->Reading1)[]((stopread->(error->Controller))[](startwrite->Writing)));
aReadersWriters()=(Controller||(Reader0|||Reader1)||(Writer0|||Writer1));
============================LTL Definitions============================
LTL(AlwaysError=[]<>error);