-- File apoptosis


-- gene No0 = NFKB
-- gene No1 = P21
-- gene No2 = FOXM
-- gene No3 = PI3K
-- gene No4 = P53
-- gene No5 = MDM2
-- gene No6 = OGT
-- gene No7 = OGA
-- gene No8 = CMYC

var
dpP210,dpP530,dpMDM20,dpOGA0,dpOGT0,dnCMYC1,dnOGA1,dpPI3K0,dnOGT1,dpCMYC0,dnMDM21,dnP531,dpFOXM0,dnPI3K1,dnFOXM1,dnP211,dnNFKB1: parameter;

hNFKB,hP21,hFOXM,hPI3K,hP53,hMDM2,hOGT,hOGA,hCMYC :analog;
k,n: discrete;
automaton auto
synclabs: ;
initially loc_010000010;

-- for the configuration 0,1,0,0,0,0,0,1,0
loc loc_010000010: while hP53 <=  dpP530  wait {dhNFKB=0,dhP21=0,dhFOXM=0,dhPI3K=0,dhP53=1,dhMDM2=1,dhOGT=0,dhOGA=0,dhCMYC=0}
when hP53=dpP530 do {hP53'=0, k'=k+1} goto loc_010010010;

-- for the configuration 0,1,0,0,1,0,0,1,0
loc loc_010010010: while hMDM2 <=  dpMDM20  wait {dhNFKB=0,dhP21=0,dhFOXM=0,dhPI3K=0,dhP53=-1,dhMDM2=1,dhOGT=0,dhOGA=0,dhCMYC=0}
when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_010011010;

-- for the configuration 0,1,0,0,1,1,0,1,0
loc loc_010011010: while hP53 >=  dnP531  wait {dhNFKB=0,dhP21=0,dhFOXM=0,dhPI3K=0,dhP53=-1,dhMDM2=-1,dhOGT=0,dhOGA=0,dhCMYC=0}
when hP53=dnP531 do {hP53'=0, k'=k+1} goto loc_010001010;

-- for the configuration 0,1,0,0,0,1,0,1,0
loc loc_010001010: while hMDM2 >=  dnMDM21  wait {dhNFKB=0,dhP21=0,dhFOXM=0,dhPI3K=0,dhP53=1,dhMDM2=-1,dhOGT=0,dhOGA=0,dhCMYC=0}
when hMDM2=dnMDM21 do {hMDM2'=0, k'=k+1} goto loc_010000010;


end
var
r_ini, r_new,r_acc, r_old:region;
-- Remove the comment symbol from the following codes for finding invariance kernel
-- Assign the initial location and the initial values of clocks to the initial region r_ini

r_ini:= loc[auto] = loc_010000010 & hP53>=0 & hP53 <=  dpP530 & hMDM2=0 ;  --complete this line
r_new:=hide k,n in hull (post(r_ini & k=n) & ~k=n) endhide;
r_old:=r_ini & ~r_ini;
while not empty(r_new) and empty(r_new & r_ini) do
r_old:=r_new;
r_new:=hide k,n in hull(post(r_new & k=n) & ~k=n) endhide;
endwhile;
-- To verify that the initial zone is accessible from itself
if not empty (r_new & r_ini) then
---- if accessible
r_acc:=hide k,n in hull(post(r_new & k=n) &~k=n) endhide; 
r_old:=r_ini & ~r_ini; --empty region initialization
while not empty(r_acc) and not r_new=r_old do 
r_old:=r_new; 
while not empty(r_acc) and empty(r_acc & r_ini) do 
r_acc:= hide k,n in hull(post(r_acc & k=n) &~k=n) endhide; 
endwhile; 
r_acc:=hull(r_acc & r_ini); 
r_new:=hull(r_acc & r_new); 
r_acc:=hide k,n in hull(post(r_new & k=n) & ~k=n) endhide; 
endwhile; 
if not empty(r_new) then 
 prints "============================================================"; 
 prints " Delay constraintes: ";
 print  hide hNFKB,hP21,hFOXM,hPI3K,hP53,hMDM2,hOGT,hOGA,hCMYC in r_new  endhide; 
 prints "============================================================"; 
else 
 prints "Invariance kernel does not exist from the initial region "; 
endif; 
else 
prints " The initial region is not accessible from itself hence " ; 
 prints " there is no initial condition that leads to an invariance kernel."; 
endif;