PRISM code: fgf4.fromgrip.sm

ctmc

global fgf : [ 0 .. 4 ] init 4 ; 
global src : [ 0 .. 4 ] init 4 ; 
global grb : [ 0 .. 4 ] init 4 ; 

formula no_18 = (4-(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_16+no_17));    // No modules in state (1,0,0,0,0,0)

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

  [] (no_0>0) & (fgf>0) -> no_0*1250*fgf:(fgf'=fgf-1)&(no_0'=no_0-1)&(no_1'=no_1+1);
  [] (no_2>0) & (fgf>0) -> no_2*1250*fgf:(fgf'=fgf-1)&(no_2'=no_2-1)&(no_3'=no_3+1);
  [] (no_4>0) & (fgf>0) -> no_4*1250*fgf:(fgf'=fgf-1)&(no_4'=no_4-1)&(no_5'=no_5+1);
  [] (no_6>0) & (fgf>0) -> no_6*1250*fgf:(fgf'=fgf-1)&(no_6'=no_6-1)&(no_7'=no_7+1);
  [] (no_8>0) & (fgf>0) -> no_8*1250*fgf:(fgf'=fgf-1)&(no_8'=no_8-1)&(no_9'=no_9+1);
  [] (no_10>0) & (fgf>0) -> no_10*1250*fgf:(fgf'=fgf-1)&(no_10'=no_10-1)&(no_11'=no_11+1);
  [] (no_12>0) & (fgf>0) -> no_12*1250*fgf:(fgf'=fgf-1)&(no_12'=no_12-1)&(no_13'=no_13+1);
  [] (no_14>0) & (fgf>0) -> no_14*1250*fgf:(fgf'=fgf-1)&(no_14'=no_14-1)&(no_15'=no_15+1);
  [] (no_16>0) & (fgf>0) -> no_16*1250*fgf:(fgf'=fgf-1)&(no_16'=no_16-1)&(no_17'=no_17+1);
  [] (no_1>0) & fgf<4 -> no_1*0.002:(fgf'=fgf+1)&(no_1'=no_1-1)&(no_0'=no_0+1);
  [] (no_3>0) & fgf<4 -> no_3*0.002:(fgf'=fgf+1)&(no_3'=no_3-1)&(no_2'=no_2+1);
  [] (no_5>0) & fgf<4 -> no_5*0.002:(fgf'=fgf+1)&(no_5'=no_5-1)&(no_4'=no_4+1);
  [] (no_7>0) & fgf<4 -> no_7*0.002:(fgf'=fgf+1)&(no_7'=no_7-1)&(no_6'=no_6+1);
  [] (no_9>0) & fgf<4 -> no_9*0.002:(fgf'=fgf+1)&(no_9'=no_9-1)&(no_8'=no_8+1);
  [] (no_11>0) & fgf<4 -> no_11*0.002:(fgf'=fgf+1)&(no_11'=no_11-1)&(no_10'=no_10+1);
  [] (no_13>0) & fgf<4 -> no_13*0.002:(fgf'=fgf+1)&(no_13'=no_13-1)&(no_12'=no_12+1);
  [] (no_15>0) & fgf<4 -> no_15*0.002:(fgf'=fgf+1)&(no_15'=no_15-1)&(no_14'=no_14+1);
  [] (no_17>0) & fgf<4 -> no_17*0.002:(fgf'=fgf+1)&(no_17'=no_17-1)&(no_16'=no_16+1);
  [] (no_1>0) -> no_1*0.1:(no_1'=no_1-1)&(no_3'=no_3+1);
  [] (no_5>0) -> no_5*0.1:(no_5'=no_5-1)&(no_7'=no_7+1);
  [] (no_9>0) -> no_9*0.1:(no_9'=no_9-1)&(no_11'=no_11+1);
  [] (no_1>0) -> no_1*0.1:(no_1'=no_1-1)&(no_5'=no_5+1);
  [] (no_3>0) -> no_3*0.1:(no_3'=no_3-1)&(no_7'=no_7+1);
  [] (no_13>0) -> no_13*0.1:(no_13'=no_13-1)&(no_15'=no_15+1);
  [] (no_2>0) -> no_2*0.1:(no_2'=no_2-1)&(no_0'=no_0+1);
  [] (no_3>0) -> no_3*0.1:(no_3'=no_3-1)&(no_1'=no_1+1);
  [] (no_6>0) -> no_6*0.1:(no_6'=no_6-1)&(no_4'=no_4+1);
  [] (no_7>0) -> no_7*0.1:(no_7'=no_7-1)&(no_5'=no_5+1);
  [] (no_10>0) -> no_10*0.1:(no_10'=no_10-1)&(no_8'=no_8+1);
  [] (no_11>0) -> no_11*0.1:(no_11'=no_11-1)&(no_9'=no_9+1);
  [] (no_4>0) -> no_4*0.1:(no_4'=no_4-1)&(no_0'=no_0+1);
  [] (no_5>0) -> no_5*0.1:(no_5'=no_5-1)&(no_1'=no_1+1);
  [] (no_6>0) -> no_6*0.1:(no_6'=no_6-1)&(no_2'=no_2+1);
  [] (no_7>0) -> no_7*0.1:(no_7'=no_7-1)&(no_3'=no_3+1);
  [] (no_14>0) -> no_14*0.1:(no_14'=no_14-1)&(no_12'=no_12+1);
  [] (no_15>0) -> no_15*0.1:(no_15'=no_15-1)&(no_13'=no_13+1);
  [] (no_12>0) & src<4 -> no_12*0.1:(src'=src+1)&(no_12'=no_12-1)&(no_0'=no_0+1);
  [] (no_13>0) & src<4 -> no_13*0.1:(src'=src+1)&(no_13'=no_13-1)&(no_1'=no_1+1);
  [] (no_14>0) & src<4 -> no_14*0.1:(src'=src+1)&(no_14'=no_14-1)&(no_4'=no_4+1);
  [] (no_15>0) & src<4 -> no_15*0.1:(src'=src+1)&(no_15'=no_15-1)&(no_5'=no_5+1);
  [] (no_16>0) & src<4 -> no_16*0.1:(src'=src+1)&(no_16'=no_16-1)&(no_8'=no_8+1);
  [] (no_17>0) & src<4 -> no_17*0.1:(src'=src+1)&(no_17'=no_17-1)&(no_9'=no_9+1);
  [] (no_8>0) & grb<4 -> no_8*0.1:(grb'=grb+1)&(no_8'=no_8-1)&(no_0'=no_0+1);
  [] (no_9>0) & grb<4 -> no_9*0.1:(grb'=grb+1)&(no_9'=no_9-1)&(no_1'=no_1+1);
  [] (no_10>0) & grb<4 -> no_10*0.1:(grb'=grb+1)&(no_10'=no_10-1)&(no_2'=no_2+1);
  [] (no_11>0) & grb<4 -> no_11*0.1:(grb'=grb+1)&(no_11'=no_11-1)&(no_3'=no_3+1);
  [] (no_16>0) & grb<4 -> no_16*0.1:(grb'=grb+1)&(no_16'=no_16-1)&(no_12'=no_12+1);
  [] (no_17>0) & grb<4 -> no_17*0.1:(grb'=grb+1)&(no_17'=no_17-1)&(no_13'=no_13+1);
  [] (no_2>0) & src>0 -> no_2*2*src:(src'=src-1)&(no_2'=no_2-1)&(no_12'=no_12+1);
  [] (no_3>0) & src>0 -> no_3*2*src:(src'=src-1)&(no_3'=no_3-1)&(no_13'=no_13+1);
  [] (no_6>0) & src>0 -> no_6*2*src:(src'=src-1)&(no_6'=no_6-1)&(no_14'=no_14+1);
  [] (no_7>0) & src>0 -> no_7*2*src:(src'=src-1)&(no_7'=no_7-1)&(no_15'=no_15+1);
  [] (no_10>0) & src>0 -> no_10*2*src:(src'=src-1)&(no_10'=no_10-1)&(no_16'=no_16+1);
  [] (no_11>0) & src>0 -> no_11*2*src:(src'=src-1)&(no_11'=no_11-1)&(no_17'=no_17+1);
  [] (no_4>0) & grb>0 -> no_4*2*grb:(grb'=grb-1)&(no_4'=no_4-1)&(no_8'=no_8+1);
  [] (no_5>0) & grb>0 -> no_5*2*grb:(grb'=grb-1)&(no_5'=no_5-1)&(no_9'=no_9+1);
  [] (no_6>0) & grb>0 -> no_6*2*grb:(grb'=grb-1)&(no_6'=no_6-1)&(no_10'=no_10+1);
  [] (no_7>0) & grb>0 -> no_7*2*grb:(grb'=grb-1)&(no_7'=no_7-1)&(no_11'=no_11+1);
  [] (no_14>0) & grb>0 -> no_14*2*grb:(grb'=grb-1)&(no_14'=no_14-1)&(no_16'=no_16+1);
  [] (no_15>0) & grb>0 -> no_15*2*grb:(grb'=grb-1)&(no_15'=no_15-1)&(no_17'=no_17+1);
  [] (no_12>0) & src<4 -> no_12*0.02:(src'=src+1)&(no_12'=no_12-1)&(no_2'=no_2+1);
  [] (no_13>0) & src<4 -> no_13*0.02:(src'=src+1)&(no_13'=no_13-1)&(no_3'=no_3+1);
  [] (no_14>0) & src<4 -> no_14*0.02:(src'=src+1)&(no_14'=no_14-1)&(no_6'=no_6+1);
  [] (no_15>0) & src<4 -> no_15*0.02:(src'=src+1)&(no_15'=no_15-1)&(no_7'=no_7+1);
  [] (no_16>0) & src<4 -> no_16*0.02:(src'=src+1)&(no_16'=no_16-1)&(no_10'=no_10+1);
  [] (no_17>0) & src<4 -> no_17*0.02:(src'=src+1)&(no_17'=no_17-1)&(no_11'=no_11+1);
  [] (no_8>0) & grb<4 -> no_8*0.02:(grb'=grb+1)&(no_8'=no_8-1)&(no_4'=no_4+1);
  [] (no_9>0) & grb<4 -> no_9*0.02:(grb'=grb+1)&(no_9'=no_9-1)&(no_5'=no_5+1);
  [] (no_10>0) & grb<4 -> no_10*0.02:(grb'=grb+1)&(no_10'=no_10-1)&(no_6'=no_6+1);
  [] (no_11>0) & grb<4 -> no_11*0.02:(grb'=grb+1)&(no_11'=no_11-1)&(no_7'=no_7+1);
  [] (no_16>0) & grb<4 -> no_16*0.02:(grb'=grb+1)&(no_16'=no_16-1)&(no_14'=no_14+1);
  [] (no_17>0) & grb<4 -> no_17*0.02:(grb'=grb+1)&(no_17'=no_17-1)&(no_15'=no_15+1);
  [] (no_12>0) -> no_12*0.0011111111111111111:(no_12'=no_12-1);
  [] (no_13>0) -> no_13*0.0011111111111111111:(no_13'=no_13-1);
  [] (no_14>0) -> no_14*0.0011111111111111111:(no_14'=no_14-1);
  [] (no_15>0) -> no_15*0.0011111111111111111:(no_15'=no_15-1);
  [] (no_16>0) -> no_16*0.0011111111111111111:(no_16'=no_16-1);
  [] (no_17>0) -> no_17*0.0011111111111111111:(no_17'=no_17-1);

endmodule