PRISM code: mutex12.fromgrip.nm

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