ctmc

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

// SPN coding style
module levchenko

 // improvements possible by exploiting the p-invariants details

 RasGTP :      [ 0..n ] init k * 1;
 Raf :         [ 0..n ] init k * 4;
 Raf_RasGTP :  [ 0..n ] init 0;
 RafP :        [ 0..n ] init 0;
 RafP_Phase1 : [ 0..n ] init 0;

 MEK :         [ 0..n ] init k * 2;
 MEK_RafP :    [ 0..n ] init 0;
 MEKP :        [ 0..n ] init 0;
 MEKP_RafP :   [ 0..n ] init 0;
 MEKPP :       [ 0..n ] init 0;
 MEKPP_Phase2 :[ 0..n ] init 0;
 MEKP_Phase2 : [ 0..n ] init 0;

 ERK :         [ 0..n ] init k * 3;
 ERK_MEKPP :   [ 0..n ] init 0;
 ERKP :        [ 0..n ] init 0;
 ERKP_MEKPP :  [ 0..n ] init 0;
 ERKPP :       [ 0..n ] init 0;
 ERKPP_Phase3 :[ 0..n ] init 0;
 ERKP_Phase3 : [ 0..n ] init 0;

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


// this version brings the right results
// but it's actually to strong because the postplaces shouldn't overflow

