const int K;

// property S1:
// What is the probability of the concentration of RafP increasing,
// when starting in a state where the level is already at K 
// (the latter side condition is specified by the filter given in braces).

P=? [ (RafP=K) U (RafP>K) {RafP=K} ]


// property S2:
// What is the probability that, given the initial concentrations 
// of RafP, MEKPP and ERKPP being zero, 
// the concentration of RafP rises to some level K 
// while the concentrations of MEKPP and ERKPP remain at zero,
// i.e. RafP is the first species to react.

P=? [ ((MEKPP=0) & (ERKPP=0)) U (RafP=K) {(MEKPP=0)&(ERKPP=0)&(RafP=0)} ]