Test LISA-cpord-obs-failure

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=1; y2=1; x3=2; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;