ctmc
formula frs = relocFRS2=0 & degFRS2=0;
formula fgfr = degFGFR=0;
module FGF
FGF : [0..1] init 1;
[fgf_bind] FGF=1 -> (FGF'=0);
[fgf_rel] FGF=0 -> (FGF'=1);
endmodule
module FGFR
FGFR : [0..1] init 1;
degFGFR : [0..1] init 0;
FGFR_FGF : [0..1] init 0;
FGFR_PLC : [0..1] init 0;
Y653P : [0..1] init 0;
Y654P : [0..1] init 0;
Y766P : [0..1] init 0;
[fgf_bind] fgfr & FGFR_FGF=0 -> 5000 : (FGFR_FGF'=1);
[fgf_rel] fgfr & FGFR_FGF=1 -> 0.002 : (FGFR_FGF'=0);
[] fgfr & FGFR_FGF=1 & Y653P=0 -> 0.1 : (Y653P'=1);
[] fgfr & FGFR_FGF=1 & Y654P=0 -> 0.1 : (Y654P'=1);
[] fgfr & Y653P=1 & Y654P=1 & Y766P=0 -> 70 : (Y766P'=1);
[fgfr_bind] fgfr & FGFR=1 -> (FGFR'=0);
[fgfr_rel] fgfr & FGFR=0 -> (FGFR'=1);
[plc_bind] fgfr & Y766P=1 & FGFR_PLC=0 -> 10 : (FGFR_PLC'=1);
[plc_rel] fgfr & FGFR_PLC=1 -> 0.02 : (FGFR_PLC'=0);
[] fgfr & FGFR_PLC=1 -> 1/(60*60) : (degFGFR'=1);
endmodule
module PLC
PLC : [0..1] init 1;
[plc_bind] PLC=1 -> (PLC'=0);
[plc_rel] PLC=0 -> (PLC'=1);
endmodule
module FRS2
relocFRS2 : [0..1] init 0;
degFRS2 : [0..1] init 0;
FRS2_Ubi : [0..1] init 0;
Y196P : [0..1] init 0;
Y306P : [0..1] init 0;
Y471P : [0..1] init 0;
FRS2_FGFR : [0..1] init 0;
FRS2_GRB : [0..2] init 0;
FRS2_SHP : [0..1] init 0;
FRS2_SRC : [0..8] init 0;
[fgfr_bind] frs & FRS2_FGFR=0 -> 10 : (FRS2_FGFR'=1);
[fgfr_rel] frs & FRS2_FGFR=1 -> 0.001 : (FRS2_FGFR'=0);
[] frs & Y653P=1 & Y654P=1 & FRS2_FGFR=1 & Y196P=0 -> 0.2 : (Y196P'=1);
[] frs & Y653P=1 & Y654P=1 & FRS2_FGFR=1 & Y306P=0 -> 0.2 : (Y306P'=1);
[] frs & Y653P=1 & Y654P=1 & FRS2_FGFR=1 & Y471P=0 -> 0.2 : (Y471P'=1);
[] frs & FRS2_SHP=1 & Y196P=1 & FRS2_SRC=0 -> 12 : (Y196P'=0);
[src_rel] frs & FRS2_SHP=1 & Y196P=1 & FRS2_SRC>0 -> 12 : (Y196P'=0) & (FRS2_SRC'=0);
[] frs & FRS2_SHP=1 & Y306P=1 & FRS2_GRB=0 -> 12 : (Y306P'=0);
[grb_rel] frs & FRS2_SHP=1 & Y306P=1 & FRS2_GRB>0 -> 12 : (Y306P'=0) & (FRS2_GRB'=0);
[shp_rel] frs & FRS2_SHP=1 & Y471P=1 -> 12 : (Y471P'=0) & (FRS2_SHP'=0);
[src_bind] frs & Y196P=1 & FRS2_SRC=0 -> 10 : (FRS2_SRC'=SRC);
[src_rel] frs & FRS2_SRC>0 -> 0.02 : (FRS2_SRC'=0);
[grb_bind] frs & Y306P=1 & FRS2_GRB=0 -> 10 : (FRS2_GRB'=GRB);
[grb_rel] frs & FRS2_GRB>0 -> 0.02 : (FRS2_GRB'=0);
[shp_bind] frs & Y471P=1 & FRS2_SHP=0 -> 10 : (FRS2_SHP'=SHP);
[shp_rel] frs & FRS2_SHP=1 -> 0.02 : (FRS2_SHP'=0);
[] frs & FRS2_SRC>0 -> 1/(15*60) : (relocFRS2'=1);
[spry_bind_frs] frs & FRS2_SRC=1 -> 1 : (FRS2_SRC'=SPRY+1);
[spry_rel_frs] frs & FRS2_SRC=2 -> 0.01 : (FRS2_SRC'=1);
[spry_rel_frs] frs & FRS2_SRC>2 -> 0.0001 : (FRS2_SRC'=1);
[] frs & FRS2_SRC=2 -> 10 : (FRS2_SRC'=3);
[cbl_bind_frs] frs & (FRS2_SRC=3|FRS2_SRC=5|FRS2_SRC=7)-> 1 : (FRS2_SRC'=FRS2_SRC+1);
[cbl_rel_frs] frs & (FRS2_SRC=4|FRS2_SRC=6|FRS2_SRC=8)-> 0.0001 : (FRS2_SRC'=FRS2_SRC-1);
[grb_bind_frs] frs & (FRS2_SRC=3|FRS2_SRC=4)-> 1 : (FRS2_SRC'=FRS2_SRC+2*GRB);
[grb_rel_frs] frs & (FRS2_SRC=5|FRS2_SRC=6)-> 0.0001 : (FRS2_SRC'=FRS2_SRC-2);
[grb_rel_frs] frs & (FRS2_SRC=7|FRS2_SRC=8)-> 0.0001 : (FRS2_SRC'=FRS2_SRC-4);
[] frs & (FRS2_SRC=4|FRS2_SRC=6|FRS2_SRC=8)& FRS2_Ubi=0 -> 0.00085 : (FRS2_Ubi'=1);
[] frs & FRS2_Ubi=1 -> 1/(5*60) : (degFRS2'=1);
[spry_dephos] frs & FRS2_SHP=1 & FRS2_SRC>2 -> 12 : (FRS2_SRC'=2);
[sos_bind_frs] frs & FRS2_GRB=1 -> 1 : (FRS2_GRB'=2);
[sos_rel_frs] frs & FRS2_GRB=2 -> 0.0001 : (FRS2_GRB'=1);
[sos_bind_frs] frs & (FRS2_SRC=5|FRS2_SRC=6)-> 1 : (FRS2_SRC'=FRS2_SRC+2);
[sos_rel_frs] frs & (FRS2_SRC=7|FRS2_SRC=8)-> 0.0001 : (FRS2_SRC'=FRS2_SRC-2);
endmodule
module SRC
SRC : [0..8] init 1;
[src_bind] SRC>0 -> (SRC'=0);
[src_rel] SRC=0 -> (SRC'=FRS2_SRC);
[spry_bind] SRC=1 -> 1 : (SRC'=SPRY+1);
[spry_rel] SRC=2 -> 0.01 : (SRC'=1);
[spry_rel] SRC>2 -> 0.0001 : (SRC'=1);
[] SRC=2 -> 10 : (SRC'=3);
[cbl_bind_src] (SRC=3|SRC=5|SRC=7)-> 1 : (SRC'=SRC+1);
[cbl_rel_src] (SRC=4|SRC=6|SRC=8)-> 0.0001 : (SRC'=SRC-1);
[grb_bind_src] (SRC=3|SRC=4)-> 1 : (SRC'=SRC+2*GRB);
[grb_rel_src] (SRC=5|SRC=6)-> 0.0001 : (SRC'=SRC-2);
[grb_rel_src] (SRC=7|SRC=8)-> 0.0001 : (SRC'=SRC-4);
[sos_bind_src] (SRC=5|SRC=6)-> 1 : (SRC'=SRC+2);
[sos_rel_src] (SRC=7|SRC=8)-> 0.0001 : (SRC'=SRC-2);
endmodule
module SPRY
SPRY : [0..7] init 0;
app : [0..1] init 0;
[spry_bind] SPRY>0 -> (SPRY'=0);
[spry_bind_frs] SPRY>0 -> (SPRY'=0);
[spry_rel] SPRY=0 & SRC>0 -> (SPRY'=SRC-1);
[spry_rel_frs] SPRY=0 & FRS2_SRC>0 -> (SPRY'=FRS2_SRC-1);
[] SPRY=0 & app=0 -> 1/(15*60) : (SPRY'=1) & (app'=1);
[cbl_bind] (SPRY=2|SPRY=4|SPRY=6)-> 1 : (SPRY'= SPRY+1);
[cbl_rel] (SPRY=3|SPRY=5|SPRY=7)-> 0.0001 : (SPRY'= SPRY-1);
[grb_bind_spry] (SPRY=2|SPRY=3)-> 1 : (SPRY'= SPRY+2*GRB);
[grb_rel_spry] (SPRY=4|SPRY=5)-> 0.0001 : (SPRY'= SPRY-2);
[grb_rel_spry] (SPRY=6|SPRY=7)-> 0.0001 : (SPRY'= SPRY-4);
[sos_bind_spry] (SPRY=4|SPRY=5)-> 1 : (SPRY'=SPRY+2);
[sos_rel_spry] (SPRY=6|SPRY=7)-> 0.0001 : (SPRY'=SPRY-2);
endmodule
module CBL
CBL : [0..1] init 1;
[cbl_bind] CBL=1 -> (CBL'=0);
[cbl_bind_src] CBL=1 -> (CBL'=0);
[cbl_bind_frs] CBL=1 -> (CBL'=0);
[cbl_rel] CBL=0 -> (CBL'=1);
[cbl_rel_src] CBL=0 -> (CBL'=1);
[cbl_rel_frs] CBL=0 -> (CBL'=1);
[spry_dephos] true -> (CBL'=1);
endmodule
module SHP
SHP : [0..1] init 1;
[shp_bind] SHP=1 -> (SHP'=0);
[shp_rel] SHP=0 -> (SHP'=1);
endmodule
module GRB
GRB : [0..2] init 1;
[sos_bind] GRB=1 -> 1 : (GRB'=2);
[sos_rel] GRB=2 -> 0.0001 : (GRB'=1);
[grb_bind] GRB>0 -> (GRB'=0);
[grb_rel] GRB=0 -> (GRB'=FRS2_GRB);
[grb_bind_spry] GRB>0 -> (GRB'=0);
[grb_bind_src] GRB>0 -> (GRB'=0);
[grb_bind_frs] GRB>0 -> (GRB'=0);
[grb_rel_spry] GRB=0 -> (GRB'=(SPRY<6)?1:2);
[grb_rel_src] GRB=0 -> (GRB'=(SRC<7)?1:2);
[grb_rel_frs] GRB=0 -> (GRB'=(FRS2_SRC<7)?1:2);
[spry_dephos] true -> (GRB'=(FRS2_SRC<7)?1:2);
endmodule
module SOS
SOS : [0..1] init 1;
[sos_bind] SOS=1 -> (SOS'=0);
[sos_bind_spry] SOS=1 -> (SOS'=0);
[sos_bind_src] SOS=1 -> (SOS'=0);
[sos_bind_frs] SOS=1 -> (SOS'=0);
[sos_rel] SOS=0 -> (SOS'=1);
[sos_rel_spry] SOS=0 -> (SOS'=1);
[sos_rel_src] SOS=0 -> (SOS'=1);
[sos_rel_frs] SOS=0 -> (SOS'=1);
endmodule
rewards "bindings"
[grb_bind] degFGFR=0 & relocFRS2=0 & degFRS2=0 : 1;
endrewards
rewards "bound"
FRS2_GRB>0 & relocFRS2=0 & degFRS2=0 : 1;
endrewards
rewards "time"
true : 60;
endrewards