LISA LISA-ppo-weakness (* ppo sequences shouldn't need to end with an Alpha-strong-ppo link. This example's cycle is: strong-prop, rd-addr, obs. *) { x=v; 1:r0=u; } P0 | P1 | P2 ; r[lderef] r0 x | w[once] y 2 | w[once] u 1 ; r[once] r1 r0 | f[mb] | f[wmb] ; r[once] r2 y | w[once] x r0 | w[once] y 1 ; Observed y=2; 0:r2=1; 0:r1=1; 0:r0=u; and y=2; 0:r2=0; 0:r1=1; 0:r0=u; and y=1; 0:r2=0; 0:r1=1; 0:r0=u; and y=1; 0:r2=0; 0:r1=0; 0:r0=u;