model.prism (0.01 MB) property.props (0.01 MB) model.jani (0.13 MB)
Taken from QVBS (January 2026). The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020. Original Prism model and property files have been adapted for compatibility and simplicity: - Constants: All open constants are now explicitly set within model.prism (no need to set them via command line) - Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property. - Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.
// MAPK cascade // taken from: C.-Y. Huang and J. Ferrell // Ultrasensitivity in the mitgen-activated protein kinase cascade // Proc. Natl. Acad. Sci. 93:10078-13100, 1996 // gxn/dxp 19/12/07 ctmc const double T =30; // constants (number of elements of each species) const int E1=1; // initial amount of E1 const int E2=1; // initial amount of E2 const int M=1; // initial amount of MAPK phosphatase and MAPKK phosphatase const int N=4; // initial amount of MAPK/MAPKK and MAPKKK // reaction rates (suppose volume proportional to the number of elements of MAPK) const double a1=1/N; const double d1=150; const double k1=150; const double a2=1/N; const double d2=150; const double k2=150; const double a3=1/N; const double d3=150; const double k3=150; const double a4=1/N; const double d4=150; const double k4=150; const double a5=1/N; const double d5=150; const double k5=150; const double a6=1/N; const double d6=150; const double k6=150; const double a7=1/N; const double d7=150; const double k7=150; const double a8=1/N; const double d8=150; const double k8=150; const double a9=1/N; const double d9=150; const double k9=150; const double a10=1/N; const double d10=150; const double k10=150; //------------------------------------------------------------------------------ // enzymes module E1 e1 : [0..E1] init E1; // amount of enzyme E1 // reaction 1 (MAPKKK is activated by E1) [a_kkk_e1] e1>0 -> e1 : (e1'=e1-1); [d_kkk_e1] e11 : (e1'=e1+1); [k_kkk_e1] e1 1 : (e1'=e1+1); endmodule // construct E2 by renaming E1 module E2 = E1[ e1=e2, E1=E2, a_kkk_e1=a_kkk_e2, d_kkk_e1=d_kkk_e2, k_kkk_e1=k_kkk_e2 ] endmodule //------------------------------------------------------------------------------ // phosphatases // mapk phosphatases module KPTASE kptase : [0..M] init M; // amount of MAPK Phosphatase // reactions 8 and 10 (MAPK/MAPK-P is deactivated by MAPK Phosphatase) [a_k_ptase] kptase>0 -> kptase : (kptase'=kptase-1); [d_k_ptase] kptase 1 : (kptase'=kptase+1); [k_k_ptase] kptase 1 : (kptase'=kptase+1); endmodule // construct mapkk phosphatases by renaming module for mapk phosphatases module KKPTASE = KPTASE[ kptase= kkptase, a_k_ptase=a_kk_ptase, d_k_ptase=d_kk_ptase, k_k_ptase=k_kk_ptase ] endmodule //------------------------------------------------------------------------------ // mapks // mapk module MAPK k : [0..N] init N; // quantity of MAPK k_kkpp : [0..N] init 0; // quantity of MAPK:MAPKK-PP kp : [0..N] init 0; // quantity of MAPK-P kp_kkpp : [0..N] init 0; // quantity of MAPK-P:MAPKK-PP kp_ptase : [0..N] init 0; // quantity of MAPK-P:MAPK Phosphatase kpp : [0..N] init 0; // quantity of MAPK-PP kpp_ptase : [0..N] init 0; // quantity of MAPK-PP:MAPK Phosphatase // reaction 7 (MAPK is activated by MAPKK-PP) [a_k_kk] k>0 & k_kkpp a7*k : (k_kkpp'=k_kkpp+1) & (k'=k-1); [d_k_kk] k 0 -> d7*k_kkpp : (k_kkpp'=k_kkpp-1) & (k'=k+1); [k_k_kk] k_kkpp>0 & kp k7*k_kkpp : (k_kkpp'=k_kkpp-1) & (kp'=kp+1); // reaction 8 (MAPK-P is deactivated by MAPK Phosphatase) [a_k_ptase] kp>0 & kp_ptase a8*kp : (kp_ptase'=kp_ptase+1) & (kp'=kp-1); [d_k_ptase] kp 0 -> d8*kp_ptase : (kp_ptase'=kp_ptase-1) & (kp'=kp+1); [k_k_ptase] kp_ptase>0 & k k8*kp_ptase : (kp_ptase'=kp_ptase-1) & (k'=k+1); // reaction 9 (MAPK-P is activated by MAPKK-PP) [a_k_kk] kp>0 & kp_kkpp a9*kp : (kp_kkpp'=kp_kkpp+1) & (kp'=kp-1); [d_k_kk] kp 0 -> d9*kp_kkpp : (kp_kkpp'=kp_kkpp-1) & (kp'=kp+1); [k_k_kk] kp_kkpp>0 & kpp k9*kp_kkpp : (kp_kkpp'=kp_kkpp-1) & (kpp'=kpp+1); // reaction 10 (MAPK-P is deactivated by MAPK Phosphatase) [a_k_ptase] kpp>0 & kpp_ptase a10*kpp : (kpp_ptase'=kpp_ptase+1) & (kpp'=kpp-1); [d_k_ptase] kpp 0 -> d10*kpp_ptase : (kpp_ptase'=kpp_ptase-1) & (kpp'=kpp+1); [k_k_ptase] kpp_ptase>0 & kp k10*kpp_ptase : (kpp_ptase'=kpp_ptase-1) & (kp'=kp+1); endmodule // mapkk module MAPKK kk : [0..N] init N; // quantity of MAPKK kk_kkkp : [0..N] init 0; // quantity of MAPKK:MAPKKK-P kkp : [0..N] init 0; // quantity of MAPKK-P kkp_kkkp : [0..N] init 0; // quantity of MAPKK-P:MAPKKK-P kkp_ptase : [0..N] init 0; // quantity of MAPKK-P:MAPKK Phosphatase kkpp : [0..N] init 0; // quantity of MAPKK-PP kkpp_ptase : [0..N] init 0; // quantity of MAPKK-PP:MAPKK Phosphatase // reaction 3 (MAPKK is activated by MAPKKK*) [a_kk_kkk] kk>0 & kk_kkkp a3*kk : (kk_kkkp'=kk_kkkp+1) & (kk'=kk-1); [d_kk_kkk] kk 0 -> d3*kk_kkkp : (kk_kkkp'=kk_kkkp-1) & (kk'=kk+1); [k_kk_kkk] kk_kkkp>0 & kkp k3*kk_kkkp : (kk_kkkp'=kk_kkkp-1) & (kkp'=kkp+1); // reaction 4 (MAPKK-P is deactivated by MAPKK Phosphatase) [a_kk_ptase] kkp>0 & kkp_ptase a4*kkp : (kkp_ptase'=kkp_ptase+1) & (kkp'=kkp-1); [d_kk_ptase] kkp 0 -> d4*kkp_ptase : (kkp_ptase'=kkp_ptase-1) & (kkp'=kkp+1); [k_kk_ptase] kkp_ptase>0 & kk k4*kkp_ptase : (kkp_ptase'=kkp_ptase-1) & (kk'=kk+1); // reaction 5 (MAPKK-P is activated by MAPKKK*) [a_kk_kkk] kkp>0 & kkp_kkkp a5*kkp : (kkp_kkkp'=kkp_kkkp+1) & (kkp'=kkp-1); [d_kk_kkk] kkp 0 -> d5*kkp_kkkp : (kkp_kkkp'=kkp_kkkp-1) & (kkp'=kkp+1); [k_kk_kkk] kkp_kkkp>0 & kkpp k5*kkp_kkkp : (kkp_kkkp'=kkp_kkkp-1) & (kkpp'=kkpp+1); // reaction 6 (MAPKK-P is deactivated by MAPKK Phosphatase) [a_kk_ptase] kkpp>0 & kkpp_ptase a6*kkpp : (kkpp_ptase'=kkpp_ptase+1) & (kkpp'=kkpp-1); [d_kk_ptase] kkpp 0 -> d6*kkpp_ptase : (kkpp_ptase'=kkpp_ptase-1) & (kkpp'=kkpp+1); [k_kk_ptase] kkpp_ptase>0 & kkp k6*kkpp_ptase : (kkpp_ptase'=kkpp_ptase-1) & (kkp'=kkp+1); // reactions 7 and 9 (MAPK/MAPK-P is activated by MAPKPP) [a_k_kk] kkpp>0 -> kkpp : (kkpp'=kkpp-1); [d_k_kk] kkpp 1 : (kkpp'=kkpp+1); [k_k_kk] kkpp 1 : (kkpp'=kkpp+1); endmodule // mapkkk module MAPKKK kkk : [0..N] init N; // quantity of MAPKKK kkk_e1 : [0..N] init 0; // quantity of MAPKKK:E1 kkkp : [0..N] init 0; // quantity of MAPKKK* kkkp_e2 : [0..N] init 0; // quantity of MAPKKK*:E2 // reaction 1 (MAPKKK is activated by E1) [a_kkk_e1] kkk>0 & kkk_e1 a1*kkk : (kkk_e1'=kkk_e1+1) & (kkk'=kkk-1); [d_kkk_e1] kkk 0 -> d1*kkk_e1 : (kkk_e1'=kkk_e1-1) & (kkk'=kkk+1); [k_kkk_e1] kkk_e1>0 & kkkp k1*kkk_e1 : (kkk_e1'=kkk_e1-1) & (kkkp'=kkkp+1); // reaction 2 (MAPKKK* is deactivated by E2) [a_kkk_e2] kkkp>0 & kkkp_e2 a2*kkkp : (kkkp_e2'=kkkp_e2+1) & (kkkp'=kkkp-1); [d_kkk_e2] kkkp 0 -> d2*kkkp_e2 : (kkkp_e2'=kkkp_e2-1) & (kkkp'=kkkp+1); [k_kkk_e2] kkkp_e2>0 & kkk k2*kkkp_e2 : (kkkp_e2'=kkkp_e2-1) & (kkk'=kkk+1); // reactions 3 and 5 (MAPKK/MAPKK-P is activated by MAPKKP) [a_kk_kkk] kkkp>0 -> kkkp : (kkkp'=kkkp-1); [d_kk_kkk] kkkp 1 : (kkkp'=kkkp+1); [k_kk_kkk] kkkp 1 : (kkkp'=kkkp+1); endmodule //------------------------------------------------------------------------------ // reward structures rewards "time" // time true : 1; endrewards label "target" = kpp=N;
//the expected number of reactions between MAPK and MAKK by time T
"activated_time": R{"time"}=? [ F "target" ];
{
"actions": [
{
"name": "a_k_kk"
},
{
"name": "a_k_ptase"
},
{
"name": "a_kk_kkk"
},
{
"name": "a_kk_ptase"
},
{
"name": "a_kkk_e1"
},
{
"name": "a_kkk_e2"
},
{
"name": "d_k_kk"
},
{
"name": "d_k_ptase"
},
{
"name": "d_kk_kkk"
},
{
"name": "d_kk_ptase"
},
{
"name": "d_kkk_e1"
},
{
"name": "d_kkk_e2"
},
{
"name": "k_k_kk"
},
{
"name": "k_k_ptase"
},
{
"name": "k_kk_kkk"
},
{
"name": "k_kk_ptase"
},
{
"name": "k_kkk_e1"
},
{
"name": "k_kkk_e2"
}
],
"automata": [
{
"edges": [
{
"action": "a_kkk_e1",
"destinations": [
{
"assignments": [
{
"comment": "e1 <- (e1 - 1)",
"ref": "e1",
"value": {
"left": "e1",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(e1 / e1)",
"exp": {
"left": "e1",
"op": "/",
"right": "e1"
}
}
}
],
"guard": {
"comment": "(e1 > 0)",
"exp": {
"left": "e1",
"op": ">",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "e1",
"exp": "e1"
}
},
{
"action": "d_kkk_e1",
"destinations": [
{
"assignments": [
{
"comment": "e1 <- (e1 + 1)",
"ref": "e1",
"value": {
"left": "e1",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(e1 < 1)",
"exp": {
"left": "e1",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "k_kkk_e1",
"destinations": [
{
"assignments": [
{
"comment": "e1 <- (e1 + 1)",
"ref": "e1",
"value": {
"left": "e1",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(e1 < 1)",
"exp": {
"left": "e1",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l",
"transient-values": [
{
"comment": "target <- (kpp = 4)",
"ref": "target",
"value": {
"left": "kpp",
"op": "=",
"right": 4
}
},
{
"comment": "time <- 1",
"ref": "time",
"value": 1
}
]
}
],
"name": "E1",
"variables": [
{
"initial-value": 1,
"name": "e1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"action": "a_kkk_e2",
"destinations": [
{
"assignments": [
{
"comment": "e2 <- (e2 - 1)",
"ref": "e2",
"value": {
"left": "e2",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(e2 / e2)",
"exp": {
"left": "e2",
"op": "/",
"right": "e2"
}
}
}
],
"guard": {
"comment": "(e2 > 0)",
"exp": {
"left": "e2",
"op": ">",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "e2",
"exp": "e2"
}
},
{
"action": "d_kkk_e2",
"destinations": [
{
"assignments": [
{
"comment": "e2 <- (e2 + 1)",
"ref": "e2",
"value": {
"left": "e2",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(e2 < 1)",
"exp": {
"left": "e2",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "k_kkk_e2",
"destinations": [
{
"assignments": [
{
"comment": "e2 <- (e2 + 1)",
"ref": "e2",
"value": {
"left": "e2",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(e2 < 1)",
"exp": {
"left": "e2",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "E2",
"variables": [
{
"initial-value": 1,
"name": "e2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"action": "a_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kptase <- (kptase - 1)",
"ref": "kptase",
"value": {
"left": "kptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(kptase / kptase)",
"exp": {
"left": "kptase",
"op": "/",
"right": "kptase"
}
}
}
],
"guard": {
"comment": "(kptase > 0)",
"exp": {
"left": "kptase",
"op": ">",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "kptase",
"exp": "kptase"
}
},
{
"action": "d_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kptase <- (kptase + 1)",
"ref": "kptase",
"value": {
"left": "kptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kptase < 1)",
"exp": {
"left": "kptase",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "k_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kptase <- (kptase + 1)",
"ref": "kptase",
"value": {
"left": "kptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kptase < 1)",
"exp": {
"left": "kptase",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "KPTASE",
"variables": [
{
"initial-value": 1,
"name": "kptase",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"action": "a_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkptase <- (kkptase - 1)",
"ref": "kkptase",
"value": {
"left": "kkptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(kkptase / kkptase)",
"exp": {
"left": "kkptase",
"op": "/",
"right": "kkptase"
}
}
}
],
"guard": {
"comment": "(kkptase > 0)",
"exp": {
"left": "kkptase",
"op": ">",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "kkptase",
"exp": "kkptase"
}
},
{
"action": "d_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkptase <- (kkptase + 1)",
"ref": "kkptase",
"value": {
"left": "kkptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kkptase < 1)",
"exp": {
"left": "kkptase",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "k_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkptase <- (kkptase + 1)",
"ref": "kkptase",
"value": {
"left": "kkptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kkptase < 1)",
"exp": {
"left": "kkptase",
"op": "<",
"right": 1
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "KKPTASE",
"variables": [
{
"initial-value": 1,
"name": "kkptase",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 1
}
}
]
},
{
"edges": [
{
"action": "a_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "k <- (k - 1)",
"ref": "k",
"value": {
"left": "k",
"op": "-",
"right": 1
}
},
{
"comment": "k_kkpp <- (k_kkpp + 1)",
"ref": "k_kkpp",
"value": {
"left": "k_kkpp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * k) / ((1 / 4) * k))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "k"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "k"
}
}
}
}
],
"guard": {
"comment": "((k > 0) & (k_kkpp < 4))",
"exp": {
"left": {
"left": "k",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "k_kkpp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * k)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "k"
}
}
},
{
"action": "a_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "kp <- (kp - 1)",
"ref": "kp",
"value": {
"left": "kp",
"op": "-",
"right": 1
}
},
{
"comment": "kp_kkpp <- (kp_kkpp + 1)",
"ref": "kp_kkpp",
"value": {
"left": "kp_kkpp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kp) / ((1 / 4) * kp))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kp"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kp"
}
}
}
}
],
"guard": {
"comment": "((kp > 0) & (kp_kkpp < 4))",
"exp": {
"left": {
"left": "kp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kp_kkpp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kp)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kp"
}
}
},
{
"action": "a_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kp <- (kp - 1)",
"ref": "kp",
"value": {
"left": "kp",
"op": "-",
"right": 1
}
},
{
"comment": "kp_ptase <- (kp_ptase + 1)",
"ref": "kp_ptase",
"value": {
"left": "kp_ptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kp) / ((1 / 4) * kp))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kp"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kp"
}
}
}
}
],
"guard": {
"comment": "((kp > 0) & (kp_ptase < 4))",
"exp": {
"left": {
"left": "kp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kp_ptase",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kp)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kp"
}
}
},
{
"action": "a_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kpp <- (kpp - 1)",
"ref": "kpp",
"value": {
"left": "kpp",
"op": "-",
"right": 1
}
},
{
"comment": "kpp_ptase <- (kpp_ptase + 1)",
"ref": "kpp_ptase",
"value": {
"left": "kpp_ptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kpp) / ((1 / 4) * kpp))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kpp"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kpp"
}
}
}
}
],
"guard": {
"comment": "((kpp > 0) & (kpp_ptase < 4))",
"exp": {
"left": {
"left": "kpp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kpp_ptase",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kpp)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kpp"
}
}
},
{
"action": "d_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "k <- (k + 1)",
"ref": "k",
"value": {
"left": "k",
"op": "+",
"right": 1
}
},
{
"comment": "k_kkpp <- (k_kkpp - 1)",
"ref": "k_kkpp",
"value": {
"left": "k_kkpp",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * k_kkpp) / (150 * k_kkpp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "k_kkpp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "k_kkpp"
}
}
}
}
],
"guard": {
"comment": "((k < 4) & (k_kkpp > 0))",
"exp": {
"left": {
"left": "k",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "k_kkpp",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * k_kkpp)",
"exp": {
"left": 150,
"op": "*",
"right": "k_kkpp"
}
}
},
{
"action": "d_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "kp <- (kp + 1)",
"ref": "kp",
"value": {
"left": "kp",
"op": "+",
"right": 1
}
},
{
"comment": "kp_kkpp <- (kp_kkpp - 1)",
"ref": "kp_kkpp",
"value": {
"left": "kp_kkpp",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kp_kkpp) / (150 * kp_kkpp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kp_kkpp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kp_kkpp"
}
}
}
}
],
"guard": {
"comment": "((kp < 4) & (kp_kkpp > 0))",
"exp": {
"left": {
"left": "kp",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kp_kkpp",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kp_kkpp)",
"exp": {
"left": 150,
"op": "*",
"right": "kp_kkpp"
}
}
},
{
"action": "d_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kp <- (kp + 1)",
"ref": "kp",
"value": {
"left": "kp",
"op": "+",
"right": 1
}
},
{
"comment": "kp_ptase <- (kp_ptase - 1)",
"ref": "kp_ptase",
"value": {
"left": "kp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kp_ptase) / (150 * kp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kp < 4) & (kp_ptase > 0))",
"exp": {
"left": {
"left": "kp",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kp_ptase",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kp_ptase"
}
}
},
{
"action": "d_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kpp <- (kpp + 1)",
"ref": "kpp",
"value": {
"left": "kpp",
"op": "+",
"right": 1
}
},
{
"comment": "kpp_ptase <- (kpp_ptase - 1)",
"ref": "kpp_ptase",
"value": {
"left": "kpp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kpp_ptase) / (150 * kpp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kpp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kpp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kpp < 4) & (kpp_ptase > 0))",
"exp": {
"left": {
"left": "kpp",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kpp_ptase",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kpp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kpp_ptase"
}
}
},
{
"action": "k_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "k_kkpp <- (k_kkpp - 1)",
"ref": "k_kkpp",
"value": {
"left": "k_kkpp",
"op": "-",
"right": 1
}
},
{
"comment": "kp <- (kp + 1)",
"ref": "kp",
"value": {
"left": "kp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * k_kkpp) / (150 * k_kkpp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "k_kkpp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "k_kkpp"
}
}
}
}
],
"guard": {
"comment": "((k_kkpp > 0) & (kp < 4))",
"exp": {
"left": {
"left": "k_kkpp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * k_kkpp)",
"exp": {
"left": 150,
"op": "*",
"right": "k_kkpp"
}
}
},
{
"action": "k_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "kp_kkpp <- (kp_kkpp - 1)",
"ref": "kp_kkpp",
"value": {
"left": "kp_kkpp",
"op": "-",
"right": 1
}
},
{
"comment": "kpp <- (kpp + 1)",
"ref": "kpp",
"value": {
"left": "kpp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kp_kkpp) / (150 * kp_kkpp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kp_kkpp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kp_kkpp"
}
}
}
}
],
"guard": {
"comment": "((kp_kkpp > 0) & (kpp < 4))",
"exp": {
"left": {
"left": "kp_kkpp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kpp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kp_kkpp)",
"exp": {
"left": 150,
"op": "*",
"right": "kp_kkpp"
}
}
},
{
"action": "k_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "k <- (k + 1)",
"ref": "k",
"value": {
"left": "k",
"op": "+",
"right": 1
}
},
{
"comment": "kp_ptase <- (kp_ptase - 1)",
"ref": "kp_ptase",
"value": {
"left": "kp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kp_ptase) / (150 * kp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kp_ptase > 0) & (k < 4))",
"exp": {
"left": {
"left": "kp_ptase",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "k",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kp_ptase"
}
}
},
{
"action": "k_k_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kp <- (kp + 1)",
"ref": "kp",
"value": {
"left": "kp",
"op": "+",
"right": 1
}
},
{
"comment": "kpp_ptase <- (kpp_ptase - 1)",
"ref": "kpp_ptase",
"value": {
"left": "kpp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kpp_ptase) / (150 * kpp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kpp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kpp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kpp_ptase > 0) & (kp < 4))",
"exp": {
"left": {
"left": "kpp_ptase",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kpp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kpp_ptase"
}
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "MAPK",
"variables": [
{
"initial-value": 4,
"name": "k",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "k_kkpp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kp_kkpp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kp_ptase",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kpp_ptase",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
}
]
},
{
"edges": [
{
"action": "a_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "kkpp <- (kkpp - 1)",
"ref": "kkpp",
"value": {
"left": "kkpp",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(kkpp / kkpp)",
"exp": {
"left": "kkpp",
"op": "/",
"right": "kkpp"
}
}
}
],
"guard": {
"comment": "(kkpp > 0)",
"exp": {
"left": "kkpp",
"op": ">",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "kkpp",
"exp": "kkpp"
}
},
{
"action": "a_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kk <- (kk - 1)",
"ref": "kk",
"value": {
"left": "kk",
"op": "-",
"right": 1
}
},
{
"comment": "kk_kkkp <- (kk_kkkp + 1)",
"ref": "kk_kkkp",
"value": {
"left": "kk_kkkp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kk) / ((1 / 4) * kk))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kk"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kk"
}
}
}
}
],
"guard": {
"comment": "((kk > 0) & (kk_kkkp < 4))",
"exp": {
"left": {
"left": "kk",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kk_kkkp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kk)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kk"
}
}
},
{
"action": "a_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kkp <- (kkp - 1)",
"ref": "kkp",
"value": {
"left": "kkp",
"op": "-",
"right": 1
}
},
{
"comment": "kkp_kkkp <- (kkp_kkkp + 1)",
"ref": "kkp_kkkp",
"value": {
"left": "kkp_kkkp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kkp) / ((1 / 4) * kkp))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkp"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkp"
}
}
}
}
],
"guard": {
"comment": "((kkp > 0) & (kkp_kkkp < 4))",
"exp": {
"left": {
"left": "kkp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkp_kkkp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kkp)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkp"
}
}
},
{
"action": "a_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkp <- (kkp - 1)",
"ref": "kkp",
"value": {
"left": "kkp",
"op": "-",
"right": 1
}
},
{
"comment": "kkp_ptase <- (kkp_ptase + 1)",
"ref": "kkp_ptase",
"value": {
"left": "kkp_ptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kkp) / ((1 / 4) * kkp))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkp"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkp"
}
}
}
}
],
"guard": {
"comment": "((kkp > 0) & (kkp_ptase < 4))",
"exp": {
"left": {
"left": "kkp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkp_ptase",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kkp)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkp"
}
}
},
{
"action": "a_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkpp <- (kkpp - 1)",
"ref": "kkpp",
"value": {
"left": "kkpp",
"op": "-",
"right": 1
}
},
{
"comment": "kkpp_ptase <- (kkpp_ptase + 1)",
"ref": "kkpp_ptase",
"value": {
"left": "kkpp_ptase",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kkpp) / ((1 / 4) * kkpp))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkpp"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkpp"
}
}
}
}
],
"guard": {
"comment": "((kkpp > 0) & (kkpp_ptase < 4))",
"exp": {
"left": {
"left": "kkpp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkpp_ptase",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kkpp)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkpp"
}
}
},
{
"action": "d_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "kkpp <- (kkpp + 1)",
"ref": "kkpp",
"value": {
"left": "kkpp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kkpp < 4)",
"exp": {
"left": "kkpp",
"op": "<",
"right": 4
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "d_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kk <- (kk + 1)",
"ref": "kk",
"value": {
"left": "kk",
"op": "+",
"right": 1
}
},
{
"comment": "kk_kkkp <- (kk_kkkp - 1)",
"ref": "kk_kkkp",
"value": {
"left": "kk_kkkp",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kk_kkkp) / (150 * kk_kkkp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kk_kkkp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kk_kkkp"
}
}
}
}
],
"guard": {
"comment": "((kk < 4) & (kk_kkkp > 0))",
"exp": {
"left": {
"left": "kk",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kk_kkkp",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kk_kkkp)",
"exp": {
"left": 150,
"op": "*",
"right": "kk_kkkp"
}
}
},
{
"action": "d_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kkp <- (kkp + 1)",
"ref": "kkp",
"value": {
"left": "kkp",
"op": "+",
"right": 1
}
},
{
"comment": "kkp_kkkp <- (kkp_kkkp - 1)",
"ref": "kkp_kkkp",
"value": {
"left": "kkp_kkkp",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkp_kkkp) / (150 * kkp_kkkp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkp_kkkp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkp_kkkp"
}
}
}
}
],
"guard": {
"comment": "((kkp < 4) & (kkp_kkkp > 0))",
"exp": {
"left": {
"left": "kkp",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kkp_kkkp",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkp_kkkp)",
"exp": {
"left": 150,
"op": "*",
"right": "kkp_kkkp"
}
}
},
{
"action": "d_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkp <- (kkp + 1)",
"ref": "kkp",
"value": {
"left": "kkp",
"op": "+",
"right": 1
}
},
{
"comment": "kkp_ptase <- (kkp_ptase - 1)",
"ref": "kkp_ptase",
"value": {
"left": "kkp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkp_ptase) / (150 * kkp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kkp < 4) & (kkp_ptase > 0))",
"exp": {
"left": {
"left": "kkp",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kkp_ptase",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kkp_ptase"
}
}
},
{
"action": "d_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkpp <- (kkpp + 1)",
"ref": "kkpp",
"value": {
"left": "kkpp",
"op": "+",
"right": 1
}
},
{
"comment": "kkpp_ptase <- (kkpp_ptase - 1)",
"ref": "kkpp_ptase",
"value": {
"left": "kkpp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkpp_ptase) / (150 * kkpp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkpp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkpp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kkpp < 4) & (kkpp_ptase > 0))",
"exp": {
"left": {
"left": "kkpp",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kkpp_ptase",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkpp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kkpp_ptase"
}
}
},
{
"action": "k_k_kk",
"destinations": [
{
"assignments": [
{
"comment": "kkpp <- (kkpp + 1)",
"ref": "kkpp",
"value": {
"left": "kkpp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kkpp < 4)",
"exp": {
"left": "kkpp",
"op": "<",
"right": 4
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "k_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kk_kkkp <- (kk_kkkp - 1)",
"ref": "kk_kkkp",
"value": {
"left": "kk_kkkp",
"op": "-",
"right": 1
}
},
{
"comment": "kkp <- (kkp + 1)",
"ref": "kkp",
"value": {
"left": "kkp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kk_kkkp) / (150 * kk_kkkp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kk_kkkp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kk_kkkp"
}
}
}
}
],
"guard": {
"comment": "((kk_kkkp > 0) & (kkp < 4))",
"exp": {
"left": {
"left": "kk_kkkp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kk_kkkp)",
"exp": {
"left": 150,
"op": "*",
"right": "kk_kkkp"
}
}
},
{
"action": "k_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kkp_kkkp <- (kkp_kkkp - 1)",
"ref": "kkp_kkkp",
"value": {
"left": "kkp_kkkp",
"op": "-",
"right": 1
}
},
{
"comment": "kkpp <- (kkpp + 1)",
"ref": "kkpp",
"value": {
"left": "kkpp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkp_kkkp) / (150 * kkp_kkkp))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkp_kkkp"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkp_kkkp"
}
}
}
}
],
"guard": {
"comment": "((kkp_kkkp > 0) & (kkpp < 4))",
"exp": {
"left": {
"left": "kkp_kkkp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkpp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkp_kkkp)",
"exp": {
"left": 150,
"op": "*",
"right": "kkp_kkkp"
}
}
},
{
"action": "k_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kk <- (kk + 1)",
"ref": "kk",
"value": {
"left": "kk",
"op": "+",
"right": 1
}
},
{
"comment": "kkp_ptase <- (kkp_ptase - 1)",
"ref": "kkp_ptase",
"value": {
"left": "kkp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkp_ptase) / (150 * kkp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kkp_ptase > 0) & (kk < 4))",
"exp": {
"left": {
"left": "kkp_ptase",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kk",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kkp_ptase"
}
}
},
{
"action": "k_kk_ptase",
"destinations": [
{
"assignments": [
{
"comment": "kkp <- (kkp + 1)",
"ref": "kkp",
"value": {
"left": "kkp",
"op": "+",
"right": 1
}
},
{
"comment": "kkpp_ptase <- (kkpp_ptase - 1)",
"ref": "kkpp_ptase",
"value": {
"left": "kkpp_ptase",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkpp_ptase) / (150 * kkpp_ptase))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkpp_ptase"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkpp_ptase"
}
}
}
}
],
"guard": {
"comment": "((kkpp_ptase > 0) & (kkp < 4))",
"exp": {
"left": {
"left": "kkpp_ptase",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkpp_ptase)",
"exp": {
"left": 150,
"op": "*",
"right": "kkpp_ptase"
}
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "MAPKK",
"variables": [
{
"initial-value": 4,
"name": "kk",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kk_kkkp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkp_kkkp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkp_ptase",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkpp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkpp_ptase",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
}
]
},
{
"edges": [
{
"action": "a_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kkkp <- (kkkp - 1)",
"ref": "kkkp",
"value": {
"left": "kkkp",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(kkkp / kkkp)",
"exp": {
"left": "kkkp",
"op": "/",
"right": "kkkp"
}
}
}
],
"guard": {
"comment": "(kkkp > 0)",
"exp": {
"left": "kkkp",
"op": ">",
"right": 0
}
},
"location": "l",
"rate": {
"comment": "kkkp",
"exp": "kkkp"
}
},
{
"action": "a_kkk_e1",
"destinations": [
{
"assignments": [
{
"comment": "kkk <- (kkk - 1)",
"ref": "kkk",
"value": {
"left": "kkk",
"op": "-",
"right": 1
}
},
{
"comment": "kkk_e1 <- (kkk_e1 + 1)",
"ref": "kkk_e1",
"value": {
"left": "kkk_e1",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kkk) / ((1 / 4) * kkk))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkk"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkk"
}
}
}
}
],
"guard": {
"comment": "((kkk > 0) & (kkk_e1 < 4))",
"exp": {
"left": {
"left": "kkk",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkk_e1",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kkk)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkk"
}
}
},
{
"action": "a_kkk_e2",
"destinations": [
{
"assignments": [
{
"comment": "kkkp <- (kkkp - 1)",
"ref": "kkkp",
"value": {
"left": "kkkp",
"op": "-",
"right": 1
}
},
{
"comment": "kkkp_e2 <- (kkkp_e2 + 1)",
"ref": "kkkp_e2",
"value": {
"left": "kkkp_e2",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(((1 / 4) * kkkp) / ((1 / 4) * kkkp))",
"exp": {
"left": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkkp"
},
"op": "/",
"right": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkkp"
}
}
}
}
],
"guard": {
"comment": "((kkkp > 0) & (kkkp_e2 < 4))",
"exp": {
"left": {
"left": "kkkp",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkkp_e2",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "((1 / 4) * kkkp)",
"exp": {
"left": {
"left": 1,
"op": "/",
"right": 4
},
"op": "*",
"right": "kkkp"
}
}
},
{
"action": "d_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kkkp <- (kkkp + 1)",
"ref": "kkkp",
"value": {
"left": "kkkp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kkkp < 4)",
"exp": {
"left": "kkkp",
"op": "<",
"right": 4
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "d_kkk_e1",
"destinations": [
{
"assignments": [
{
"comment": "kkk <- (kkk + 1)",
"ref": "kkk",
"value": {
"left": "kkk",
"op": "+",
"right": 1
}
},
{
"comment": "kkk_e1 <- (kkk_e1 - 1)",
"ref": "kkk_e1",
"value": {
"left": "kkk_e1",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkk_e1) / (150 * kkk_e1))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkk_e1"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkk_e1"
}
}
}
}
],
"guard": {
"comment": "((kkk < 4) & (kkk_e1 > 0))",
"exp": {
"left": {
"left": "kkk",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kkk_e1",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkk_e1)",
"exp": {
"left": 150,
"op": "*",
"right": "kkk_e1"
}
}
},
{
"action": "d_kkk_e2",
"destinations": [
{
"assignments": [
{
"comment": "kkkp <- (kkkp + 1)",
"ref": "kkkp",
"value": {
"left": "kkkp",
"op": "+",
"right": 1
}
},
{
"comment": "kkkp_e2 <- (kkkp_e2 - 1)",
"ref": "kkkp_e2",
"value": {
"left": "kkkp_e2",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkkp_e2) / (150 * kkkp_e2))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkkp_e2"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkkp_e2"
}
}
}
}
],
"guard": {
"comment": "((kkkp < 4) & (kkkp_e2 > 0))",
"exp": {
"left": {
"left": "kkkp",
"op": "<",
"right": 4
},
"op": "∧",
"right": {
"left": "kkkp_e2",
"op": ">",
"right": 0
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkkp_e2)",
"exp": {
"left": 150,
"op": "*",
"right": "kkkp_e2"
}
}
},
{
"action": "k_kk_kkk",
"destinations": [
{
"assignments": [
{
"comment": "kkkp <- (kkkp + 1)",
"ref": "kkkp",
"value": {
"left": "kkkp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "(1 / 1)",
"exp": 1
}
}
],
"guard": {
"comment": "(kkkp < 4)",
"exp": {
"left": "kkkp",
"op": "<",
"right": 4
}
},
"location": "l",
"rate": {
"comment": "1",
"exp": 1
}
},
{
"action": "k_kkk_e1",
"destinations": [
{
"assignments": [
{
"comment": "kkk_e1 <- (kkk_e1 - 1)",
"ref": "kkk_e1",
"value": {
"left": "kkk_e1",
"op": "-",
"right": 1
}
},
{
"comment": "kkkp <- (kkkp + 1)",
"ref": "kkkp",
"value": {
"left": "kkkp",
"op": "+",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkk_e1) / (150 * kkk_e1))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkk_e1"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkk_e1"
}
}
}
}
],
"guard": {
"comment": "((kkk_e1 > 0) & (kkkp < 4))",
"exp": {
"left": {
"left": "kkk_e1",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkkp",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkk_e1)",
"exp": {
"left": 150,
"op": "*",
"right": "kkk_e1"
}
}
},
{
"action": "k_kkk_e2",
"destinations": [
{
"assignments": [
{
"comment": "kkk <- (kkk + 1)",
"ref": "kkk",
"value": {
"left": "kkk",
"op": "+",
"right": 1
}
},
{
"comment": "kkkp_e2 <- (kkkp_e2 - 1)",
"ref": "kkkp_e2",
"value": {
"left": "kkkp_e2",
"op": "-",
"right": 1
}
}
],
"location": "l",
"probability": {
"comment": "((150 * kkkp_e2) / (150 * kkkp_e2))",
"exp": {
"left": {
"left": 150,
"op": "*",
"right": "kkkp_e2"
},
"op": "/",
"right": {
"left": 150,
"op": "*",
"right": "kkkp_e2"
}
}
}
}
],
"guard": {
"comment": "((kkkp_e2 > 0) & (kkk < 4))",
"exp": {
"left": {
"left": "kkkp_e2",
"op": ">",
"right": 0
},
"op": "∧",
"right": {
"left": "kkk",
"op": "<",
"right": 4
}
}
},
"location": "l",
"rate": {
"comment": "(150 * kkkp_e2)",
"exp": {
"left": 150,
"op": "*",
"right": "kkkp_e2"
}
}
}
],
"initial-locations": [
"l"
],
"locations": [
{
"name": "l"
}
],
"name": "MAPKKK",
"variables": [
{
"initial-value": 4,
"name": "kkk",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkk_e1",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkkp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
},
{
"initial-value": 0,
"name": "kkkp_e2",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
}
]
}
],
"constants": [
{
"name": "T",
"type": "real",
"value": 30
},
{
"name": "E1",
"type": "int",
"value": 1
},
{
"name": "E2",
"type": "int",
"value": 1
},
{
"name": "M",
"type": "int",
"value": 1
},
{
"name": "N",
"type": "int",
"value": 4
},
{
"name": "a1",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d1",
"type": "real",
"value": 150
},
{
"name": "k1",
"type": "real",
"value": 150
},
{
"name": "a2",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d2",
"type": "real",
"value": 150
},
{
"name": "k2",
"type": "real",
"value": 150
},
{
"name": "a3",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d3",
"type": "real",
"value": 150
},
{
"name": "k3",
"type": "real",
"value": 150
},
{
"name": "a4",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d4",
"type": "real",
"value": 150
},
{
"name": "k4",
"type": "real",
"value": 150
},
{
"name": "a5",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d5",
"type": "real",
"value": 150
},
{
"name": "k5",
"type": "real",
"value": 150
},
{
"name": "a6",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d6",
"type": "real",
"value": 150
},
{
"name": "k6",
"type": "real",
"value": 150
},
{
"name": "a7",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d7",
"type": "real",
"value": 150
},
{
"name": "k7",
"type": "real",
"value": 150
},
{
"name": "a8",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d8",
"type": "real",
"value": 150
},
{
"name": "k8",
"type": "real",
"value": 150
},
{
"name": "a9",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d9",
"type": "real",
"value": 150
},
{
"name": "k9",
"type": "real",
"value": 150
},
{
"name": "a10",
"type": "real",
"value": {
"left": 1,
"op": "/",
"right": 4
}
},
{
"name": "d10",
"type": "real",
"value": 150
},
{
"name": "k10",
"type": "real",
"value": 150
}
],
"features": [
"derived-operators"
],
"jani-version": 1,
"name": "model",
"properties": [
{
"expression": {
"fun": "values",
"op": "filter",
"states": {
"op": "initial"
},
"values": {
"accumulate": [
"time"
],
"exp": "time",
"op": "Emin",
"reach": "target"
}
},
"name": "activated_time"
}
],
"restrict-initial": {
"exp": true
},
"system": {
"elements": [
{
"automaton": "E1"
},
{
"automaton": "E2"
},
{
"automaton": "KPTASE"
},
{
"automaton": "KKPTASE"
},
{
"automaton": "MAPK"
},
{
"automaton": "MAPKK"
},
{
"automaton": "MAPKKK"
}
],
"syncs": [
{
"result": "a_k_kk",
"synchronise": [
null,
null,
null,
null,
"a_k_kk",
"a_k_kk",
null
]
},
{
"result": "a_k_ptase",
"synchronise": [
null,
null,
"a_k_ptase",
null,
"a_k_ptase",
null,
null
]
},
{
"result": "a_kk_kkk",
"synchronise": [
null,
null,
null,
null,
null,
"a_kk_kkk",
"a_kk_kkk"
]
},
{
"result": "a_kk_ptase",
"synchronise": [
null,
null,
null,
"a_kk_ptase",
null,
"a_kk_ptase",
null
]
},
{
"result": "a_kkk_e1",
"synchronise": [
"a_kkk_e1",
null,
null,
null,
null,
null,
"a_kkk_e1"
]
},
{
"result": "a_kkk_e2",
"synchronise": [
null,
"a_kkk_e2",
null,
null,
null,
null,
"a_kkk_e2"
]
},
{
"result": "d_k_kk",
"synchronise": [
null,
null,
null,
null,
"d_k_kk",
"d_k_kk",
null
]
},
{
"result": "d_k_ptase",
"synchronise": [
null,
null,
"d_k_ptase",
null,
"d_k_ptase",
null,
null
]
},
{
"result": "d_kk_kkk",
"synchronise": [
null,
null,
null,
null,
null,
"d_kk_kkk",
"d_kk_kkk"
]
},
{
"result": "d_kk_ptase",
"synchronise": [
null,
null,
null,
"d_kk_ptase",
null,
"d_kk_ptase",
null
]
},
{
"result": "d_kkk_e1",
"synchronise": [
"d_kkk_e1",
null,
null,
null,
null,
null,
"d_kkk_e1"
]
},
{
"result": "d_kkk_e2",
"synchronise": [
null,
"d_kkk_e2",
null,
null,
null,
null,
"d_kkk_e2"
]
},
{
"result": "k_k_kk",
"synchronise": [
null,
null,
null,
null,
"k_k_kk",
"k_k_kk",
null
]
},
{
"result": "k_k_ptase",
"synchronise": [
null,
null,
"k_k_ptase",
null,
"k_k_ptase",
null,
null
]
},
{
"result": "k_kk_kkk",
"synchronise": [
null,
null,
null,
null,
null,
"k_kk_kkk",
"k_kk_kkk"
]
},
{
"result": "k_kk_ptase",
"synchronise": [
null,
null,
null,
"k_kk_ptase",
null,
"k_kk_ptase",
null
]
},
{
"result": "k_kkk_e1",
"synchronise": [
"k_kkk_e1",
null,
null,
null,
null,
null,
"k_kkk_e1"
]
},
{
"result": "k_kkk_e2",
"synchronise": [
null,
"k_kkk_e2",
null,
null,
null,
null,
"k_kkk_e2"
]
}
]
},
"type": "ctmc",
"variables": [
{
"initial-value": false,
"name": "target",
"transient": true,
"type": "bool"
},
{
"initial-value": 0.0,
"name": "time",
"transient": true,
"type": "real"
},
{
"initial-value": 0,
"name": "kpp",
"type": {
"base": "int",
"kind": "bounded",
"lower-bound": 0,
"upper-bound": 4
}
}
]
}