-- 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,dpNFKB0: parameter;

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

-- for the configuration 1,0,0,0,0,0,1,0,0
loc loc_100000100: while hNFKB >=  dnNFKB1 & hP21 <=  dpP210 & hPI3K <=  dpPI3K0 & hP53 <=  dpP530 & hOGT >=  dnOGT1 & hCMYC <=  dpCMYC0  wait {dhNFKB=-1,dhP21=1,dhFOXM=1,dhPI3K=1,dhP53=1,dhMDM2=1,dhOGT=-1,dhOGA=1,dhCMYC=1}
when hNFKB=dnNFKB1 do {hNFKB'=0, k'=k+1} goto loc_000000100;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_110000100;
----when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_101000100;
--when hPI3K=dpPI3K0 do {hPI3K'=0, k'=k+1} goto loc_100100100;
--when hP53=dpP530 do {hP53'=0, k'=k+1} goto loc_100010100;
----when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_100001100;
--when hOGT=dnOGT1 do {hOGT'=0, k'=k+1} goto loc_100000000;
----when hOGA=dpOGA0 do {hOGA'=0, k'=k+1} goto loc_100000110;
--when hCMYC=dpCMYC0 do {hCMYC'=0, k'=k+1} goto loc_100000101;

-- for the configuration 0,0,0,0,0,0,1,0,0
loc loc_000000100: while hP21 <=  dpP210 & hPI3K <=  dpPI3K0 & hP53 <=  dpP530 & hOGT >=  dnOGT1 & hCMYC <=  dpCMYC0  wait {dhNFKB=1,dhP21=1,dhFOXM=1,dhPI3K=1,dhP53=1,dhMDM2=1,dhOGT=-1,dhOGA=1,dhCMYC=1}
----when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100000100;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_010000100;
----when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001000100;
--when hPI3K=dpPI3K0 do {hPI3K'=0, k'=k+1} goto loc_000100100;
when hP53=dpP530 do {hP53'=0, k'=k+1} goto loc_000010100;
----when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_000001100;
--when hOGT=dnOGT1 do {hOGT'=0, k'=k+1} goto loc_000000000;
----when hOGA=dpOGA0 do {hOGA'=0, k'=k+1} goto loc_000000110;
--when hCMYC=dpCMYC0 do {hCMYC'=0, k'=k+1} goto loc_000000101;

-- for the configuration 0,0,0,0,1,0,1,0,0
loc loc_000010100: while hP21 <=  dpP210 & hPI3K <=  dpPI3K0 & hMDM2 <=  dpMDM20 & hOGT >=  dnOGT1 & hCMYC <=  dpCMYC0  wait {dhNFKB=1,dhP21=1,dhFOXM=1,dhPI3K=1,dhP53=-1,dhMDM2=1,dhOGT=-1,dhOGA=1,dhCMYC=1}
----when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100010100;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_010010100;
----when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001010100;
when hPI3K=dpPI3K0 do {hPI3K'=0, k'=k+1} goto loc_000110100;
----when hP53=dnP531 do {hP53'=0, k'=k+1} goto loc_000000100;
--when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_000011100;
--when hOGT=dnOGT1 do {hOGT'=0, k'=k+1} goto loc_000010000;
----when hOGA=dpOGA0 do {hOGA'=0, k'=k+1} goto loc_000010110;
--when hCMYC=dpCMYC0 do {hCMYC'=0, k'=k+1} goto loc_000010101;

-- for the configuration 0,0,0,1,1,0,1,0,0
loc loc_000110100: while hNFKB <=  dpNFKB0 & hP21 <=  dpP210 & hFOXM <=  dpFOXM0 & hMDM2 <=  dpMDM20 & hOGT >=  dnOGT1 & hCMYC <=  dpCMYC0  wait {dhNFKB=1,dhP21=1,dhFOXM=1,dhPI3K=-1,dhP53=-1,dhMDM2=1,dhOGT=-1,dhOGA=1,dhCMYC=1}
--when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100110100;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_010110100;
--when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001110100;
----when hPI3K=dnPI3K1 do {hPI3K'=0, k'=k+1} goto loc_000010100;
----when hP53=dnP531 do {hP53'=0, k'=k+1} goto loc_000100100;
when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_000111100;
--when hOGT=dnOGT1 do {hOGT'=0, k'=k+1} goto loc_000110000;
----when hOGA=dpOGA0 do {hOGA'=0, k'=k+1} goto loc_000110110;
--when hCMYC=dpCMYC0 do {hCMYC'=0, k'=k+1} goto loc_000110101;

