ctmc

const int k;
const int n = k * 4;
const double r = 0.4 / n;

// process algebra coding style
module Raf 

  Raf : [ 0..n ] init k * 4;

  [ r1 ] ( Raf > 0 ) -> Raf * r : ( Raf' = Raf - 1 );
  [ r2 ] ( Raf < n ) -> 1 : ( Raf' = Raf + 1 );
  [ r6 ] ( Raf < n ) -> 1 : ( Raf' = Raf + 1 );

endmodule

module RasGTP

  RasGTP : [ 0..n ] init k * 1;

  [ r1 ] ( RasGTP > 0 ) -> RasGTP * r : ( RasGTP' = RasGTP - 1 );
  [ r2 ] ( RasGTP < n ) -> 1 : ( RasGTP' = RasGTP + 1 );
  [ r3 ] ( RasGTP < n ) -> 1 : ( RasGTP' = RasGTP + 1 );

endmodule

module Raf_RasGTP

  Raf_RasGTP : [ 0..n ] init 0;

  [ r2 ] ( Raf_RasGTP > 0 ) -> Raf_RasGTP * r : ( Raf_RasGTP' = Raf_RasGTP - 1 );
  [ r3 ] ( Raf_RasGTP > 0 ) -> Raf_RasGTP * r : ( Raf_RasGTP' = Raf_RasGTP - 1 );
  [ r1 ] ( Raf_RasGTP < n ) -> 1 : ( Raf_RasGTP' = Raf_RasGTP + 1 );

endmodule

module RafP

  RafP : [ 0..n ] init 0;

  [ r4 ] ( RafP > 0 ) -> RafP * r : ( RafP' = RafP - 1 );
  [ r7 ] ( RafP > 0 ) -> RafP * r : ( RafP' = RafP - 1 );
  [ r10 ] ( RafP > 0 ) -> RafP * r : ( RafP' = RafP - 1 );
  [ r3 ] ( RafP < n ) -> 1 : ( RafP' = RafP + 1 );
  [ r5 ] ( RafP < n ) -> 1 : ( RafP' = RafP + 1 );
  [ r8 ] ( RafP < n ) -> 1 : ( RafP' = RafP + 1 );
  [ r9 ] ( RafP < n ) -> 1 : ( RafP' = RafP + 1 );
  [ r11 ] ( RafP < n ) -> 1 : ( RafP' = RafP + 1 );
  [ r12 ] ( RafP < n ) -> 1 : ( RafP' = RafP + 1 );


endmodule

module Phase1

  Phase1 : [ 0..n ] init k * 3;

  [ r4 ] ( Phase1 > 0 ) -> Phase1 * r : ( Phase1' = Phase1 - 1 );
  [ r5 ] ( Phase1 < n ) -> 1 : ( Phase1' = Phase1 + 1 );
  [ r6 ] ( Phase1 < n ) -> 1 : ( Phase1' = Phase1 + 1 );

endmodule

module RafP_Phase1

  RafP_Phase1 : [ 0..n ] init 0;

  [ r5 ] ( RafP_Phase1 > 0 ) -> RafP_Phase1 * r : ( RafP_Phase1' = RafP_Phase1 - 1 );
  [ r6 ] ( RafP_Phase1 > 0 ) -> RafP_Phase1 * r : ( RafP_Phase1' = RafP_Phase1 - 1 );
  [ r4 ] ( RafP_Phase1 < n ) -> 1 : ( RafP_Phase1' = RafP_Phase1 + 1 );

endmodule

module MEK

  MEK : [ 0..n ] init k * 2;

  [ r7 ] ( MEK > 0 ) -> MEK * r : ( MEK' = MEK - 1 );
  [ r8 ] ( MEK < n ) -> 1 : ( MEK' = MEK + 1 );
  [ r18 ] ( MEK < n ) -> 1 : ( MEK' = MEK + 1 );

endmodule

module MEK_RafP

  MEK_RafP : [ 0..n ] init 0;

  [ r8 ] ( MEK_RafP > 0 ) -> MEK_RafP * r : ( MEK_RafP' = MEK_RafP - 1 );
  [ r9 ] ( MEK_RafP > 0 ) -> MEK_RafP * r : ( MEK_RafP' = MEK_RafP - 1 );
  [ r7 ] ( MEK_RafP < n ) -> 1 : ( MEK_RafP' = MEK_RafP + 1 );

endmodule

module MEKP

  MEKP : [ 0..n ] init 0;

  [ r10 ] ( MEKP > 0 ) -> MEKP * r : ( MEKP' = MEKP - 1 );
  [ r16 ] ( MEKP > 0 ) -> MEKP * r : ( MEKP' = MEKP - 1 );
  [ r9 ] ( MEKP < n ) -> 1 : ( MEKP' = MEKP + 1 );
  [ r11 ] ( MEKP < n ) -> 1 : ( MEKP' = MEKP + 1 );
  [ r15 ] ( MEKP < n ) -> 1 : ( MEKP' = MEKP + 1 );
  [ r17 ] ( MEKP < n ) -> 1 : ( MEKP' = MEKP + 1 );

endmodule

module MEKP_RafP

  MEKP_RafP : [ 0..n ] init 0;

  [ r11 ] ( MEKP_RafP > 0 ) -> MEKP_RafP * r : ( MEKP_RafP' = MEKP_RafP - 1 );
  [ r12 ] ( MEKP_RafP > 0 ) -> MEKP_RafP * r : ( MEKP_RafP' = MEKP_RafP - 1 );
  [ r10 ] ( MEKP_RafP < n ) -> 1 : ( MEKP_RafP' = MEKP_RafP + 1 );

endmodule

module MEKPP

  MEKPP : [ 0..n ] init 0;

  [ r13 ] ( MEKPP > 0 ) -> MEKPP * r : ( MEKPP' = MEKPP - 1 );
  [ r19 ] ( MEKPP > 0 ) -> MEKPP * r : ( MEKPP' = MEKPP - 1 );
  [ r22 ] ( MEKPP > 0 ) -> MEKPP * r : ( MEKPP' = MEKPP - 1 );
  [ r12 ] ( MEKPP < n ) -> 1 : ( MEKPP' = MEKPP + 1 );
  [ r14 ] ( MEKPP < n ) -> 1 : ( MEKPP' = MEKPP + 1 );
  [ r20 ] ( MEKPP < n ) -> 1 : ( MEKPP' = MEKPP + 1 );
  [ r21 ] ( MEKPP < n ) -> 1 : ( MEKPP' = MEKPP + 1 );
  [ r23 ] ( MEKPP < n ) -> 1 : ( MEKPP' = MEKPP + 1 );
  [ r24 ] ( MEKPP < n ) -> 1 : ( MEKPP' = MEKPP + 1 );

endmodule

module Phase2

  Phase2 : [ 0..n ] init k * 2;

  [ r13 ] ( Phase2 > 0 ) -> Phase2 * r : ( Phase2' = Phase2 - 1 );
  [ r16 ] ( Phase2 > 0 ) -> Phase2 * r : ( Phase2' = Phase2 - 1 );
  [ r14 ] ( Phase2 < n ) -> 1 : ( Phase2' = Phase2 + 1 );
  [ r15 ] ( Phase2 < n ) -> 1 : ( Phase2' = Phase2 + 1 );
  [ r17 ] ( Phase2 < n ) -> 1 : ( Phase2' = Phase2 + 1 );
  [ r18 ] ( Phase2 < n ) -> 1 : ( Phase2' = Phase2 + 1 );

endmodule

module MEKPP_Phase2

  MEKPP_Phase2 : [ 0..n ] init 0;

  [ r14 ] ( MEKPP_Phase2 > 0 ) -> MEKPP_Phase2 * r : ( MEKPP_Phase2' = MEKPP_Phase2 - 1 );
  [ r15 ] ( MEKPP_Phase2 > 0 ) -> MEKPP_Phase2 * r : ( MEKPP_Phase2' = MEKPP_Phase2 - 1 );
  [ r13 ] ( MEKPP_Phase2 < n ) -> 1 : ( MEKPP_Phase2' = MEKPP_Phase2 + 1 );

endmodule

module MEKP_Phase2

  MEKP_Phase2 : [ 0..n ] init 0;

  [ r17 ] ( MEKP_Phase2 > 0 ) -> MEKP_Phase2 * r : ( MEKP_Phase2' = MEKP_Phase2 - 1 );
  [ r18 ] ( MEKP_Phase2 > 0 ) -> MEKP_Phase2 * r : ( MEKP_Phase2' = MEKP_Phase2 - 1 );
  [ r16 ] ( MEKP_Phase2 < n ) -> 1 : ( MEKP_Phase2' = MEKP_Phase2 + 1 );

endmodule

module ERK

  ERK : [ 0..n ] init k * 3;

  [ r19 ] ( ERK > 0 ) -> ERK * r : ( ERK' = ERK - 1 );
  [ r20 ] ( ERK < n ) -> 1 : ( ERK' = ERK + 1 );
  [ r30 ] ( ERK < n ) -> 1 : ( ERK' = ERK + 1 );

endmodule

module ERK_MEKPP

  ERK_MEKPP : [ 0..n ] init 0;

  [ r20 ] ( ERK_MEKPP > 0 ) -> ERK_MEKPP * r : ( ERK_MEKPP' = ERK_MEKPP - 1 );
  [ r21 ] ( ERK_MEKPP > 0 ) -> ERK_MEKPP * r : ( ERK_MEKPP' = ERK_MEKPP - 1 );
  [ r19 ] ( ERK_MEKPP < n ) -> 1 : ( ERK_MEKPP' = ERK_MEKPP + 1 );

endmodule

module ERKP

  ERKP : [ 0..n ] init 0;

  [ r22 ] ( ERKP > 0 ) -> ERKP * r : ( ERKP' = ERKP - 1 );
  [ r28 ] ( ERKP > 0 ) -> ERKP * r : ( ERKP' = ERKP - 1 );
  [ r21 ] ( ERKP < n ) -> 1 : ( ERKP' = ERKP + 1 );
  [ r23 ] ( ERKP < n ) -> 1 : ( ERKP' = ERKP + 1 );
  [ r27 ] ( ERKP < n ) -> 1 : ( ERKP' = ERKP + 1 );
  [ r29 ] ( ERKP < n ) -> 1 : ( ERKP' = ERKP + 1 );

endmodule

module ERKP_MEKPP

  ERKP_MEKPP : [ 0..n ] init 0;

  [ r23 ] ( ERKP_MEKPP > 0 ) -> ERKP_MEKPP * r : ( ERKP_MEKPP' = ERKP_MEKPP - 1 );
  [ r24 ] ( ERKP_MEKPP > 0 ) -> ERKP_MEKPP * r : ( ERKP_MEKPP' = ERKP_MEKPP - 1 );
  [ r22 ] ( ERKP_MEKPP < n ) -> 1 : ( ERKP_MEKPP' = ERKP_MEKPP + 1 );

endmodule

module ERKPP

  ERKPP : [ 0..n ] init 0;

  [ r25 ] ( ERKPP > 0 ) -> ERKPP * r : ( ERKPP' = ERKPP - 1 );
  [ r24 ] ( ERKPP < n ) -> 1 : ( ERKPP' = ERKPP + 1 );
  [ r26 ] ( ERKPP < n ) -> 1 : ( ERKPP' = ERKPP + 1 );

endmodule

module Phase3

  Phase3 : [ 0..n ] init k * 3;

  [ r25 ] ( Phase3 > 0 ) -> Phase3 * r : ( Phase3' = Phase3 - 1 );
  [ r28 ] ( Phase3 > 0 ) -> Phase3 * r : ( Phase3' = Phase3 - 1 );
  [ r26 ] ( Phase3 < n ) -> 1 : ( Phase3' = Phase3 + 1 );
  [ r27 ] ( Phase3 < n ) -> 1 : ( Phase3' = Phase3 + 1 );
  [ r29 ] ( Phase3 < n ) -> 1 : ( Phase3' = Phase3 + 1 );
  [ r30 ] ( Phase3 < n ) -> 1 : ( Phase3' = Phase3 + 1 );

endmodule

module ERKPP_Phase3

  ERKPP_Phase3 : [ 0..n ] init 0;

  [ r26 ] ( ERKPP_Phase3 > 0 ) -> ERKPP_Phase3 * r : ( ERKPP_Phase3' = ERKPP_Phase3 - 1 );
  [ r27 ] ( ERKPP_Phase3 > 0 ) -> ERKPP_Phase3 * r : ( ERKPP_Phase3' = ERKPP_Phase3 - 1 );
  [ r25 ] ( ERKPP_Phase3 < n ) -> 1 : ( ERKPP_Phase3' = ERKPP_Phase3 + 1 );

endmodule

module ERKP_Phase3

  ERKP_Phase3 : [ 0..n ] init 0;

  [ r29 ] ( ERKP_Phase3 > 0 ) -> ERKP_Phase3 * r : ( ERKP_Phase3' = ERKP_Phase3 - 1 );
  [ r30 ] ( ERKP_Phase3 > 0 ) -> ERKP_Phase3 * r : ( ERKP_Phase3' = ERKP_Phase3 - 1 );
  [ r28 ] ( ERKP_Phase3 < n ) -> 1 : ( ERKP_Phase3' = ERKP_Phase3 + 1 );

endmodule

module Constants

  x : bool init true;

  [ r1 ] ( x = true ) -> 1 / r : ( x' = true );
  [ r2 ] ( x = true ) -> 0.4 / r : ( x' = true );
  [ r3 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r4 ] ( x = true ) -> 0.5 / r : ( x' = true );
  [ r5 ] ( x = true ) -> 0.5 / r : ( x' = true );
  [ r6 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r7 ] ( x = true ) -> 3.3 / r : ( x' = true );
  [ r8 ] ( x = true ) -> 0.42 / r : ( x' = true );
  [ r9 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r10 ] ( x = true ) -> 3.3 / r : ( x' = true );
  [ r11 ] ( x = true ) -> 0.4 / r : ( x' = true );
  [ r12 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r13 ] ( x = true ) -> 10 / r : ( x' = true );
  [ r14 ] ( x = true ) -> 0.8 / r : ( x' = true );
  [ r15 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r16 ] ( x = true ) -> 10 / r : ( x' = true );
  [ r17 ] ( x = true ) -> 0.8 / r : ( x' = true );
  [ r18 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r19 ] ( x = true ) -> 20 / r : ( x' = true );
  [ r20 ] ( x = true ) -> 0.6 / r : ( x' = true );
  [ r21 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r22 ] ( x = true ) -> 20 / r : ( x' = true );
  [ r23 ] ( x = true ) -> 0.6 / r : ( x' = true );
  [ r24 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r25 ] ( x = true ) -> 5 / r : ( x' = true );
  [ r26 ] ( x = true ) -> 0.4 / r : ( x' = true );
  [ r27 ] ( x = true ) -> 0.1 / r : ( x' = true );
  [ r28 ] ( x = true ) -> 5 / r : ( x' = true );
  [ r29 ] ( x = true ) -> 0.4 / r : ( x' = true );
  [ r30 ] ( x = true ) -> 0.1 / r : ( x' = true );

endmodule

rewards

  true : RafP * ( 0.1 / k );

endrewards