% Prolog file generated by Biocham http://contraintes.inria.fr/BIOCHAM
% Model of biochemical reactions represented in Prolog as a state transition system
% CTL specification where reachable(X)=EF(X)checkpoint(X,Y)=!E(!X U Y) oscil(X)=EG(F X & F !X)
:- include(ctl).

%%% State variables names
dimension(13).
state('CycB','APC','CDK','CycB-CDK~{p1,p2}','CycB-CDK~{p1}','C25~{p1,p2}','Wee1','C25','C25~{p1}','Wee1~{p1}','CKI','CKI-CycB-CDK~{p1}','(CKI-CycB-CDK~{p1})~{p2}').

%%% Initial state.
:- dynamic(initial/1).
initial(state(0,0,1,0,0,0,1,0,0,0,1,0,0)).

%%% transition(predecessor,successor)

% k1 for _=>CycB
transition(state(_,A,B,C,D,E,F,G,H,I,J,K,L),state(1,A,B,C,D,E,F,G,H,I,J,K,L)).

% k2*[CycB] for CycB=>_
transition(state(1,A,B,C,D,E,F,G,H,I,J,K,L),state(_,A,B,C,D,E,F,G,H,I,J,K,L)).

% k2u*[APC]*[CycB] for CycB=[APC]=>_
transition(state(1,1,A,B,C,D,E,F,G,H,I,J,K),state(_,1,A,B,C,D,E,F,G,H,I,J,K)).

% (k3*[CDK]*[CycB],k4*[CycB-CDK~{p1,p2}]) for CDK+CycB<=>CycB-CDK~{p1,p2}
transition(state(1,A,1,_,B,C,D,E,F,G,H,I,J),state(_,A,_,1,B,C,D,E,F,G,H,I,J)).

% (k3*[CDK]*[CycB],k4*[CycB-CDK~{p1,p2}]) for CDK+CycB<=>CycB-CDK~{p1,p2}
transition(state(_,A,_,1,B,C,D,E,F,G,H,I,J),state(1,A,1,_,B,C,D,E,F,G,H,I,J)).

% k5*[CycB-CDK~{p1,p2}] for CycB-CDK~{p1,p2}=>CycB-CDK~{p1}
transition(state(A,B,C,1,_,D,E,F,G,H,I,J,K),state(A,B,C,_,1,D,E,F,G,H,I,J,K)).

% k5u*[C25~{p1,p2}]*[CycB-CDK~{p1,p2}] for CycB-CDK~{p1,p2}=[C25~{p1,p2}]=>CycB-CDK~{p1}
transition(state(A,B,C,1,_,1,D,E,F,G,H,I,J),state(A,B,C,_,1,1,D,E,F,G,H,I,J)).

% k6*[CycB-CDK~{p1}] for CycB-CDK~{p1}=>CycB-CDK~{p1,p2}
transition(state(A,B,C,_,1,D,E,F,G,H,I,J,K),state(A,B,C,1,_,D,E,F,G,H,I,J,K)).

% [Wee1]*[CycB-CDK~{p1}] for CycB-CDK~{p1}=[Wee1]=>CycB-CDK~{p1,p2}
transition(state(A,B,C,_,1,D,1,E,F,G,H,I,J),state(A,B,C,1,_,D,1,E,F,G,H,I,J)).

% k7*[CycB-CDK~{p1}] for CycB-CDK~{p1}=>CDK
transition(state(A,B,_,C,1,D,E,F,G,H,I,J,K),state(A,B,1,C,_,D,E,F,G,H,I,J,K)).

% k7u*[APC]*[CycB-CDK~{p1}] for CycB-CDK~{p1}=[APC]=>CDK
transition(state(A,1,_,B,1,C,D,E,F,G,H,I,J),state(A,1,1,B,_,C,D,E,F,G,H,I,J)).

% k8 for _=>C25
transition(state(A,B,C,D,E,F,G,_,H,I,J,K,L),state(A,B,C,D,E,F,G,1,H,I,J,K,L)).

% k9*[C25] for C25=>_
transition(state(A,B,C,D,E,F,G,1,H,I,J,K,L),state(A,B,C,D,E,F,G,_,H,I,J,K,L)).

% k9*[C25~{p1}] for C25~{p1}=>_
transition(state(A,B,C,D,E,F,G,H,1,I,J,K,L),state(A,B,C,D,E,F,G,H,_,I,J,K,L)).

% k9*[C25~{p1,p2}] for C25~{p1,p2}=>_
transition(state(A,B,C,D,E,1,F,G,H,I,J,K,L),state(A,B,C,D,E,_,F,G,H,I,J,K,L)).

% bz*[C25] for C25=>C25~{p1}
transition(state(A,B,C,D,E,F,G,1,_,H,I,J,K),state(A,B,C,D,E,F,G,_,1,H,I,J,K)).

% cz*[CycB-CDK~{p1}]*[C25] for C25=[CycB-CDK~{p1}]=>C25~{p1}
transition(state(A,B,C,D,1,E,F,1,_,G,H,I,J),state(A,B,C,D,1,E,F,_,1,G,H,I,J)).