-- for the configuration 0,0,0,1,1,1,1,0,0
loc loc_000111100: while hNFKB <=  dpNFKB0 & hP21 <=  dpP210 & hFOXM <=  dpFOXM0 & hP53 >=  dnP531 & hOGT >=  dnOGT1 & hCMYC <=  dpCMYC0  wait {dhNFKB=1,dhP21=1,dhFOXM=1,dhPI3K=-1,dhP53=-1,dhMDM2=-1,dhOGT=-1,dhOGA=1,dhCMYC=1}
--when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100111100;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_010111100;
--when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001111100;
----when hPI3K=dnPI3K1 do {hPI3K'=0, k'=k+1} goto loc_000011100;
when hP53=dnP531 do {hP53'=0, k'=k+1} goto loc_000101100;
----when hMDM2=dnMDM21 do {hMDM2'=0, k'=k+1} goto loc_000110100;
--when hOGT=dnOGT1 do {hOGT'=0, k'=k+1} goto loc_000111000;
----when hOGA=dpOGA0 do {hOGA'=0, k'=k+1} goto loc_000111110;
--when hCMYC=dpCMYC0 do {hCMYC'=0, k'=k+1} goto loc_000111101;

-- for the configuration 0,0,0,1,0,1,1,0,0
loc loc_000101100: while hNFKB <=  dpNFKB0 & hFOXM <=  dpFOXM0 & hMDM2 >=  dnMDM21 & hOGT >=  dnOGT1 & hCMYC <=  dpCMYC0  wait {dhNFKB=1,dhP21=0,dhFOXM=1,dhPI3K=-1,dhP53=1,dhMDM2=-1,dhOGT=-1,dhOGA=1,dhCMYC=1}
--when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100101100;
--when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001101100;
----when hPI3K=dnPI3K1 do {hPI3K'=0, k'=k+1} goto loc_000001100;
----when hP53=dpP530 do {hP53'=0, k'=k+1} goto loc_000111100;
when hMDM2=dnMDM21 do {hMDM2'=0, k'=k+1} goto loc_000100100;
--when hOGT=dnOGT1 do {hOGT'=0, k'=k+1} goto loc_000101000;
----when hOGA=dpOGA0 do {hOGA'=0, k'=k+1} goto loc_000101110;
--when hCMYC=dpCMYC0 do {hCMYC'=0, k'=k+1} goto loc_000101101;

-- for the configuration 0,0,0,1,0,0,1,0,0
loc loc_000100100: while hNFKB <=  dpNFKB0 & hFOXM <=  dpFOXM0 & hP53 <=  dpP530 & hOGT >=  dnOGT1 & hCMYC <=  dpCMYC0  wait {dhNFKB=1,dhP21=1,dhFOXM=1,dhPI3K=-1,dhP53=1,dhMDM2=1,dhOGT=-1,dhOGA=1,dhCMYC=1}
--when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100100100;
----when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_010100100;
--when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001100100;
----when hPI3K=dnPI3K1 do {hPI3K'=0, k'=k+1} goto loc_000000100;
--when hP53=dpP530 do {hP53'=0, k'=k+1} goto loc_000110100;
----when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_000101100;
--when hOGT=dnOGT1 do {hOGT'=0, k'=k+1} goto loc_000100000;
----when hOGA=dpOGA0 do {hOGA'=0, k'=k+1} goto loc_000100110;
when hCMYC=dpCMYC0 do {hCMYC'=0, k'=k+1} goto loc_000100101;

