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