1C CoRW+poonceonce+Once
2
3{}
4
5P0(int *x)
6{
7	int r0;
8
9	r0 = READ_ONCE(*x);
10	WRITE_ONCE(*x, 1);
11}
12
13P1(int *x)
14{
15	WRITE_ONCE(*x, 2);
16}
17
18exists (x=2 /\ 0:r0=2)
19