1	#define NPROCS 6
2
3	typedef Semaphore {
4	byte count;
5	byte i;
6	byte temp;
7	chan ch = [NPROCS] of {pid};
8	}
9
10	inline initSem(S, n) {S.count = n;
11	S.i = 0;}
12
13	inline wait (S) {
14	atomic {
15	if :: S.count >= 1 -> S.count--;
16	::else ->
17	S.ch ! _pid;
18	!(S.ch ?? [eval(_pid)])
19	fi;
20	}
21	}
22
23	inline signal (S) {
24	atomic {
25	S.i = len(S.ch);
26	if :: S.i == 0 -> S.count++
27	::else ->
28	do :: S.i == 1 -> S.ch ? _; break
29	::else ->
30	S.i--;
31	S.ch ? S.temp;
32	if
33	:: break
34	::S.ch ! S.temp;
35	fi
36	od
37	fi
38	}
39	}
40
41	Semaphore mutex;
42	Semaphore db;
43	int reader_count;
44
45	proctype reader (){
46	do
47	::true->
48	wait(mutex);
49	reader_count++;
50	if :: (reader_count == 1) -> wait(db);
51	fi;
52	signal(mutex);
53	/* read */
54	wait (mutex);
55	reader_count = reader_count - 1;
56	if :: (reader_count == 0) ->
57	signal(db);
58	fi;
59
60	signal(mutex);
61	od;
62	}
63
64	proctype writer () {
65	do
66	::true ->
67	/* create */
68	wait (db);
69	/* write */
70	signal (db);
71	od;
72	}
73
74	init {
75	atomic {
76	initSem (mutex, 3);
77	initSem (db,3);
78	int j;
79	for (j :1..3){
80	run writer ();
81	run reader ();
82	}
83	}
84	}
85
86
87
88
89
90
91
92
93
94
95.0