…
LISA LISA-cpord-obs-failure
(* This test should be forbidden, but it isn't.
P0 P1 P2 P3 P4 P5
Rx1=1 Rx2=1 Wx3=2 Wx4=1 Wy2=2 Wy3=2
data dep mb mb wmb wmb wmb
a:Wx2=1 Wx3=1 Rx4=0 Wy1=1 wy3=1 Wx1=1
Ry1=1
data dep
b:Wy2=1
a: ->rfe 1:Rx2 ->mb 1:Wx3 ->co 2:Wx3 ->mb 2:Rx4 ->fre 3:Wx4 ->wmb
3:Wy1 ->hb* b:
b: ->co 4:Wy2 ->wmb 4:Wy3 ->co 5:Wy3 ->wmb 5:Wx1 ->hb* a:
Since wmb is B-cumulative, if a: executes before b: then we get
b: ->cpord* 5:Wy3 ->wmb 5:Wx1 ->hb* a: ->hb b:
and so b: ->cpord* b:. If b: executes before a: then we get
1:Wx3 ->co 2:Wx3 ->mb 2:Rx4 ->fre 3:Wx4 ->wmb 3:Wy1 ->hb*
b: ->hb a: ->rfe 1:Rx2 ->mb 1:Wx3
and so 1:Wx3 ->cpord* 2:Rx4 -> strong-prop 1:Wx3.
Either way, there is a violation of the propagation check.
*)
{
}
P0 | P1 | P2 | P3 | P4 | P5 ;
r[once] r0 x1 | r[once] r2 x2 | w[once] x3 2 | w[once] x4 1 | w[once] y2 2 | w[once] y3 2 ;
w[once] x2 r0 | f[mb] | f[mb] | f[wmb] | f[wmb] | f[wmb] ;
r[once] r1 y1 | w[once] x3 1 | r[once] r4 x4 | w[once] y1 1 | w[once] y3 1 | w[once] x1 1 ;
w[once] y2 r1 | | | | | ;
Observed
y3=2; y2=2; x3=2; 2:r4=1; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=1; y2=2; x3=2; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=1; x3=2; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=1; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=1; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=1; 1:r2=0; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=0; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=0; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=0; 0:r1=0; 0:r0=1;