nondeterministic formula no_15 = (12-(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 modules in state (15) module generic_process no_0 : [0..12] init 12; // No modules in state (0) no_1 : [0..12] init 0; // No modules in state (1) no_2 : [0..12] init 0; // No modules in state (2) no_3 : [0..12] init 0; // No modules in state (3) no_4 : [0..12] init 0; // No modules in state (4) no_5 : [0..12] init 0; // No modules in state (5) no_6 : [0..12] init 0; // No modules in state (6) no_7 : [0..12] init 0; // No modules in state (7) no_8 : [0..12] init 0; // No modules in state (8) no_9 : [0..12] init 0; // No modules in state (9) no_10 : [0..12] init 0; // No modules in state (10) no_11 : [0..12] init 0; // No modules in state (11) no_12 : [0..12] init 0; // No modules in state (12) no_13 : [0..12] init 0; // No modules in state (13) no_14 : [0..12] init 0; // No modules in state (14) [] (no_0>0) -> 1:true; [] (no_0>0) -> 1:(no_0'=no_0-1)&(no_1'=no_1+1); [] (no_1>0) -> 1:(no_1'=no_1-1)&(no_2'=no_2+1); [] (no_2>0) & (((no_0+no_1+no_2+no_3+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_12+no_13+no_14+no_15=12)&(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_13+no_14+no_15=12)&(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_14+no_15=12))|((no_14>0)|(no_15>0))) -> 1:(no_2'=no_2-1)&(no_3'=no_3+1); [] (no_2>0) & !(((no_0+no_1+no_2+no_3+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_12+no_13+no_14+no_15=12)&(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_13+no_14+no_15=12)&(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_14+no_15=12))|((no_14>0)|(no_15>0))) -> 1:true; [] (no_3>0) -> 1:(no_3'=no_3-1)&(no_4'=no_4+1); [] (no_3>0) -> 1:(no_3'=no_3-1)&(no_7'=no_7+1); [] (no_4>0) & ((no_4>1)|(no_5>0)|(no_10>0)|(no_11>0)|(no_12>0)|(no_13>0)|(no_14>0)|(no_15>0)) -> 1:(no_4'=no_4-1)&(no_5'=no_5+1); [] (no_4>0) & !((no_4>1)|(no_5>0)|(no_10>0)|(no_11>0)|(no_12>0)|(no_13>0)|(no_14>0)|(no_15>0)) -> 1:(no_4'=no_4-1)&(no_10'=no_10+1); [] (no_5>0) -> 1:(no_5'=no_5-1)&(no_6'=no_6+1); [] (no_6>0) & ((no_4>0)|(no_5>0)|(no_10>0)|(no_11>0)|(no_12>0)|(no_13>0)|(no_14>0)|(no_15>0)) -> 1:true; [] (no_6>0) & !((no_4>0)|(no_5>0)|(no_10>0)|(no_11>0)|(no_12>0)|(no_13>0)|(no_14>0)|(no_15>0)) -> 1:(no_6'=no_6-1)&(no_9'=no_9+1); [] (no_7>0) & ((no_0+no_1+no_2+no_3+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_12+no_13+no_14+no_15=12)&(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_13+no_14+no_15=12)&(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_14+no_15=12)&(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_15=12)&(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=12)) -> 1:(no_7'=no_7-1)&(no_8'=no_8+1); [] (no_7>0) & !((no_0+no_1+no_2+no_3+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_12+no_13+no_14+no_15=12)&(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_13+no_14+no_15=12)&(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_14+no_15=12)&(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_15=12)&(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=12)) -> 1:true; [] (no_8>0) -> 1:(no_8'=no_8-1)&(no_9'=no_9+1); [] (no_9>0) -> 0.5:(no_9'=no_9-1)&(no_4'=no_4+1) + 0.5:(no_9'=no_9-1)&(no_7'=no_7+1); [] (no_10>0) -> 1:(no_10'=no_10-1)&(no_11'=no_11+1); [] (no_11>0) & ((no_0+no_1+no_2+no_3+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_12+no_13+no_14+no_15=11)&(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_13+no_14+no_15=12)&(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_14+no_15=12)) -> 1:(no_11'=no_11-1)&(no_13'=no_13+1); [] (no_11>0) & !((no_0+no_1+no_2+no_3+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_10+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_11+no_12+no_13+no_14+no_15=12)&(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_12+no_13+no_14+no_15=11)&(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_13+no_14+no_15=12)&(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_14+no_15=12)) -> 1:(no_11'=no_11-1)&(no_12'=no_12+1); [] (no_12>0) -> 1:(no_12'=no_12-1)&(no_0'=no_0+1); [] (no_13>0) -> 1:(no_13'=no_13-1)&(no_14'=no_14+1); [] (no_14>0) & ((no_0+no_1+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=12)&(no_0+no_1+no_2+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)) -> 1:(no_14'=no_14-1); [] (no_14>0) & !((no_0+no_1+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=12)&(no_0+no_1+no_2+no_4+no_5+no_6+no_7+no_8+no_9+no_10+no_11+no_12+no_13+no_14+no_15=12)) -> 1:true; [] (no_15>0) -> 1:(no_0'=no_0+1); endmodule