1C IRIW+poonceonces+OnceOnce 2 3{} 4 5P0(int *x) 6{ 7 WRITE_ONCE(*x, 1); 8} 9 10P1(int *x, int *y) 11{ 12 int r0; 13 int r1; 14 15 r0 = READ_ONCE(*x); 16 r1 = READ_ONCE(*y); 17} 18 19P2(int *y) 20{ 21 WRITE_ONCE(*y, 1); 22} 23 24P3(int *x, int *y) 25{ 26 int r0; 27 int r1; 28 29 r0 = READ_ONCE(*y); 30 r1 = READ_ONCE(*x); 31} 32 33exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0) 34