PRISM code: rabin5.fromgrip.nm

mdp

global c : [ 0 .. 1 ] ; 
global b : [ 0 .. 7 ] ; 
global r : [ 1 .. 2 ] ; 

formula no_16 = (5-(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15));    // No modules in state (2,0,0)

module generic_process
 no_0 : [0..5] init 5;    // No modules in state (0,0,0)
 no_1 : [0..5] init 0;    // No modules in state (1,0,0)
 no_2 : [0..5] init 0;    // No modules in state (1,1,1)
 no_3 : [0..5] init 0;    // No modules in state (1,1,2)
 no_4 : [0..5] init 0;    // No modules in state (1,2,1)
 no_5 : [0..5] init 0;    // No modules in state (1,2,2)
 no_6 : [0..5] init 0;    // No modules in state (1,3,1)
 no_7 : [0..5] init 0;    // No modules in state (1,3,2)
 no_8 : [0..5] init 0;    // No modules in state (1,4,1)
 no_9 : [0..5] init 0;    // No modules in state (1,4,2)
 no_10 : [0..5] init 0;    // No modules in state (1,5,1)
 no_11 : [0..5] init 0;    // No modules in state (1,5,2)
 no_12 : [0..5] init 0;    // No modules in state (1,6,1)
 no_13 : [0..5] init 0;    // No modules in state (1,6,2)
 no_14 : [0..5] init 0;    // No modules in state (1,7,1)
 no_15 : [0..5] init 0;    // No modules in state (1,7,2)

  [] (no_0>0) -> true;
  [] (no_0>0) -> (no_0'=no_0-1)&(no_1'=no_1+1);
  [] (no_1>0) & (r=1) & (b<0|1!=0) -> 0.5:(b'=max(b,1))&(no_1'=no_1-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_1'=no_1-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_1'=no_1-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_1'=no_1-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_1'=no_1-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_1'=no_1-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_1'=no_1-1)&(no_14'=no_14+1);
  [] (no_2>0) & (r=1) & (b<1|1!=1) -> 0.5:(b'=max(b,1)) + 0.25:(b'=max(b,2))&(no_2'=no_2-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_2'=no_2-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_2'=no_2-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_2'=no_2-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_2'=no_2-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_2'=no_2-1)&(no_14'=no_14+1);
  [] (no_3>0) & (r=1) & (b<1|1!=2) -> 0.5:(b'=max(b,1))&(no_3'=no_3-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_3'=no_3-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_3'=no_3-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_3'=no_3-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_3'=no_3-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_3'=no_3-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_3'=no_3-1)&(no_14'=no_14+1);
  [] (no_4>0) & (r=1) & (b<2|1!=1) -> 0.5:(b'=max(b,1))&(no_4'=no_4-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2)) + 0.125:(b'=max(b,3))&(no_4'=no_4-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_4'=no_4-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_4'=no_4-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_4'=no_4-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_4'=no_4-1)&(no_14'=no_14+1);
  [] (no_5>0) & (r=1) & (b<2|1!=2) -> 0.5:(b'=max(b,1))&(no_5'=no_5-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_5'=no_5-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_5'=no_5-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_5'=no_5-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_5'=no_5-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_5'=no_5-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_5'=no_5-1)&(no_14'=no_14+1);
  [] (no_6>0) & (r=1) & (b<3|1!=1) -> 0.5:(b'=max(b,1))&(no_6'=no_6-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_6'=no_6-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3)) + 0.0625:(b'=max(b,4))&(no_6'=no_6-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_6'=no_6-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_6'=no_6-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_6'=no_6-1)&(no_14'=no_14+1);
  [] (no_7>0) & (r=1) & (b<3|1!=2) -> 0.5:(b'=max(b,1))&(no_7'=no_7-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_7'=no_7-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_7'=no_7-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_7'=no_7-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_7'=no_7-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_7'=no_7-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_7'=no_7-1)&(no_14'=no_14+1);
  [] (no_8>0) & (r=1) & (b<4|1!=1) -> 0.5:(b'=max(b,1))&(no_8'=no_8-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_8'=no_8-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_8'=no_8-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4)) + 0.03125:(b'=max(b,5))&(no_8'=no_8-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_8'=no_8-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_8'=no_8-1)&(no_14'=no_14+1);
  [] (no_9>0) & (r=1) & (b<4|1!=2) -> 0.5:(b'=max(b,1))&(no_9'=no_9-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_9'=no_9-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_9'=no_9-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_9'=no_9-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_9'=no_9-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_9'=no_9-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_9'=no_9-1)&(no_14'=no_14+1);
  [] (no_10>0) & (r=1) & (b<5|1!=1) -> 0.5:(b'=max(b,1))&(no_10'=no_10-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_10'=no_10-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_10'=no_10-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_10'=no_10-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5)) + 0.015625:(b'=max(b,6))&(no_10'=no_10-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_10'=no_10-1)&(no_14'=no_14+1);
  [] (no_11>0) & (r=1) & (b<5|1!=2) -> 0.5:(b'=max(b,1))&(no_11'=no_11-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_11'=no_11-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_11'=no_11-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_11'=no_11-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_11'=no_11-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_11'=no_11-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_11'=no_11-1)&(no_14'=no_14+1);
  [] (no_12>0) & (r=1) & (b<6|1!=1) -> 0.5:(b'=max(b,1))&(no_12'=no_12-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_12'=no_12-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_12'=no_12-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_12'=no_12-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_12'=no_12-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6)) + 0.015625:(b'=max(b,7))&(no_12'=no_12-1)&(no_14'=no_14+1);
  [] (no_13>0) & (r=1) & (b<6|1!=2) -> 0.5:(b'=max(b,1))&(no_13'=no_13-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_13'=no_13-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_13'=no_13-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_13'=no_13-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_13'=no_13-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_13'=no_13-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_13'=no_13-1)&(no_14'=no_14+1);
  [] (no_14>0) & (r=1) & (b<7|1!=1) -> 0.5:(b'=max(b,1))&(no_14'=no_14-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_14'=no_14-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_14'=no_14-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_14'=no_14-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_14'=no_14-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_14'=no_14-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7));
  [] (no_15>0) & (r=1) & (b<7|1!=2) -> 0.5:(b'=max(b,1))&(no_15'=no_15-1)&(no_2'=no_2+1) + 0.25:(b'=max(b,2))&(no_15'=no_15-1)&(no_4'=no_4+1) + 0.125:(b'=max(b,3))&(no_15'=no_15-1)&(no_6'=no_6+1) + 0.0625:(b'=max(b,4))&(no_15'=no_15-1)&(no_8'=no_8+1) + 0.03125:(b'=max(b,5))&(no_15'=no_15-1)&(no_10'=no_10+1) + 0.015625:(b'=max(b,6))&(no_15'=no_15-1)&(no_12'=no_12+1) + 0.015625:(b'=max(b,7))&(no_15'=no_15-1)&(no_14'=no_14+1);
  [] (no_1>0) & (r=2) & (b<0|2!=0) -> 0.5:(b'=max(b,1))&(no_1'=no_1-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_1'=no_1-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_1'=no_1-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_1'=no_1-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_1'=no_1-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_1'=no_1-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_1'=no_1-1)&(no_15'=no_15+1);
  [] (no_2>0) & (r=2) & (b<1|2!=1) -> 0.5:(b'=max(b,1))&(no_2'=no_2-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_2'=no_2-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_2'=no_2-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_2'=no_2-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_2'=no_2-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_2'=no_2-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_2'=no_2-1)&(no_15'=no_15+1);
  [] (no_3>0) & (r=2) & (b<1|2!=2) -> 0.5:(b'=max(b,1)) + 0.25:(b'=max(b,2))&(no_3'=no_3-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_3'=no_3-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_3'=no_3-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_3'=no_3-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_3'=no_3-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_3'=no_3-1)&(no_15'=no_15+1);
  [] (no_4>0) & (r=2) & (b<2|2!=1) -> 0.5:(b'=max(b,1))&(no_4'=no_4-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_4'=no_4-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_4'=no_4-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_4'=no_4-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_4'=no_4-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_4'=no_4-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_4'=no_4-1)&(no_15'=no_15+1);
  [] (no_5>0) & (r=2) & (b<2|2!=2) -> 0.5:(b'=max(b,1))&(no_5'=no_5-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2)) + 0.125:(b'=max(b,3))&(no_5'=no_5-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_5'=no_5-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_5'=no_5-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_5'=no_5-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_5'=no_5-1)&(no_15'=no_15+1);
  [] (no_6>0) & (r=2) & (b<3|2!=1) -> 0.5:(b'=max(b,1))&(no_6'=no_6-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_6'=no_6-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_6'=no_6-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_6'=no_6-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_6'=no_6-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_6'=no_6-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_6'=no_6-1)&(no_15'=no_15+1);
  [] (no_7>0) & (r=2) & (b<3|2!=2) -> 0.5:(b'=max(b,1))&(no_7'=no_7-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_7'=no_7-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3)) + 0.0625:(b'=max(b,4))&(no_7'=no_7-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_7'=no_7-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_7'=no_7-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_7'=no_7-1)&(no_15'=no_15+1);
  [] (no_8>0) & (r=2) & (b<4|2!=1) -> 0.5:(b'=max(b,1))&(no_8'=no_8-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_8'=no_8-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_8'=no_8-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_8'=no_8-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_8'=no_8-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_8'=no_8-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_8'=no_8-1)&(no_15'=no_15+1);
  [] (no_9>0) & (r=2) & (b<4|2!=2) -> 0.5:(b'=max(b,1))&(no_9'=no_9-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_9'=no_9-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_9'=no_9-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4)) + 0.03125:(b'=max(b,5))&(no_9'=no_9-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_9'=no_9-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_9'=no_9-1)&(no_15'=no_15+1);
  [] (no_10>0) & (r=2) & (b<5|2!=1) -> 0.5:(b'=max(b,1))&(no_10'=no_10-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_10'=no_10-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_10'=no_10-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_10'=no_10-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_10'=no_10-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_10'=no_10-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_10'=no_10-1)&(no_15'=no_15+1);
  [] (no_11>0) & (r=2) & (b<5|2!=2) -> 0.5:(b'=max(b,1))&(no_11'=no_11-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_11'=no_11-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_11'=no_11-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_11'=no_11-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5)) + 0.015625:(b'=max(b,6))&(no_11'=no_11-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_11'=no_11-1)&(no_15'=no_15+1);
  [] (no_12>0) & (r=2) & (b<6|2!=1) -> 0.5:(b'=max(b,1))&(no_12'=no_12-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_12'=no_12-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_12'=no_12-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_12'=no_12-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_12'=no_12-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_12'=no_12-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_12'=no_12-1)&(no_15'=no_15+1);
  [] (no_13>0) & (r=2) & (b<6|2!=2) -> 0.5:(b'=max(b,1))&(no_13'=no_13-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_13'=no_13-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_13'=no_13-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_13'=no_13-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_13'=no_13-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6)) + 0.015625:(b'=max(b,7))&(no_13'=no_13-1)&(no_15'=no_15+1);
  [] (no_14>0) & (r=2) & (b<7|2!=1) -> 0.5:(b'=max(b,1))&(no_14'=no_14-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_14'=no_14-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_14'=no_14-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_14'=no_14-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_14'=no_14-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_14'=no_14-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7))&(no_14'=no_14-1)&(no_15'=no_15+1);
  [] (no_15>0) & (r=2) & (b<7|2!=2) -> 0.5:(b'=max(b,1))&(no_15'=no_15-1)&(no_3'=no_3+1) + 0.25:(b'=max(b,2))&(no_15'=no_15-1)&(no_5'=no_5+1) + 0.125:(b'=max(b,3))&(no_15'=no_15-1)&(no_7'=no_7+1) + 0.0625:(b'=max(b,4))&(no_15'=no_15-1)&(no_9'=no_9+1) + 0.03125:(b'=max(b,5))&(no_15'=no_15-1)&(no_11'=no_11+1) + 0.015625:(b'=max(b,6))&(no_15'=no_15-1)&(no_13'=no_13+1) + 0.015625:(b'=max(b,7));
  [] (no_1>0) & (b=0&r=0&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_1'=no_1-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_1'=no_1-1);
  [] (no_2>0) & (b=1&r=1&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_2'=no_2-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_2'=no_2-1);
  [] (no_3>0) & (b=1&r=2&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_3'=no_3-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_3'=no_3-1);
  [] (no_4>0) & (b=2&r=1&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_4'=no_4-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_4'=no_4-1);
  [] (no_5>0) & (b=2&r=2&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_5'=no_5-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_5'=no_5-1);
  [] (no_6>0) & (b=3&r=1&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_6'=no_6-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_6'=no_6-1);
  [] (no_7>0) & (b=3&r=2&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_7'=no_7-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_7'=no_7-1);
  [] (no_8>0) & (b=4&r=1&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_8'=no_8-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_8'=no_8-1);
  [] (no_9>0) & (b=4&r=2&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_9'=no_9-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_9'=no_9-1);
  [] (no_10>0) & (b=5&r=1&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_10'=no_10-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_10'=no_10-1);
  [] (no_11>0) & (b=5&r=2&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_11'=no_11-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_11'=no_11-1);
  [] (no_12>0) & (b=6&r=1&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_12'=no_12-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_12'=no_12-1);
  [] (no_13>0) & (b=6&r=2&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_13'=no_13-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_13'=no_13-1);
  [] (no_14>0) & (b=7&r=1&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_14'=no_14-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_14'=no_14-1);
  [] (no_15>0) & (b=7&r=2&c=0) -> 0.5:(r'=1)&(c'=1)&(b'=0)&(no_15'=no_15-1) + 0.5:(r'=2)&(c'=1)&(b'=0)&(no_15'=no_15-1);
  [] (no_1>0) & (0=r&0<=b&((c=0&0!=b)|c=1)) -> true;
  [] (no_2>0) & (1=r&1<=b&((c=0&1!=b)|c=1)) -> true;
  [] (no_3>0) & (2=r&1<=b&((c=0&1!=b)|c=1)) -> true;
  [] (no_4>0) & (1=r&2<=b&((c=0&2!=b)|c=1)) -> true;
  [] (no_5>0) & (2=r&2<=b&((c=0&2!=b)|c=1)) -> true;
  [] (no_6>0) & (1=r&3<=b&((c=0&3!=b)|c=1)) -> true;
  [] (no_7>0) & (2=r&3<=b&((c=0&3!=b)|c=1)) -> true;
  [] (no_8>0) & (1=r&4<=b&((c=0&4!=b)|c=1)) -> true;
  [] (no_9>0) & (2=r&4<=b&((c=0&4!=b)|c=1)) -> true;
  [] (no_10>0) & (1=r&5<=b&((c=0&5!=b)|c=1)) -> true;
  [] (no_11>0) & (2=r&5<=b&((c=0&5!=b)|c=1)) -> true;
  [] (no_12>0) & (1=r&6<=b&((c=0&6!=b)|c=1)) -> true;
  [] (no_13>0) & (2=r&6<=b&((c=0&6!=b)|c=1)) -> true;
  [] (no_14>0) & (1=r&7<=b&((c=0&7!=b)|c=1)) -> true;
  [] (no_15>0) & (2=r&7<=b&((c=0&7!=b)|c=1)) -> true;
  [] (no_16>0) -> (c'=0)&(no_0'=no_0+1);
  [] (no_16>0) -> true;

endmodule