spec

ctrl M = 2;
ctrl R = 0;
ctrl T = 0;
ctrl ND = 5;


react rx1 =
	(M{b,a}.1 | M{b,c}.1) || ND{x,a,b,c,d}.1
	-->
	(x/{x0,x1} M{x0,x1}.1 | x/{x0,x1} M{x0,x1}.1) || ND{x,a,b,c,d}.1;

react rx2 =
	(M{b,a}.1 | M{b,c}.1) || (M{c,d}.1 | M{a,d}.1) || ND{x,a,b,c,d}.1
	-->
	(M{b,x}.1 | M{b,c}.1) || (M{c,d}.1 | M{x,d}.1) || ND{x,a,b,c,d}.1;


big w1 = R.(M{b,a}.1 | M{b,c}.1) | T.(T.(M{c,d}.1 | M{a,d}.1)) || R.(ND{x,a,b,c,d}.1);

big phi = w/{w0,w1} M{w0,w1}.1;

begin brs
  init w1;
  rules = [ {rx1,rx2} ];
  preds = { phi };
end