-- for the configuration 0,0,0,1,0,0,1,0,1
loc loc_000100101: while hNFKB <=  dpNFKB0 & hFOXM <=  dpFOXM0 & hP53 <=  dpP530  wait {dhNFKB=1,dhP21=1,dhFOXM=1,dhPI3K=0,dhP53=1,dhMDM2=1,dhOGT=0,dhOGA=0,dhCMYC=0}
--when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100100101;
----when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_010100101;
--when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001100101;
when hP53=dpP530 do {hP53'=0, k'=k+1} goto loc_000110101;
----when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_000101101;

-- for the configuration 0,0,0,1,1,0,1,0,1
loc loc_000110101: while hNFKB <=  dpNFKB0 & hP21 <=  dpP210 & hFOXM <=  dpFOXM0 & hMDM2 <=  dpMDM20  wait {dhNFKB=1,dhP21=1,dhFOXM=1,dhPI3K=0,dhP53=-1,dhMDM2=1,dhOGT=0,dhOGA=0,dhCMYC=0}
when hNFKB=dpNFKB0 do {hNFKB'=0, k'=k+1} goto loc_100110101;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_010110101;
--when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_001110101;
----when hP53=dnP531 do {hP53'=0, k'=k+1} goto loc_000100101;
--when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_000111101;

-- for the configuration 1,0,0,1,1,0,1,0,1
loc loc_100110101: while hP21 <=  dpP210 & hFOXM <=  dpFOXM0 & hMDM2 <=  dpMDM20  wait {dhNFKB=-1,dhP21=1,dhFOXM=1,dhPI3K=0,dhP53=0,dhMDM2=1,dhOGT=0,dhOGA=0,dhCMYC=0}
----when hNFKB=dnNFKB1 do {hNFKB'=0, k'=k+1} goto loc_000110101;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_110110101;
--when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_101110101;
when hMDM2=dpMDM20 do {hMDM2'=0, k'=k+1} goto loc_100111101;

-- for the configuration 1,0,0,1,1,1,1,0,1
loc loc_100111101: while hP21 <=  dpP210 & hFOXM <=  dpFOXM0  wait {dhNFKB=-1,dhP21=1,dhFOXM=1,dhPI3K=0,dhP53=0,dhMDM2=0,dhOGT=0,dhOGA=0,dhCMYC=0}
----when hNFKB=dnNFKB1 do {hNFKB'=0, k'=k+1} goto loc_000111101;
--when hP21=dpP210 do {hP21'=0, k'=k+1} goto loc_110111101;
when hFOXM=dpFOXM0 do {hFOXM'=0, k'=k+1} goto loc_101111101;

-- for the configuration 1,0,1,1,1,1,1,0,1
loc loc_101111101: while  True  wait {dhNFKB=0,dhP21=0,dhFOXM=0,dhPI3K=0,dhP53=0,dhMDM2=0,dhOGT=0,dhOGA=0,dhCMYC=0}
end
var
r_ini, r_new,r_acc, r_old:region;
--r_ini:= loc[auto] = loc_101111101 & hMDM2=0 & hCMYC=0 ; 
--r_ini:= loc[auto] = loc_101111101 & hNFKB=0 & hP21=0 & hFOXM=0 & hPI3K=0 & hP53=0 & hMDM2=0 & hOGT=0 & hOGA=0 & hCMYC=0 ;
r_ini:= loc[auto] = loc_100000100 & hNFKB=0 & hP21=0 & hFOXM=0 & hPI3K=0 & hP53=0 & hMDM2=0 & hOGT=0 & hOGA=0 & hCMYC=0 ;
--r_acc := pre(pre(pre(pre(r_ini))));
r_acc := post(post(post(post(post(post(post(post(post(post(post(r_ini)))))))))));

 prints "============================================================"; 
 prints " Delay constraintes: ";
 print  hide hNFKB,hP21,hFOXM,hPI3K,hP53,hMDM2,hOGT,hOGA,hCMYC in r_acc  endhide; 
 prints "============================================================";