PRISM code: mutex12.forgrip.nm

nondeterministic

module process1

  s1 : [0..15] init 0;

  [] s1=0 -> 1:(s1'=0);
  [] s1=0 -> 1:(s1'=1);
  [] s1=1 -> 1:(s1'=2);
  [] s1=2 & (((s2!=4 & s3!=4 & s4!=4 & s5!=4 & s6!=4 & s7!=4 & s8!=4 & s9!=4 & s10!=4 & s11!=4 & s12!=4) & (s2!=5 & s3!=5 & s4!=5 & s5!=5 & s6!=5 & s7!=5 & s8!=5 & s9!=5 & s10!=5 & s11!=5 & s12!=5) & (s2!=6 & s3!=6 & s4!=6 & s5!=6 & s6!=6 & s7!=6 & s8!=6 & s9!=6 & s10!=6 & s11!=6 & s12!=6) & (s2!=7 & s3!=7 & s4!=7 & s5!=7 & s6!=7 & s7!=7 & s8!=7 & s9!=7 & s10!=7 & s11!=7 & s12!=7) & (s2!=8 & s3!=8 & s4!=8 & s5!=8 & s6!=8 & s7!=8 & s8!=8 & s9!=8 & s10!=8 & s11!=8 & s12!=8) & (s2!=9 & s3!=9 & s4!=9 & s5!=9 & s6!=9 & s7!=9 & s8!=9 & s9!=9 & s10!=9 & s11!=9 & s12!=9) & (s2!=10 & s3!=10 & s4!=10 & s5!=10 & s6!=10 & s7!=10 & s8!=10 & s9!=10 & s10!=10 & s11!=10 & s12!=10) & (s2!=11 & s3!=11 & s4!=11 & s5!=11 & s6!=11 & s7!=11 & s8!=11 & s9!=11 & s10!=11 & s11!=11 & s12!=11) & (s2!=12 & s3!=12 & s4!=12 & s5!=12 & s6!=12 & s7!=12 & s8!=12 & s9!=12 & s10!=12 & s11!=12 & s12!=12) & (s2!=13 & s3!=13 & s4!=13 & s5!=13 & s6!=13 & s7!=13 & s8!=13 & s9!=13 & s10!=13 & s11!=13 & s12!=13)) | ((s2=14 | s3=14 | s4=14 | s5=14 | s6=14 | s7=14 | s8=14 | s9=14 | s10=14 | s11=14 | s12=14) | (s2=15 | s3=15 | s4=15 | s5=15 | s6=15 | s7=15 | s8=15 | s9=15 | s10=15 | s11=15 | s12=15))) -> 1:(s1'=3);
  [] s1=2 & !(((s2!=4 & s3!=4 & s4!=4 & s5!=4 & s6!=4 & s7!=4 & s8!=4 & s9!=4 & s10!=4 & s11!=4 & s12!=4) & (s2!=5 & s3!=5 & s4!=5 & s5!=5 & s6!=5 & s7!=5 & s8!=5 & s9!=5 & s10!=5 & s11!=5 & s12!=5) & (s2!=6 & s3!=6 & s4!=6 & s5!=6 & s6!=6 & s7!=6 & s8!=6 & s9!=6 & s10!=6 & s11!=6 & s12!=6) & (s2!=7 & s3!=7 & s4!=7 & s5!=7 & s6!=7 & s7!=7 & s8!=7 & s9!=7 & s10!=7 & s11!=7 & s12!=7) & (s2!=8 & s3!=8 & s4!=8 & s5!=8 & s6!=8 & s7!=8 & s8!=8 & s9!=8 & s10!=8 & s11!=8 & s12!=8) & (s2!=9 & s3!=9 & s4!=9 & s5!=9 & s6!=9 & s7!=9 & s8!=9 & s9!=9 & s10!=9 & s11!=9 & s12!=9) & (s2!=10 & s3!=10 & s4!=10 & s5!=10 & s6!=10 & s7!=10 & s8!=10 & s9!=10 & s10!=10 & s11!=10 & s12!=10) & (s2!=11 & s3!=11 & s4!=11 & s5!=11 & s6!=11 & s7!=11 & s8!=11 & s9!=11 & s10!=11 & s11!=11 & s12!=11) & (s2!=12 & s3!=12 & s4!=12 & s5!=12 & s6!=12 & s7!=12 & s8!=12 & s9!=12 & s10!=12 & s11!=12 & s12!=12) & (s2!=13 & s3!=13 & s4!=13 & s5!=13 & s6!=13 & s7!=13 & s8!=13 & s9!=13 & s10!=13 & s11!=13 & s12!=13)) | ((s2=14 | s3=14 | s4=14 | s5=14 | s6=14 | s7=14 | s8=14 | s9=14 | s10=14 | s11=14 | s12=14) | (s2=15 | s3=15 | s4=15 | s5=15 | s6=15 | s7=15 | s8=15 | s9=15 | s10=15 | s11=15 | s12=15))) -> 1:(s1'=2);
  [] s1=3 -> 1:(s1'=4);
  [] s1=3 -> 1:(s1'=7);
  [] s1=4 & ((s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4 | s11=4 | s12=4) | (s2=5 | s3=5 | s4=5 | s5=5 | s6=5 | s7=5 | s8=5 | s9=5 | s10=5 | s11=5 | s12=5) | (s2=10 | s3=10 | s4=10 | s5=10 | s6=10 | s7=10 | s8=10 | s9=10 | s10=10 | s11=10 | s12=10) | (s2=11 | s3=11 | s4=11 | s5=11 | s6=11 | s7=11 | s8=11 | s9=11 | s10=11 | s11=11 | s12=11) | (s2=12 | s3=12 | s4=12 | s5=12 | s6=12 | s7=12 | s8=12 | s9=12 | s10=12 | s11=12 | s12=12) | (s2=13 | s3=13 | s4=13 | s5=13 | s6=13 | s7=13 | s8=13 | s9=13 | s10=13 | s11=13 | s12=13) | (s2=14 | s3=14 | s4=14 | s5=14 | s6=14 | s7=14 | s8=14 | s9=14 | s10=14 | s11=14 | s12=14) | (s2=15 | s3=15 | s4=15 | s5=15 | s6=15 | s7=15 | s8=15 | s9=15 | s10=15 | s11=15 | s12=15)) -> 1:(s1'=5);
  [] s1=4 & !((s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4 | s11=4 | s12=4) | (s2=5 | s3=5 | s4=5 | s5=5 | s6=5 | s7=5 | s8=5 | s9=5 | s10=5 | s11=5 | s12=5) | (s2=10 | s3=10 | s4=10 | s5=10 | s6=10 | s7=10 | s8=10 | s9=10 | s10=10 | s11=10 | s12=10) | (s2=11 | s3=11 | s4=11 | s5=11 | s6=11 | s7=11 | s8=11 | s9=11 | s10=11 | s11=11 | s12=11) | (s2=12 | s3=12 | s4=12 | s5=12 | s6=12 | s7=12 | s8=12 | s9=12 | s10=12 | s11=12 | s12=12) | (s2=13 | s3=13 | s4=13 | s5=13 | s6=13 | s7=13 | s8=13 | s9=13 | s10=13 | s11=13 | s12=13) | (s2=14 | s3=14 | s4=14 | s5=14 | s6=14 | s7=14 | s8=14 | s9=14 | s10=14 | s11=14 | s12=14) | (s2=15 | s3=15 | s4=15 | s5=15 | s6=15 | s7=15 | s8=15 | s9=15 | s10=15 | s11=15 | s12=15)) -> 1:(s1'=10);
  [] s1=5 -> 1:(s1'=6);
  [] s1=6 & ((s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4 | s11=4 | s12=4) | (s2=5 | s3=5 | s4=5 | s5=5 | s6=5 | s7=5 | s8=5 | s9=5 | s10=5 | s11=5 | s12=5) | (s2=10 | s3=10 | s4=10 | s5=10 | s6=10 | s7=10 | s8=10 | s9=10 | s10=10 | s11=10 | s12=10) | (s2=11 | s3=11 | s4=11 | s5=11 | s6=11 | s7=11 | s8=11 | s9=11 | s10=11 | s11=11 | s12=11) | (s2=12 | s3=12 | s4=12 | s5=12 | s6=12 | s7=12 | s8=12 | s9=12 | s10=12 | s11=12 | s12=12) | (s2=13 | s3=13 | s4=13 | s5=13 | s6=13 | s7=13 | s8=13 | s9=13 | s10=13 | s11=13 | s12=13) | (s2=14 | s3=14 | s4=14 | s5=14 | s6=14 | s7=14 | s8=14 | s9=14 | s10=14 | s11=14 | s12=14) | (s2=15 | s3=15 | s4=15 | s5=15 | s6=15 | s7=15 | s8=15 | s9=15 | s10=15 | s11=15 | s12=15)) -> 1:(s1'=6);
  [] s1=6 & !((s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4 | s11=4 | s12=4) | (s2=5 | s3=5 | s4=5 | s5=5 | s6=5 | s7=5 | s8=5 | s9=5 | s10=5 | s11=5 | s12=5) | (s2=10 | s3=10 | s4=10 | s5=10 | s6=10 | s7=10 | s8=10 | s9=10 | s10=10 | s11=10 | s12=10) | (s2=11 | s3=11 | s4=11 | s5=11 | s6=11 | s7=11 | s8=11 | s9=11 | s10=11 | s11=11 | s12=11) | (s2=12 | s3=12 | s4=12 | s5=12 | s6=12 | s7=12 | s8=12 | s9=12 | s10=12 | s11=12 | s12=12) | (s2=13 | s3=13 | s4=13 | s5=13 | s6=13 | s7=13 | s8=13 | s9=13 | s10=13 | s11=13 | s12=13) | (s2=14 | s3=14 | s4=14 | s5=14 | s6=14 | s7=14 | s8=14 | s9=14 | s10=14 | s11=14 | s12=14) | (s2=15 | s3=15 | s4=15 | s5=15 | s6=15 | s7=15 | s8=15 | s9=15 | s10=15 | s11=15 | s12=15)) -> 1:(s1'=9);
  [] s1=7 & ((s2!=4 & s3!=4 & s4!=4 & s5!=4 & s6!=4 & s7!=4 & s8!=4 & s9!=4 & s10!=4 & s11!=4 & s12!=4) & (s2!=5 & s3!=5 & s4!=5 & s5!=5 & s6!=5 & s7!=5 & s8!=5 & s9!=5 & s10!=5 & s11!=5 & s12!=5) & (s2!=6 & s3!=6 & s4!=6 & s5!=6 & s6!=6 & s7!=6 & s8!=6 & s9!=6 & s10!=6 & s11!=6 & s12!=6) & (s2!=9 & s3!=9 & s4!=9 & s5!=9 & s6!=9 & s7!=9 & s8!=9 & s9!=9 & s10!=9 & s11!=9 & s12!=9) & (s2!=10 & s3!=10 & s4!=10 & s5!=10 & s6!=10 & s7!=10 & s8!=10 & s9!=10 & s10!=10 & s11!=10 & s12!=10) & (s2!=11 & s3!=11 & s4!=11 & s5!=11 & s6!=11 & s7!=11 & s8!=11 & s9!=11 & s10!=11 & s11!=11 & s12!=11) & (s2!=12 & s3!=12 & s4!=12 & s5!=12 & s6!=12 & s7!=12 & s8!=12 & s9!=12 & s10!=12 & s11!=12 & s12!=12) & (s2!=13 & s3!=13 & s4!=13 & s5!=13 & s6!=13 & s7!=13 & s8!=13 & s9!=13 & s10!=13 & s11!=13 & s12!=13) & (s2!=14 & s3!=14 & s4!=14 & s5!=14 & s6!=14 & s7!=14 & s8!=14 & s9!=14 & s10!=14 & s11!=14 & s12!=14) & (s2!=15 & s3!=15 & s4!=15 & s5!=15 & s6!=15 & s7!=15 & s8!=15 & s9!=15 & s10!=15 & s11!=15 & s12!=15)) -> 1:(s1'=8);
  [] s1=7 & !((s2!=4 & s3!=4 & s4!=4 & s5!=4 & s6!=4 & s7!=4 & s8!=4 & s9!=4 & s10!=4 & s11!=4 & s12!=4) & (s2!=5 & s3!=5 & s4!=5 & s5!=5 & s6!=5 & s7!=5 & s8!=5 & s9!=5 & s10!=5 & s11!=5 & s12!=5) & (s2!=6 & s3!=6 & s4!=6 & s5!=6 & s6!=6 & s7!=6 & s8!=6 & s9!=6 & s10!=6 & s11!=6 & s12!=6) & (s2!=9 & s3!=9 & s4!=9 & s5!=9 & s6!=9 & s7!=9 & s8!=9 & s9!=9 & s10!=9 & s11!=9 & s12!=9) & (s2!=10 & s3!=10 & s4!=10 & s5!=10 & s6!=10 & s7!=10 & s8!=10 & s9!=10 & s10!=10 & s11!=10 & s12!=10) & (s2!=11 & s3!=11 & s4!=11 & s5!=11 & s6!=11 & s7!=11 & s8!=11 & s9!=11 & s10!=11 & s11!=11 & s12!=11) & (s2!=12 & s3!=12 & s4!=12 & s5!=12 & s6!=12 & s7!=12 & s8!=12 & s9!=12 & s10!=12 & s11!=12 & s12!=12) & (s2!=13 & s3!=13 & s4!=13 & s5!=13 & s6!=13 & s7!=13 & s8!=13 & s9!=13 & s10!=13 & s11!=13 & s12!=13) & (s2!=14 & s3!=14 & s4!=14 & s5!=14 & s6!=14 & s7!=14 & s8!=14 & s9!=14 & s10!=14 & s11!=14 & s12!=14) & (s2!=15 & s3!=15 & s4!=15 & s5!=15 & s6!=15 & s7!=15 & s8!=15 & s9!=15 & s10!=15 & s11!=15 & s12!=15)) -> 1:(s1'=7);
  [] s1=8 -> 1:(s1'=9);
  [] s1=9 -> 0.5:(s1'=4) + 0.5:(s1'=7);
  [] s1=10 -> 1:(s1'=11);
  [] s1=11 & ((s2!=4 & s3!=4 & s4!=4 & s5!=4 & s6!=4 & s7!=4 & s8!=4 & s9!=4 & s10!=4 & s11!=4 & s12!=4) & (s2!=5 & s3!=5 & s4!=5 & s5!=5 & s6!=5 & s7!=5 & s8!=5 & s9!=5 & s10!=5 & s11!=5 & s12!=5) & (s2!=6 & s3!=6 & s4!=6 & s5!=6 & s6!=6 & s7!=6 & s8!=6 & s9!=6 & s10!=6 & s11!=6 & s12!=6) & (s2!=7 & s3!=7 & s4!=7 & s5!=7 & s6!=7 & s7!=7 & s8!=7 & s9!=7 & s10!=7 & s11!=7 & s12!=7) & (s2!=8 & s3!=8 & s4!=8 & s5!=8 & s6!=8 & s7!=8 & s8!=8 & s9!=8 & s10!=8 & s11!=8 & s12!=8) & (s2!=9 & s3!=9 & s4!=9 & s5!=9 & s6!=9 & s7!=9 & s8!=9 & s9!=9 & s10!=9 & s11!=9 & s12!=9) & (s2!=10 & s3!=10 & s4!=10 & s5!=10 & s6!=10 & s7!=10 & s8!=10 & s9!=10 & s10!=10 & s11!=10 & s12!=10) & (s2!=11 & s3!=11 & s4!=11 & s5!=11 & s6!=11 & s7!=11 & s8!=11 & s9!=11 & s10!=11 & s11!=11 & s12!=11) & (s2!=12 & s3!=12 & s4!=12 & s5!=12 & s6!=12 & s7!=12 & s8!=12 & s9!=12 & s10!=12 & s11!=12 & s12!=12) & (s2!=13 & s3!=13 & s4!=13 & s5!=13 & s6!=13 & s7!=13 & s8!=13 & s9!=13 & s10!=13 & s11!=13 & s12!=13)) -> 1:(s1'=13);
  [] s1=11 & !((s2!=4 & s3!=4 & s4!=4 & s5!=4 & s6!=4 & s7!=4 & s8!=4 & s9!=4 & s10!=4 & s11!=4 & s12!=4) & (s2!=5 & s3!=5 & s4!=5 & s5!=5 & s6!=5 & s7!=5 & s8!=5 & s9!=5 & s10!=5 & s11!=5 & s12!=5) & (s2!=6 & s3!=6 & s4!=6 & s5!=6 & s6!=6 & s7!=6 & s8!=6 & s9!=6 & s10!=6 & s11!=6 & s12!=6) & (s2!=7 & s3!=7 & s4!=7 & s5!=7 & s6!=7 & s7!=7 & s8!=7 & s9!=7 & s10!=7 & s11!=7 & s12!=7) & (s2!=8 & s3!=8 & s4!=8 & s5!=8 & s6!=8 & s7!=8 & s8!=8 & s9!=8 & s10!=8 & s11!=8 & s12!=8) & (s2!=9 & s3!=9 & s4!=9 & s5!=9 & s6!=9 & s7!=9 & s8!=9 & s9!=9 & s10!=9 & s11!=9 & s12!=9) & (s2!=10 & s3!=10 & s4!=10 & s5!=10 & s6!=10 & s7!=10 & s8!=10 & s9!=10 & s10!=10 & s11!=10 & s12!=10) & (s2!=11 & s3!=11 & s4!=11 & s5!=11 & s6!=11 & s7!=11 & s8!=11 & s9!=11 & s10!=11 & s11!=11 & s12!=11) & (s2!=12 & s3!=12 & s4!=12 & s5!=12 & s6!=12 & s7!=12 & s8!=12 & s9!=12 & s10!=12 & s11!=12 & s12!=12) & (s2!=13 & s3!=13 & s4!=13 & s5!=13 & s6!=13 & s7!=13 & s8!=13 & s9!=13 & s10!=13 & s11!=13 & s12!=13)) -> 1:(s1'=12);
  [] s1=12 -> 1:(s1'=0);
  [] s1=13 -> 1:(s1'=14);
  [] s1=14 & ((s2!=2 & s3!=2 & s4!=2 & s5!=2 & s6!=2 & s7!=2 & s8!=2 & s9!=2 & s10!=2 & s11!=2 & s12!=2) & (s2!=3 & s3!=3 & s4!=3 & s5!=3 & s6!=3 & s7!=3 & s8!=3 & s9!=3 & s10!=3 & s11!=3 & s12!=3)) -> 1:(s1'=15);
  [] s1=14 & !((s2!=2 & s3!=2 & s4!=2 & s5!=2 & s6!=2 & s7!=2 & s8!=2 & s9!=2 & s10!=2 & s11!=2 & s12!=2) & (s2!=3 & s3!=3 & s4!=3 & s5!=3 & s6!=3 & s7!=3 & s8!=3 & s9!=3 & s10!=3 & s11!=3 & s12!=3)) -> 1:(s1'=14);
  [] s1=15 -> 1:(s1'=0);
endmodule

module process2 = process1 [ s1 = s2, s2 = s1 ] endmodule
module process3 = process1 [ s1 = s3, s3 = s1 ] endmodule
module process4 = process1 [ s1 = s4, s4 = s1 ] endmodule
module process5 = process1 [ s1 = s5, s5 = s1 ] endmodule
module process6 = process1 [ s1 = s6, s6 = s1 ] endmodule
module process7 = process1 [ s1 = s7, s7 = s1 ] endmodule
module process8 = process1 [ s1 = s8, s8 = s1 ] endmodule
module process9 = process1 [ s1 = s9, s9 = s1 ] endmodule
module process10 = process1 [ s1 = s10, s10 = s1 ] endmodule
module process11 = process1 [ s1 = s11, s11 = s1 ] endmodule
module process12 = process1 [ s1 = s12, s12 = s1 ] endmodule