LISA Wo+Ro-rb-Ro+Wo-mb-Ro (* Allowed: rmb not transitive. Also allowed by Power. *) { x = 0; y = 0; } P0 | P1 | P2 ; w[once] x 1 | r[once] r1 x | w[once] y 1 ; | f[rmb] | f[mb] ; | r[once] r2 y | r[once] r3 x ; Observed 2:r3=0; 1:r2=0; 1:r1=1;