% az*[C25~{p1}] for C25~{p1}=>C25
transition(state(A,B,C,D,E,F,G,_,1,H,I,J,K),state(A,B,C,D,E,F,G,1,_,H,I,J,K)).

% bz*[C25~{p1}] for C25~{p1}=>C25~{p1,p2}
transition(state(A,B,C,D,E,_,F,G,1,H,I,J,K),state(A,B,C,D,E,1,F,G,_,H,I,J,K)).

% cz*[CycB-CDK~{p1}]*[C25~{p1}] for C25~{p1}=[CycB-CDK~{p1}]=>C25~{p1,p2}
transition(state(A,B,C,D,1,_,E,F,1,G,H,I,J),state(A,B,C,D,1,1,E,F,_,G,H,I,J)).

% az*[C25~{p1,p2}] for C25~{p1,p2}=>C25~{p1}
transition(state(A,B,C,D,E,1,F,G,_,H,I,J,K),state(A,B,C,D,E,_,F,G,1,H,I,J,K)).

% k10 for _=>Wee1
transition(state(A,B,C,D,E,F,_,G,H,I,J,K,L),state(A,B,C,D,E,F,1,G,H,I,J,K,L)).

% k11*[Wee1] for Wee1=>_
transition(state(A,B,C,D,E,F,1,G,H,I,J,K,L),state(A,B,C,D,E,F,_,G,H,I,J,K,L)).

% k11*[Wee1~{p1}] for Wee1~{p1}=>_
transition(state(A,B,C,D,E,F,G,H,I,1,J,K,L),state(A,B,C,D,E,F,G,H,I,_,J,K,L)).

% bw*[Wee1] for Wee1=>Wee1~{p1}
transition(state(A,B,C,D,E,F,1,G,H,_,I,J,K),state(A,B,C,D,E,F,_,G,H,1,I,J,K)).

% cw*[CycB-CDK~{p1}]*[Wee1] for Wee1=[CycB-CDK~{p1}]=>Wee1~{p1}
transition(state(A,B,C,D,1,E,1,F,G,_,H,I,J),state(A,B,C,D,1,E,_,F,G,1,H,I,J)).

% aw*[Wee1~{p1}] for Wee1~{p1}=>Wee1
transition(state(A,B,C,D,E,F,_,G,H,1,I,J,K),state(A,B,C,D,E,F,1,G,H,_,I,J,K)).

% [CycB-CDK~{p1}]^2/(a^2+[CycB-CDK~{p1}]^2)/tho for _=[CycB-CDK~{p1}]=>APC
transition(state(A,_,B,C,1,D,E,F,G,H,I,J,K),state(A,1,B,C,1,D,E,F,G,H,I,J,K)).

% [APC]/tho for APC=>_
transition(state(A,1,B,C,D,E,F,G,H,I,J,K,L),state(A,_,B,C,D,E,F,G,H,I,J,K,L)).

% k12 for _=>CKI
transition(state(A,B,C,D,E,F,G,H,I,J,_,K,L),state(A,B,C,D,E,F,G,H,I,J,1,K,L)).

% k13*[CKI] for CKI=>_
transition(state(A,B,C,D,E,F,G,H,I,J,1,K,L),state(A,B,C,D,E,F,G,H,I,J,_,K,L)).

% (k14*[CKI]*[CycB-CDK~{p1}],k15*[CKI-CycB-CDK~{p1}]) for CKI+CycB-CDK~{p1}<=>CKI-CycB-CDK~{p1}
transition(state(A,B,C,D,1,E,F,G,H,I,1,_,J),state(A,B,C,D,_,E,F,G,H,I,_,1,J)).

% (k14*[CKI]*[CycB-CDK~{p1}],k15*[CKI-CycB-CDK~{p1}]) for CKI+CycB-CDK~{p1}<=>CKI-CycB-CDK~{p1}
transition(state(A,B,C,D,_,E,F,G,H,I,_,1,J),state(A,B,C,D,1,E,F,G,H,I,1,_,J)).

% bi*[CKI-CycB-CDK~{p1}] for CKI-CycB-CDK~{p1}=>(CKI-CycB-CDK~{p1})~{p2}
transition(state(A,B,C,D,E,F,G,H,I,J,K,1,_),state(A,B,C,D,E,F,G,H,I,J,K,_,1)).

% ci*[CycB-CDK~{p1}]*[CKI-CycB-CDK~{p1}] for CKI-CycB-CDK~{p1}=[CycB-CDK~{p1}]=>(CKI-CycB-CDK~{p1})~{p2}
transition(state(A,B,C,D,1,E,F,G,H,I,J,1,_),state(A,B,C,D,1,E,F,G,H,I,J,_,1)).

% ai*[(CKI-CycB-CDK~{p1})~{p2}] for (CKI-CycB-CDK~{p1})~{p2}=>CKI-CycB-CDK~{p1}
transition(state(A,B,C,D,E,F,G,H,I,J,K,_,1),state(A,B,C,D,E,F,G,H,I,J,K,1,_)).