[ r1 ] ( Raf > 0 ) & ( RasGTP > 0 ) & ( Raf_RasGTP < n )
          -> 1.0 * Raf * RasGTP * r : 
        ( Raf' = Raf - 1 ) & ( RasGTP' = RasGTP - 1 ) & ( Raf_RasGTP' = Raf_RasGTP + 1 );


[ r2 ] ( Raf_RasGTP > 0 ) & ( Raf < n ) & ( RasGTP < n )
          -> 0.4 * Raf_RasGTP :
        ( Raf_RasGTP' = Raf_RasGTP - 1 ) & ( Raf' = Raf + 1 ) & ( RasGTP' = RasGTP + 1 );

  
[ r3 ] ( Raf_RasGTP > 0 ) & ( RasGTP < n ) & ( RafP < n )
         -> 0.1 * Raf_RasGTP : 
       ( Raf_RasGTP' = Raf_RasGTP - 1 ) & ( RasGTP' = RasGTP + 1 ) & ( RafP' = RafP + 1 );


[ r4 ] ( RafP > 0 ) & ( Phase1 > 0 ) & ( RafP_Phase1 < n )
         ->  0.5 * RafP * Phase1 * r : 
       ( RafP' = RafP - 1 ) & ( Phase1' = Phase1 - 1 ) & ( RafP_Phase1' = RafP_Phase1 + 1 );


[ r5 ] ( RafP_Phase1 > 0 ) & ( RafP < n ) & ( Phase1 < n )
         -> 0.5 * RafP_Phase1 : 
       ( RafP_Phase1' = RafP_Phase1 - 1 ) & ( RafP' = RafP + 1 ) & ( Phase1' = Phase1 + 1 );

  
[ r6 ] ( RafP_Phase1 > 0 ) & ( Raf < n ) & ( Phase1 < n )
         -> 0.1 * RafP_Phase1 : 
       ( RafP_Phase1' = RafP_Phase1 - 1 ) & ( Raf' = Raf + 1 ) & ( Phase1' = Phase1 + 1 );


[ r7 ] ( RafP > 0 ) & ( MEK > 0 ) & ( MEK_RafP < n )
         -> 3.3 * RafP * MEK * r : 
       ( RafP' = RafP - 1 ) & ( MEK' = MEK - 1 ) & ( MEK_RafP' = MEK_RafP + 1 );

  
[ r8 ] ( MEK_RafP > 0 ) & ( RafP < n ) & ( MEK < n )
         -> 0.42 * MEK_RafP : 
       ( MEK_RafP' = MEK_RafP - 1 ) & ( RafP' = RafP + 1 ) & ( MEK' = MEK + 1 );

 
[ r9 ] ( MEK_RafP > 0 ) & ( RafP < n ) & ( MEKP < n )
         -> 0.1 * MEK_RafP :
       ( MEK_RafP' = MEK_RafP - 1 ) & ( RafP' = RafP + 1 ) & ( MEKP' = MEKP + 1 );

  
[ r10 ] ( MEKP > 0 ) & ( RafP > 0 ) & ( MEKP_RafP < n )  
          -> 3.3 * RafP * MEKP * r: 
        ( MEKP' = MEKP - 1 ) & ( RafP' = RafP - 1 ) & ( MEKP_RafP' = MEKP_RafP + 1 );


[ r11 ] ( MEKP_RafP > 0 ) & ( RafP < n ) & ( MEKP < n )
          -> 0.4 * MEKP_RafP : 
        ( MEKP_RafP' = MEKP_RafP - 1 ) & ( RafP' = RafP + 1 ) & ( MEKP' = MEKP + 1 );


[ r12 ] ( MEKP_RafP > 0 ) & ( RafP < n ) & ( MEKPP < n )
          -> 0.1 * MEKP_RafP : 
        ( MEKP_RafP' = MEKP_RafP - 1 ) & ( RafP' = RafP + 1 ) & ( MEKPP' = MEKPP + 1 );


[ r13 ] ( MEKPP > 0 ) & ( Phase2 > 0 ) & ( MEKPP_Phase2 < n )
          -> 10 * MEKPP * Phase2 * r :
        ( MEKPP' = MEKPP - 1 ) & ( Phase2' = Phase2 - 1 ) & ( MEKPP_Phase2' = MEKPP_Phase2 + 1 );


[ r14 ] ( MEKPP_Phase2 > 0 ) & ( MEKPP < n ) & ( Phase2 < n )
          -> 0.8 * MEKPP_Phase2 : 
        ( MEKPP_Phase2' = MEKPP_Phase2 - 1 ) & ( MEKPP' = MEKPP + 1 ) & ( Phase2' = Phase2 + 1 );


[ r15 ] ( MEKPP_Phase2 > 0 ) & ( MEKP < n ) & ( Phase2 < n )  
          -> 0.1 * MEKPP_Phase2 :  
        ( MEKPP_Phase2' = MEKPP_Phase2 - 1 ) & ( MEKP' = MEKP + 1 ) & ( Phase2' = Phase2 + 1 );


[ r16 ] ( MEKP > 0 ) & ( Phase2 > 0 ) &  ( MEKP_Phase2 < n ) 
          -> 10 * MEKP * Phase2 * r : 
        ( MEKP' = MEKP - 1 ) & ( Phase2' = Phase2 - 1 ) & ( MEKP_Phase2' = MEKP_Phase2 + 1 );
 
 
[ r17 ] ( MEKP_Phase2 > 0 ) & ( MEKP < n ) & ( Phase2 < n )
          -> 0.8 * MEKP_Phase2 : 
        ( MEKP_Phase2' = MEKP_Phase2 - 1 ) & ( MEKP' = MEKP + 1 ) & ( Phase2' = Phase2 + 1 );

 
[ r18 ] ( MEKP_Phase2 > 0 ) & ( MEK < n ) & ( Phase2 < n )
          -> 0.1 * MEKP_Phase2 : 
        ( MEKP_Phase2' = MEKP_Phase2 - 1 ) & ( MEK' = MEK + 1 ) & ( Phase2' = Phase2 + 1 );


[ r19 ] ( ERK > 0 ) & ( MEKPP > 0 ) & ( ERK_MEKPP < n )
          -> 20 * ERK * MEKPP * r :
        ( ERK' = ERK - 1 ) & ( MEKPP' = MEKPP - 1 ) & ( ERK_MEKPP' = ERK_MEKPP + 1 );


[ r20 ] ( ERK_MEKPP > 0 ) & ( ERK < n ) & ( MEKPP < n )
          -> 0.6 * ERK_MEKPP :
        ( ERK_MEKPP' = ERK_MEKPP - 1 ) & ( ERK' = ERK + 1 ) & ( MEKPP' = MEKPP + 1 );


[ r21 ] ( ERK_MEKPP > 0 ) & ( ERKP < n ) & ( MEKPP < n )
          -> 0.1 * ERK_MEKPP : 
        ( ERK_MEKPP' = ERK_MEKPP - 1 ) & ( ERKP' = ERKP + 1 ) & ( MEKPP' = MEKPP + 1 );


[ r22 ] ( ERKP > 0 ) & ( MEKPP > 0 ) & ( ERKP_MEKPP < n )
          -> 20 * ERKP * MEKPP * r : 
        ( ERKP' = ERKP - 1 ) & ( MEKPP' = MEKPP - 1 ) & ( ERKP_MEKPP' = ERKP_MEKPP + 1 );


[ r23 ] ( ERKP_MEKPP > 0 ) & ( ERKP < n ) & ( MEKPP < n )
          -> 0.6 * ERKP_MEKPP : 
        ( ERKP_MEKPP' = ERKP_MEKPP - 1 ) & ( ERKP' = ERKP + 1 ) & ( MEKPP' = MEKPP + 1 );


[ r24 ] ( ERKP_MEKPP > 0 ) & ( ERKPP < n ) & ( MEKPP < n ) 
          -> 0.1 * ERKP_MEKPP :
( ERKP_MEKPP' = ERKP_MEKPP - 1 ) & ( ERKPP' = ERKPP + 1 ) & ( MEKPP' = MEKPP + 1 );


[ r25 ] ( ERKPP > 0 ) & ( Phase3 > 0 ) & ( ERKPP_Phase3 < n )
          -> 5 * ERKPP * Phase3 *r : 
        ( ERKPP' = ERKPP - 1 ) & ( Phase3' = Phase3 - 1 ) & ( ERKPP_Phase3' = ERKPP_Phase3 + 1 );


[ r26 ] ( ERKPP_Phase3 > 0 ) & ( ERKPP < n ) & ( Phase3 < n )
          -> 0.4 * ERKPP_Phase3 :
        ( ERKPP_Phase3' = ERKPP_Phase3 - 1 ) & ( ERKPP' = ERKPP + 1 ) & ( Phase3' = Phase3 + 1 );


[ r27 ] ( ERKPP_Phase3 > 0 ) & ( ERKP < n ) & ( Phase3 < n )
          -> 0.1 * ERKPP_Phase3 :  
        ( ERKPP_Phase3' = ERKPP_Phase3 - 1 ) & ( ERKP' = ERKP + 1 ) & ( Phase3' = Phase3 + 1 );
  

[ r28 ] ( ERKP > 0 ) & ( Phase3 > 0 ) & ( ERKP_Phase3 < n )
          -> 5 * ERKP * Phase3 * r : 
        ( ERKP' = ERKP - 1 ) & ( Phase3' = Phase3 - 1 ) & ( ERKP_Phase3' = ERKP_Phase3 + 1 );


[ r29 ] ( ERKP_Phase3 > 0 ) & ( ERKP < n ) & ( Phase3 < n )
          -> 0.4 * ERKP_Phase3 :
        ( ERKP_Phase3' = ERKP_Phase3 - 1 ) & ( ERKP' = ERKP + 1 ) & ( Phase3' = Phase3 + 1 );


[ r30 ] ( ERKP_Phase3 > 0 ) & ( ERK < n ) & ( Phase3 < n )
          -> 0.1 * ERKP_Phase3 :
        ( ERKP_Phase3' = ERKP_Phase3 - 1 ) & ( ERK' = ERK + 1 ) & ( Phase3' = Phase3 + 1 );


endmodule
  

rewards

  true : RafP * ( 0.1 / k );

endrewards