% 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(6).
state('Cyclin','Cdc2~{p1}','Cdc2-Cyclin~{p1,p2}','Cdc2-Cyclin~{p1}','Cdc2','Cyclin~{p1}').

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

%%% transition(predecessor,successor)

% k1 for _=>Cyclin
transition(state(_,A,B,C,D,E),state(1,A,B,C,D,E)).

% k2*[Cyclin] for Cyclin=>_
transition(state(1,A,B,C,D,E),state(_,A,B,C,D,E)).

% k3*[Cyclin]*[Cdc2~{p1}] for Cyclin+Cdc2~{p1}=>Cdc2-Cyclin~{p1,p2}
transition(state(1,1,_,A,B,C),state(_,_,1,A,B,C)).

% k4p*[Cdc2-Cyclin~{p1,p2}] for Cdc2-Cyclin~{p1,p2}=>Cdc2-Cyclin~{p1}
transition(state(A,B,1,_,C,D),state(A,B,_,1,C,D)).

% k4*[Cdc2-Cyclin~{p1}]^2*[Cdc2-Cyclin~{p1,p2}] for Cdc2-Cyclin~{p1,p2}=[Cdc2-Cyclin~{p1}]=>Cdc2-Cyclin~{p1}
transition(state(A,B,1,1,C,D),state(A,B,_,1,C,D)).

% k5*[Cdc2-Cyclin~{p1}] for Cdc2-Cyclin~{p1}=>Cdc2-Cyclin~{p1,p2}
transition(state(A,B,_,1,C,D),state(A,B,1,_,C,D)).

% k6*[Cdc2-Cyclin~{p1}] for Cdc2-Cyclin~{p1}=>Cyclin~{p1}+Cdc2
transition(state(A,B,C,1,_,_),state(A,B,C,_,1,1)).

% k7*[Cyclin~{p1}] for Cyclin~{p1}=>_
transition(state(A,B,C,D,E,1),state(A,B,C,D,E,_)).

% k8*[Cdc2] for Cdc2=>Cdc2~{p1}
transition(state(A,_,B,C,1,D),state(A,1,B,C,_,D)).

% k9*[Cdc2~{p1}] for Cdc2~{p1}=>Cdc2
transition(state(A,1,B,C,_,D),state(A,_,B,C,1,D)).

%%% CTL specification

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

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

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

% Ei(reachable(Cdc2~{p1}))
ctl('Ei'(reachable(2))).

% Ei(reachable(!(Cdc2~{p1})))
ctl('Ei'(reachable(!(2)))).

% Ai(oscil(Cdc2~{p1}))
ctl('Ai'(oscil(2))).

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

% Ei(reachable(Cdc2-Cyclin~{p1,p2}))
ctl('Ei'(reachable(3))).

% Ei(reachable(!(Cdc2-Cyclin~{p1,p2})))
ctl('Ei'(reachable(!(3)))).

% Ai(oscil(Cdc2-Cyclin~{p1,p2}))
ctl('Ai'(oscil(3))).

% Ei(reachable(Cdc2-Cyclin~{p1}))
ctl('Ei'(reachable(4))).

% Ei(reachable(!(Cdc2-Cyclin~{p1})))
ctl('Ei'(reachable(!(4)))).

% Ai(oscil(Cdc2-Cyclin~{p1}))
ctl('Ai'(oscil(4))).

% Ai(AG(!(Cdc2-Cyclin~{p1})->checkpoint(Cdc2-Cyclin~{p1,p2},Cdc2-Cyclin~{p1})))
ctl('Ai'('AG'(->(!(4),checkpoint(3,4))))).

% Ei(reachable(Cdc2))
ctl('Ei'(reachable(5))).

% Ei(reachable(!(Cdc2)))
ctl('Ei'(reachable(!(5)))).

% Ai(oscil(Cdc2))
ctl('Ai'(oscil(5))).

% Ei(reachable(Cyclin~{p1}))
ctl('Ei'(reachable(6))).

% Ei(reachable(!(Cyclin~{p1})))
ctl('Ei'(reachable(!(6)))).

% Ai(oscil(Cyclin~{p1}))
ctl('Ai'(oscil(6))).

% Ai(AG(!(Cyclin~{p1})->checkpoint(Cdc2-Cyclin~{p1},Cyclin~{p1})))
ctl('Ai'('AG'(->(!(6),checkpoint(4,6))))).