% k16*[(CKI-CycB-CDK~{p1})~{p2}] for (CKI-CycB-CDK~{p1})~{p2}=>CDK
transition(state(A,B,_,C,D,E,F,G,H,I,J,K,1),state(A,B,1,C,D,E,F,G,H,I,J,K,_)).

% k16u*[APC]*[(CKI-CycB-CDK~{p1})~{p2}] for (CKI-CycB-CDK~{p1})~{p2}=[APC]=>CDK
transition(state(A,1,_,B,C,D,E,F,G,H,I,J,1),state(A,1,1,B,C,D,E,F,G,H,I,J,_)).

%%% CTL specification

% Ei(reachable(CycB))
ctl('Ei'(reachable(1))).

% Ei(reachable(!(CycB)))
ctl('Ei'(reachable(!(1)))).

% Ai(oscil(CycB))
ctl('Ai'(oscil(1))).

% Ei(reachable(APC))
ctl('Ei'(reachable(2))).

% Ei(reachable(!(APC)))
ctl('Ei'(reachable(!(2)))).

% Ai(oscil(APC))
ctl('Ai'(oscil(2))).

% Ai(AG(!(APC)->checkpoint(CycB-CDK~{p1},APC)))
ctl('Ai'('AG'(->(!(2),checkpoint(5,2))))).

% Ei(reachable(CDK))
ctl('Ei'(reachable(3))).

% Ei(reachable(!(CDK)))
ctl('Ei'(reachable(!(3)))).

% Ai(oscil(CDK))
ctl('Ai'(oscil(3))).

% Ei(reachable(CycB-CDK~{p1,p2}))
ctl('Ei'(reachable(4))).

% Ei(reachable(!(CycB-CDK~{p1,p2})))
ctl('Ei'(reachable(!(4)))).

% Ai(oscil(CycB-CDK~{p1,p2}))
ctl('Ai'(oscil(4))).

% Ei(reachable(CycB-CDK~{p1}))
ctl('Ei'(reachable(5))).

% Ei(reachable(!(CycB-CDK~{p1})))
ctl('Ei'(reachable(!(5)))).

% Ai(oscil(CycB-CDK~{p1}))
ctl('Ai'(oscil(5))).

% Ei(reachable(C25~{p1,p2}))
ctl('Ei'(reachable(6))).

% Ei(reachable(!(C25~{p1,p2})))
ctl('Ei'(reachable(!(6)))).

% Ai(oscil(C25~{p1,p2}))
ctl('Ai'(oscil(6))).

% Ai(AG(!(C25~{p1,p2})->checkpoint(C25~{p1},C25~{p1,p2})))
ctl('Ai'('AG'(->(!(6),checkpoint(9,6))))).

% Ei(reachable(Wee1))
ctl('Ei'(reachable(7))).

% Ei(reachable(!(Wee1)))
ctl('Ei'(reachable(!(7)))).

% Ai(oscil(Wee1))
ctl('Ai'(oscil(7))).

% Ei(reachable(C25))
ctl('Ei'(reachable(8))).

% Ei(reachable(!(C25)))
ctl('Ei'(reachable(!(8)))).

% Ai(oscil(C25))
ctl('Ai'(oscil(8))).

% Ei(reachable(C25~{p1}))
ctl('Ei'(reachable(9))).

% Ei(reachable(!(C25~{p1})))
ctl('Ei'(reachable(!(9)))).

% Ai(oscil(C25~{p1}))
ctl('Ai'(oscil(9))).

% Ei(reachable(Wee1~{p1}))
ctl('Ei'(reachable(10))).

% Ei(reachable(!(Wee1~{p1})))
ctl('Ei'(reachable(!(10)))).

% Ai(oscil(Wee1~{p1}))
ctl('Ai'(oscil(10))).

% Ai(AG(!(Wee1~{p1})->checkpoint(Wee1,Wee1~{p1})))
ctl('Ai'('AG'(->(!(10),checkpoint(7,10))))).

% Ei(reachable(CKI))
ctl('Ei'(reachable(11))).

% Ei(reachable(!(CKI)))
ctl('Ei'(reachable(!(11)))).

% Ai(oscil(CKI))
ctl('Ai'(oscil(11))).

% Ei(reachable(CKI-CycB-CDK~{p1}))
ctl('Ei'(reachable(12))).

% Ei(reachable(!(CKI-CycB-CDK~{p1})))
ctl('Ei'(reachable(!(12)))).

% Ai(oscil(CKI-CycB-CDK~{p1}))
ctl('Ai'(oscil(12))).

% Ei(reachable((CKI-CycB-CDK~{p1})~{p2}))
ctl('Ei'(reachable(13))).

% Ei(reachable(!((CKI-CycB-CDK~{p1})~{p2})))
ctl('Ei'(reachable(!(13)))).

% Ai(oscil((CKI-CycB-CDK~{p1})~{p2}))
ctl('Ai'(oscil(13))).

% Ai(AG(!((CKI-CycB-CDK~{p1})~{p2})->checkpoint(CKI-CycB-CDK~{p1},(CKI-CycB-CDK~{p1})~{p2})))
ctl('Ai'('AG'(->(!(13),checkpoint(12,13))))).