LISA Alan08 (* mrcu Translation of Alan07... Forbidden ! *) {} P0 | P1 | P2 ; w[once] x 1 | r[once] r1 y | r[once] r2 z ; w[release] C0 1 | w[once] z r1 | f[rmb] ; mov r0 1 | | r[once] r3 x ; f[wmb] | | ; w[once] y 1 | | ; filter true Observed 2:r3=0; 2:r2=1; 1:r1=1;