LISA Alan05
(* This test is forbidden if release/acquire is B-cumulative and is
allowed otherwise.
*)
{
}
P0 | P1 | P2 ;
w[once] x 1 | r[acquire] r1 y | r[acquire] r2 z ;
w[release] y 1 | w[once] z 1 | r[once] r3 x ;
Observed
2:r3=0; 2:r2=1; 1:r1=1;