// steady state values, found by trial and error

trace_check(F ([RafP] >0.11 ) ). -> true
trace_check(F ([MEKPP]>0.007) ).  -> true
trace_check(F ([ERKPP]>0.001) ).  -> true

// C0: because we know that the curves are monotonously increasing, 
//     these commands give the steady state values

get_max_from_trace(RafP).  -> 0.11808 at time 201.9
get_max_from_trace(MEKPP). -> 0.00753 at time 201.9
get_max_from_trace(ERKPP). -> 0.00127 at time 2001.9

// I don't know how to ask for the maximal value after a certain time point,  
// therfore I don't get the steady state value for RasGTP by this command
// it's also possible to ask for the minimal value

get_min_from_trace(RasGTP). -> 0.059 at time 5.4 -> i.e. very early
get_min_from_trace(MEKPP).  -> 0 at time 0 -> obvious

// the steady state (because we know the shape of the curves)

trace_check(F( ([RafP]>0.11) & ([MEKPP]>0.007) & ([ERKPP]>0.001) ) ).

//-------------------------------------------------------------

// C1.1: RafP rises to a significant level (above half of its steady state value), 
//     but MEKPP and ERKPP are close to zero;

trace_check(F( ([RafP]>0.06) & ([MEKPP]<0.001)  & ([ERKPP]<0.0002) ) ). -> true
trace_check(F( ([RafP]>0.06) & ([MEKPP]<0.0007) & ([ERKPP]<0.0002) ) ). -> true
trace_check(F( ([RafP]>0.06) & ([MEKPP]<0.0006) & ([ERKPP]<0.0002) ) ). -> false
trace_check(F( ([RafP]>0.07) & ([MEKPP]<0.001)  & ([ERKPP]<0.0002) ) ). -> false


// C1.2 RafP rises to a significant concentration level 
//      (above half of its steady state value),
//      while MEKPP and ERKPP remain close to zero all the time in between;
//      i.e. RafP is really the first species to react 

trace_check((([MEKPP]<0.001)  & ([ERKPP]<0.0002)) U ([RafP]>0.06) ).    -> true
trace_check((([MEKPP]<0.0007) & ([ERKPP]<0.0002)) U ([RafP]>0.06) ).    -> true


//-------------------------------------------------------------

// C2.1: RafP and MEKPP are active (above half of their steady state values), 
//       but ERKPP is still near to zero

F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP<0.0005) ) -> true
F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP<0.0003) ) -> true
F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP<0.0002) ) -> true
F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP<0.0001) ) -> false

F( (RafP>0.06) & (MEKPP>0.005) & (ERKPP<0.001) )  -> true
F( (RafP>0.06) & (MEKPP>0.005) & (ERKPP<0.0005) ) -> true
F( (RafP>0.06) & (MEKPP>0.006) & (ERKPP<0.0005) ) -> false


// C2.2: RafP and MEKPP become active (above half of its steady state values), 
//       while ERKPP remains near to zero all the time in between; 

(ERKPP<0.0002) U ((MEKPP>0.004) & (RafP>0.06))    -> true 


// C2.3: even more precise:
//       if RafP is at a significant concentration level and ERKPP is close to zero, 
//       both species remain in their concentrations
//       until MEKPP gets a significant concentration level (above half of its steady state values);
//       i.e. MEKPP is the second species to react; 

trace_check((([RafP]>0.06) & ([ERKPP]<0.0002)) -> (([RafP]>0.06) & ([ERKPP]<0.0002)) U ([MEKPP]>0.004)).    -> true


//-------------------------------------------------------------

// C3.1: RafP and MEKPP and ERKPP are active 
//       (above half of their steady state values), 

F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP>0.0005) )   -> true

// C3.2: if RafP and MEKPP are at a significant concentration level, 
//       they remain in their concentrations,
//       until ERKPP gets a significant concentration level 
//       (above half of its steady state values);
//       i.e. ERKPP is the third species to react 

trace_check((([RafP]>0.06) & ([MEKPP]>0.004)) -> (([RafP]>0.06) & ([MEKPP]>0.004)) U ([ERKPP]>0.0005)).  -> true


//-------------------------------------------------------------
// pattern for nesting reachability queries, not used
//-------------------------------------------------------------

F( (RafP>0.11) & F (MEKPP>0.007))                 -> true

// F( S1 & F( S2 ))
F( [(RafP>0.06) & (MEKPP<0.001) & (ERKPP<0.0002)] &  -> syntax error ????
   F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP<0.0002) 
    ) 
 )

// should be the same as the previous formula, and the result should be true
F( (RafP>0.06) & (MEKPP<0.001) & (ERKPP<0.0002) & 
   F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP<0.0002) -> false ????
    ) 
 )


// F( S1 & F( S2 & F( S3 ))) -> this formula would confirm the prediction by the qpn
F( (RafP>0.06) & (MEKPP<0.001) & (ERKPP<0.0002) &           -> ???
   F( (RafP>0.06) & (MEKPP>0.004) & (ERKPP<0.0002) &
      F( (RafP>0.11) & (MEKPP>0.007) & (ERKPP>0.001) 
       )
    ) 
 )

// -- the end --