PRISM code: byzantine8.fromgrip.nm

mdp

global nzero : [ 0 .. 5 ] ; 
global mainone_zero : [ 0 .. 1 ] ; 
global mainone_one : [ 0 .. 1 ] ; 
global mainone_abs : [ 0 .. 1 ] ; 
global preone_zero : [ 0 .. 8 ] ; 
global preone_one : [ 0 .. 8 ] ; 
global pretwo_zero : [ 0 .. 1 ] ; 
global pretwo_one : [ 0 .. 1 ] ; 

module adversary

  mainzero_zero : [ 0 .. 1 ] ; 
  mainzero_one : [ 0 .. 1 ] ; 

  [] (mainzero_zero=0)&(mainzero_one=0) -> (mainzero_zero'=1);
  [] (mainzero_zero=0)&(mainzero_one=0) -> (mainzero_one'=1);
endmodule

module coinone

  fone : [ 0 .. 1 ] ; 
  coinone : [ 0 .. 1 ] ; 

  [] (coinone=0)&(nzero>=5) -> 0.5:(fone'=0)&(coinone'=1)+0.5:(fone'=1)&(coinone'=1);
endmodule

module cointwo

  ftwo : [ 0 .. 1 ] ; 
  cointwo : [ 0 .. 1 ] ; 

  [] (cointwo=0)&(nzero>=5) -> 0.5:(ftwo'=0)&(cointwo'=1)+0.5:(ftwo'=1)&(cointwo'=1);
endmodule

formula no_9 = (8-(no_0+no_1+no_2+no_3+no_4+no_5+no_6+no_7+no_8));    // No modules in state (9)

module generic_process
 no_0 : [0..8] init 8;    // No modules in state (0)
 no_1 : [0..8] init 0;    // No modules in state (1)
 no_2 : [0..8] init 0;    // No modules in state (2)
 no_3 : [0..8] init 0;    // No modules in state (3)
 no_4 : [0..8] init 0;    // No modules in state (4)
 no_5 : [0..8] init 0;    // No modules in state (5)
 no_6 : [0..8] init 0;    // No modules in state (6)
 no_7 : [0..8] init 0;    // No modules in state (7)
 no_8 : [0..8] init 0;    // No modules in state (8)

  [] (no_0>0) & (mainzero_zero=1) -> (nzero'=min(5,nzero+1))&(no_0'=no_0-1)&(no_1'=no_1+1);
  [] (no_0>0) & (mainzero_one=1) -> (nzero'=min(5,nzero+1))&(no_0'=no_0-1)&(no_2'=no_2+1);
  [] (no_0>0) -> (nzero'=min(5,nzero+1))&(no_0'=no_0-1)&(no_3'=no_3+1);
  [] (no_1>0) & (coinone=1) -> (preone_zero'=min(8,preone_zero+1))&(no_1'=no_1-1)&(no_4'=no_4+1);
  [] (no_2>0) & (coinone=1) -> (preone_one'=min(8,preone_one+1))&(no_2'=no_2-1)&(no_4'=no_4+1);
  [] (no_3>0) & (coinone=1)&(fone=0) -> (preone_zero'=min(8,preone_zero+1))&(no_3'=no_3-1)&(no_4'=no_4+1);
  [] (no_3>0) & (coinone=1)&(fone=1) -> (preone_one'=min(8,preone_one+1))&(no_3'=no_3-1)&(no_4'=no_4+1);
  [] (no_4>0) & (preone_zero+preone_one>=5)&((preone_zero>0)|(fone=0)|(mainzero_zero=1))&((preone_one>0)|(fone=1)|(mainzero_one=1)) -> (mainone_abs'=1)&(no_4'=no_4-1)&(no_5'=no_5+1);
  [] (no_4>0) & (preone_zero+preone_one>=5)&(preone_zero>=5) -> (mainone_zero'=1)&(no_4'=no_4-1)&(no_5'=no_5+1);
  [] (no_4>0) & (preone_zero+preone_one>=5)&(preone_one>=5) -> (mainone_one'=1)&(no_4'=no_4-1)&(no_5'=no_5+1);
  [] (no_5>0) & (mainone_abs=1) -> (no_5'=no_5-1)&(no_6'=no_6+1);
  [] (no_5>0) & ((mainone_zero=1)|(preone_zero>=5)) -> (no_5'=no_5-1)&(no_7'=no_7+1);
  [] (no_5>0) & ((mainone_one=1)|(preone_one>=5)) -> (no_5'=no_5-1)&(no_8'=no_8+1);
  [] (no_6>0) & (cointwo=1)&(ftwo=0) -> (pretwo_zero'=1)&(no_6'=no_6-1);
  [] (no_6>0) & (cointwo=1)&(ftwo=1) -> (pretwo_one'=1)&(no_6'=no_6-1);
  [] (no_7>0) & (cointwo=1) -> (pretwo_zero'=1)&(no_7'=no_7-1);
  [] (no_8>0) & (cointwo=1) -> (pretwo_one'=1)&(no_8'=no_8-1);

endmodule