% Stochastic Logic Program file generated by Biocham http://contraintes.inria.fr/BIOCHAM
% Model of biochemical reactions represented in SLP 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)

%%% State variables names
dimension(22).
state('RAF','RAFK','RAF-RAFK','RAFPH','RAF~{p1}','RAFPH-RAF~{p1}','MEK','MEK-RAF~{p1}','MEK~{p1}','MEK~{p1}-RAF~{p1}','MEKPH','MEKPH-MEK~{p1}','MEK~{p1,p2}','MEKPH-MEK~{p1,p2}','MAPK','MAPK-MEK~{p1,p2}','MAPK~{p1}','MAPK~{p1}-MEK~{p1,p2}','MAPKPH','MAPKPH-MAPK~{p1}','MAPK~{p1,p2}','MAPKPH-MAPK~{p1,p2}').

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

%%% transition(predecessor,successor)

% (1*[RAF]*[RAFK],0.40000000000000002*[RAF-RAFK]) for RAF+RAFK<=>RAF-RAFK
1 :: transition(state(1,1,_,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(_,_,1,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (1*[RAF]*[RAFK],0.40000000000000002*[RAF-RAFK]) for RAF+RAFK<=>RAF-RAFK
0.40000000000000002 :: transition(state(_,_,1,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(1,1,_,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (0.5*[RAF~{p1}]*[RAFPH],0.5*[RAF~{p1}-RAFPH]) for RAF~{p1}+RAFPH<=>RAF~{p1}-RAFPH
0.5 :: transition(state(A,B,C,1,1,_,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,_,_,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (0.5*[RAF~{p1}]*[RAFPH],0.5*[RAF~{p1}-RAFPH]) for RAF~{p1}+RAFPH<=>RAF~{p1}-RAFPH
0.5 :: transition(state(A,B,C,_,_,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,1,1,_,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (3.2999999999999998*[MEK~ $P]*[RAF~{p1}],0.41999999999999998*[MEK~ $P-RAF~{p1}]) for MEK~ $P+RAF~{p1}<=>MEK~ $P-RAF~{p1} where p2 not in $P
3.2999999999999998 :: transition(state(A,B,C,D,1,E,1,_,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,_,E,_,1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (3.2999999999999998*[MEK~ $P]*[RAF~{p1}],0.41999999999999998*[MEK~ $P-RAF~{p1}]) for MEK~ $P+RAF~{p1}<=>MEK~ $P-RAF~{p1} where p2 not in $P
0.41999999999999998 :: transition(state(A,B,C,D,_,E,_,1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,1,E,1,_,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (3.2999999999999998*[MEK~ $P]*[RAF~{p1}],0.41999999999999998*[MEK~ $P-RAF~{p1}]) for MEK~ $P+RAF~{p1}<=>MEK~ $P-RAF~{p1} where p2 not in $P
3.2999999999999998 :: transition(state(A,B,C,D,1,E,F,G,1,_,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,_,E,F,G,_,1,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (3.2999999999999998*[MEK~ $P]*[RAF~{p1}],0.41999999999999998*[MEK~ $P-RAF~{p1}]) for MEK~ $P+RAF~{p1}<=>MEK~ $P-RAF~{p1} where p2 not in $P
0.41999999999999998 :: transition(state(A,B,C,D,_,E,F,G,_,1,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,1,E,F,G,1,_,H,I,J,K,L,M,N,O,P,Q,R,S)).

% (10*[MEKPH]*[MEK~{p1}~ $P],0.80000000000000004*[MEK~{p1}~ $P-MEKPH]) for MEKPH+MEK~{p1}~ $P<=>MEK~{p1}~ $P-MEKPH
10 :: transition(state(A,B,C,D,E,F,G,H,1,I,1,_,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,_,I,_,1,J,K,L,M,N,O,P,Q,R,S)).

% (10*[MEKPH]*[MEK~{p1}~ $P],0.80000000000000004*[MEK~{p1}~ $P-MEKPH]) for MEKPH+MEK~{p1}~ $P<=>MEK~{p1}~ $P-MEKPH
0.80000000000000004 :: transition(state(A,B,C,D,E,F,G,H,_,I,_,1,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,1,I,1,_,J,K,L,M,N,O,P,Q,R,S)).

% (10*[MEKPH]*[MEK~{p1}~ $P],0.80000000000000004*[MEK~{p1}~ $P-MEKPH]) for MEKPH+MEK~{p1}~ $P<=>MEK~{p1}~ $P-MEKPH
10 :: transition(state(A,B,C,D,E,F,G,H,I,J,1,K,1,_,L,M,N,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,I,J,_,K,_,1,L,M,N,O,P,Q,R,S)).

% (10*[MEKPH]*[MEK~{p1}~ $P],0.80000000000000004*[MEK~{p1}~ $P-MEKPH]) for MEKPH+MEK~{p1}~ $P<=>MEK~{p1}~ $P-MEKPH
0.80000000000000004 :: transition(state(A,B,C,D,E,F,G,H,I,J,_,K,_,1,L,M,N,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,I,J,1,K,1,_,L,M,N,O,P,Q,R,S)).

% (20*[MAPK~ $P]*[MEK~{p1,p2}],0.69999999999999996*[MAPK~ $P-MEK~{p1,p2}]) for MAPK~ $P+MEK~{p1,p2}<=>MAPK~ $P-MEK~{p1,p2} where p2 not in $P
20 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,1,M,1,_,N,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,_,M,_,1,N,O,P,Q,R,S)).

% (20*[MAPK~ $P]*[MEK~{p1,p2}],0.69999999999999996*[MAPK~ $P-MEK~{p1,p2}]) for MAPK~ $P+MEK~{p1,p2}<=>MAPK~ $P-MEK~{p1,p2} where p2 not in $P
0.69999999999999996 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,_,M,_,1,N,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,1,M,1,_,N,O,P,Q,R,S)).

% (20*[MAPK~ $P]*[MEK~{p1,p2}],0.69999999999999996*[MAPK~ $P-MEK~{p1,p2}]) for MAPK~ $P+MEK~{p1,p2}<=>MAPK~ $P-MEK~{p1,p2} where p2 not in $P
20 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,1,M,N,O,1,_,P,Q,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,_,M,N,O,_,1,P,Q,R,S)).

% (20*[MAPK~ $P]*[MEK~{p1,p2}],0.69999999999999996*[MAPK~ $P-MEK~{p1,p2}]) for MAPK~ $P+MEK~{p1,p2}<=>MAPK~ $P-MEK~{p1,p2} where p2 not in $P
0.69999999999999996 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,_,M,N,O,_,1,P,Q,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,1,M,N,O,1,_,P,Q,R,S)).

% (5*[MAPKPH]*[MAPK~{p1}~ $P],0.40000000000000002*[MAPK~{p1}~ $P-MAPKPH]) for MAPKPH+MAPK~{p1}~ $P<=>MAPK~{p1}~ $P-MAPKPH
5 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1,Q,1,_,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,_,Q,_,1,R,S)).

% (5*[MAPKPH]*[MAPK~{p1}~ $P],0.40000000000000002*[MAPK~{p1}~ $P-MAPKPH]) for MAPKPH+MAPK~{p1}~ $P<=>MAPK~{p1}~ $P-MAPKPH
0.40000000000000002 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,_,Q,_,1,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1,Q,1,_,R,S)).

% (5*[MAPKPH]*[MAPK~{p1}~ $P],0.40000000000000002*[MAPK~{p1}~ $P-MAPKPH]) for MAPKPH+MAPK~{p1}~ $P<=>MAPK~{p1}~ $P-MAPKPH
5 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,1,S,1,_),state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,_,S,_,1)).

% (5*[MAPKPH]*[MAPK~{p1}~ $P],0.40000000000000002*[MAPK~{p1}~ $P-MAPKPH]) for MAPKPH+MAPK~{p1}~ $P<=>MAPK~{p1}~ $P-MAPKPH
0.40000000000000002 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,_,S,_,1),state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,1,S,1,_)).

% 0.10000000000000001*[RAF-RAFK] for RAF-RAFK=>RAFK+RAF~{p1}
0.10000000000000001 :: transition(state(A,_,1,B,_,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,1,_,B,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% 0.10000000000000001*[RAF~{p1}-RAFPH] for RAF~{p1}-RAFPH=>RAF+RAFPH
0.10000000000000001 :: transition(state(_,A,B,_,C,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(1,A,B,1,C,_,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% 0.10000000000000001*[MEK~{p1}-RAF~{p1}] for MEK~{p1}-RAF~{p1}=>MEK~{p1,p2}+RAF~{p1}
0.10000000000000001 :: transition(state(A,B,C,D,_,E,F,G,H,1,I,J,_,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,1,E,F,G,H,_,I,J,1,K,L,M,N,O,P,Q,R,S)).

% 0.10000000000000001*[MEK-RAF~{p1}] for MEK-RAF~{p1}=>MEK~{p1}+RAF~{p1}
0.10000000000000001 :: transition(state(A,B,C,D,_,E,F,1,_,G,H,I,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,1,E,F,_,1,G,H,I,J,K,L,M,N,O,P,Q,R,S)).

% 0.10000000000000001*[MEK~{p1}-MEKPH] for MEK~{p1}-MEKPH=>MEK+MEKPH
0.10000000000000001 :: transition(state(A,B,C,D,E,F,_,G,H,I,_,1,J,K,L,M,N,O,P,Q,R,S),state(A,B,C,D,E,F,1,G,H,I,1,_,J,K,L,M,N,O,P,Q,R,S)).

% 0.10000000000000001*[MEK~{p1,p2}-MEKPH] for MEK~{p1,p2}-MEKPH=>MEK~{p1}+MEKPH
0.10000000000000001 :: transition(state(A,B,C,D,E,F,G,H,_,I,_,J,K,1,L,M,N,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,1,I,1,J,K,_,L,M,N,O,P,Q,R,S)).

% 0.10000000000000001*[MAPK-MEK~{p1,p2}] for MAPK-MEK~{p1,p2}=>MAPK~{p1}+MEK~{p1,p2}
0.10000000000000001 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,_,M,N,1,_,O,P,Q,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,1,M,N,_,1,O,P,Q,R,S)).

% 0.10000000000000001*[MAPK~{p1}-MEK~{p1,p2}] for MAPK~{p1}-MEK~{p1,p2}=>MAPK~{p1,p2}+MEK~{p1,p2}
0.10000000000000001 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,_,M,N,O,P,1,Q,R,_,S),state(A,B,C,D,E,F,G,H,I,J,K,L,1,M,N,O,P,_,Q,R,1,S)).

% 0.10000000000000001*[MAPK~{p1}-MAPKPH] for MAPK~{p1}-MAPKPH=>MAPK+MAPKPH
0.10000000000000001 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,_,O,P,Q,_,1,R,S),state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,1,O,P,Q,1,_,R,S)).

% 0.10000000000000001*[MAPK~{p1,p2}-MAPKPH] for MAPK~{p1,p2}-MAPKPH=>MAPK~{p1}+MAPKPH
0.10000000000000001 :: transition(state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,_,Q,_,R,S,1),state(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1,Q,1,R,S,_)).

%%% CTL specification

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

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

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

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

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

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

% Ai(AG(!(RAFK)->checkpoint(RAF-RAFK,RAFK)))
ctl('Ai'('AG'(->(!(2),checkpoint(3,2))))).

% Ei(reachable(RAF-RAFK))
ctl('Ei'(reachable(3))).

% Ei(reachable(!(RAF-RAFK)))
ctl('Ei'(reachable(!(3)))).

% Ai(oscil(RAF-RAFK))
ctl('Ai'(oscil(3))).

% Ai(AG(!(RAF-RAFK)->checkpoint(RAF,RAF-RAFK)))
ctl('Ai'('AG'(->(!(3),checkpoint(1,3))))).

% Ai(AG(!(RAF-RAFK)->checkpoint(RAFK,RAF-RAFK)))
ctl('Ai'('AG'(->(!(3),checkpoint(2,3))))).

% Ei(reachable(RAFPH))
ctl('Ei'(reachable(4))).

% Ei(reachable(!(RAFPH)))
ctl('Ei'(reachable(!(4)))).

% Ai(oscil(RAFPH))
ctl('Ai'(oscil(4))).

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

% Ei(reachable(RAF~{p1}))
ctl('Ei'(reachable(5))).

% Ei(reachable(!(RAF~{p1})))
ctl('Ei'(reachable(!(5)))).

% Ai(oscil(RAF~{p1}))
ctl('Ai'(oscil(5))).

% Ei(reachable(RAFPH-RAF~{p1}))
ctl('Ei'(reachable(6))).

% Ei(reachable(!(RAFPH-RAF~{p1})))
ctl('Ei'(reachable(!(6)))).

% Ai(oscil(RAFPH-RAF~{p1}))
ctl('Ai'(oscil(6))).

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

% Ai(AG(!(RAFPH-RAF~{p1})->checkpoint(RAF~{p1},RAFPH-RAF~{p1})))
ctl('Ai'('AG'(->(!(6),checkpoint(5,6))))).

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

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

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

% Ei(reachable(MEK-RAF~{p1}))
ctl('Ei'(reachable(8))).

% Ei(reachable(!(MEK-RAF~{p1})))
ctl('Ei'(reachable(!(8)))).

% Ai(oscil(MEK-RAF~{p1}))
ctl('Ai'(oscil(8))).

% Ai(AG(!(MEK-RAF~{p1})->checkpoint(MEK,MEK-RAF~{p1})))
ctl('Ai'('AG'(->(!(8),checkpoint(7,8))))).

% Ai(AG(!(MEK-RAF~{p1})->checkpoint(RAF~{p1},MEK-RAF~{p1})))
ctl('Ai'('AG'(->(!(8),checkpoint(5,8))))).

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

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

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

% Ei(reachable(MEK~{p1}-RAF~{p1}))
ctl('Ei'(reachable(10))).

% Ei(reachable(!(MEK~{p1}-RAF~{p1})))
ctl('Ei'(reachable(!(10)))).

% Ai(oscil(MEK~{p1}-RAF~{p1}))
ctl('Ai'(oscil(10))).

% Ai(AG(!(MEK~{p1}-RAF~{p1})->checkpoint(RAF~{p1},MEK~{p1}-RAF~{p1})))
ctl('Ai'('AG'(->(!(10),checkpoint(5,10))))).

% Ai(AG(!(MEK~{p1}-RAF~{p1})->checkpoint(MEK~{p1},MEK~{p1}-RAF~{p1})))
ctl('Ai'('AG'(->(!(10),checkpoint(9,10))))).

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

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

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

% Ei(reachable(MEKPH-MEK~{p1}))
ctl('Ei'(reachable(12))).

% Ei(reachable(!(MEKPH-MEK~{p1})))
ctl('Ei'(reachable(!(12)))).

% Ai(oscil(MEKPH-MEK~{p1}))
ctl('Ai'(oscil(12))).

% Ai(AG(!(MEKPH-MEK~{p1})->checkpoint(MEKPH,MEKPH-MEK~{p1})))
ctl('Ai'('AG'(->(!(12),checkpoint(11,12))))).

% Ai(AG(!(MEKPH-MEK~{p1})->checkpoint(MEK~{p1},MEKPH-MEK~{p1})))
ctl('Ai'('AG'(->(!(12),checkpoint(9,12))))).

% Ei(reachable(MEK~{p1,p2}))
ctl('Ei'(reachable(13))).

% Ei(reachable(!(MEK~{p1,p2})))
ctl('Ei'(reachable(!(13)))).

% Ai(oscil(MEK~{p1,p2}))
ctl('Ai'(oscil(13))).

% Ei(reachable(MEKPH-MEK~{p1,p2}))
ctl('Ei'(reachable(14))).

% Ei(reachable(!(MEKPH-MEK~{p1,p2})))
ctl('Ei'(reachable(!(14)))).

% Ai(oscil(MEKPH-MEK~{p1,p2}))
ctl('Ai'(oscil(14))).

% Ai(AG(!(MEKPH-MEK~{p1,p2})->checkpoint(MEKPH,MEKPH-MEK~{p1,p2})))
ctl('Ai'('AG'(->(!(14),checkpoint(11,14))))).

% Ai(AG(!(MEKPH-MEK~{p1,p2})->checkpoint(MEK~{p1,p2},MEKPH-MEK~{p1,p2})))
ctl('Ai'('AG'(->(!(14),checkpoint(13,14))))).

% Ei(reachable(MAPK))
ctl('Ei'(reachable(15))).

% Ei(reachable(!(MAPK)))
ctl('Ei'(reachable(!(15)))).

% Ai(oscil(MAPK))
ctl('Ai'(oscil(15))).

% Ei(reachable(MAPK-MEK~{p1,p2}))
ctl('Ei'(reachable(16))).

% Ei(reachable(!(MAPK-MEK~{p1,p2})))
ctl('Ei'(reachable(!(16)))).

% Ai(oscil(MAPK-MEK~{p1,p2}))
ctl('Ai'(oscil(16))).

% Ai(AG(!(MAPK-MEK~{p1,p2})->checkpoint(MAPK,MAPK-MEK~{p1,p2})))
ctl('Ai'('AG'(->(!(16),checkpoint(15,16))))).

% Ai(AG(!(MAPK-MEK~{p1,p2})->checkpoint(MEK~{p1,p2},MAPK-MEK~{p1,p2})))
ctl('Ai'('AG'(->(!(16),checkpoint(13,16))))).

% Ei(reachable(MAPK~{p1}))
ctl('Ei'(reachable(17))).

% Ei(reachable(!(MAPK~{p1})))
ctl('Ei'(reachable(!(17)))).

% Ai(oscil(MAPK~{p1}))
ctl('Ai'(oscil(17))).

% Ei(reachable(MAPK~{p1}-MEK~{p1,p2}))
ctl('Ei'(reachable(18))).

% Ei(reachable(!(MAPK~{p1}-MEK~{p1,p2})))
ctl('Ei'(reachable(!(18)))).

% Ai(oscil(MAPK~{p1}-MEK~{p1,p2}))
ctl('Ai'(oscil(18))).

% Ai(AG(!(MAPK~{p1}-MEK~{p1,p2})->checkpoint(MEK~{p1,p2},MAPK~{p1}-MEK~{p1,p2})))
ctl('Ai'('AG'(->(!(18),checkpoint(13,18))))).

% Ai(AG(!(MAPK~{p1}-MEK~{p1,p2})->checkpoint(MAPK~{p1},MAPK~{p1}-MEK~{p1,p2})))
ctl('Ai'('AG'(->(!(18),checkpoint(17,18))))).

% Ei(reachable(MAPKPH))
ctl('Ei'(reachable(19))).

% Ei(reachable(!(MAPKPH)))
ctl('Ei'(reachable(!(19)))).

% Ai(oscil(MAPKPH))
ctl('Ai'(oscil(19))).

% Ei(reachable(MAPKPH-MAPK~{p1}))
ctl('Ei'(reachable(20))).

% Ei(reachable(!(MAPKPH-MAPK~{p1})))
ctl('Ei'(reachable(!(20)))).

% Ai(oscil(MAPKPH-MAPK~{p1}))
ctl('Ai'(oscil(20))).

% Ai(AG(!(MAPKPH-MAPK~{p1})->checkpoint(MAPKPH,MAPKPH-MAPK~{p1})))
ctl('Ai'('AG'(->(!(20),checkpoint(19,20))))).

% Ai(AG(!(MAPKPH-MAPK~{p1})->checkpoint(MAPK~{p1},MAPKPH-MAPK~{p1})))
ctl('Ai'('AG'(->(!(20),checkpoint(17,20))))).

% Ei(reachable(MAPK~{p1,p2}))
ctl('Ei'(reachable(21))).

% Ei(reachable(!(MAPK~{p1,p2})))
ctl('Ei'(reachable(!(21)))).

% Ai(oscil(MAPK~{p1,p2}))
ctl('Ai'(oscil(21))).

% Ei(reachable(MAPKPH-MAPK~{p1,p2}))
ctl('Ei'(reachable(22))).

% Ei(reachable(!(MAPKPH-MAPK~{p1,p2})))
ctl('Ei'(reachable(!(22)))).

% Ai(oscil(MAPKPH-MAPK~{p1,p2}))
ctl('Ai'(oscil(22))).

% Ai(AG(!(MAPKPH-MAPK~{p1,p2})->checkpoint(MAPKPH,MAPKPH-MAPK~{p1,p2})))
ctl('Ai'('AG'(->(!(22),checkpoint(19,22))))).

% Ai(AG(!(MAPKPH-MAPK~{p1,p2})->checkpoint(MAPK~{p1,p2},MAPKPH-MAPK~{p1,p2})))
ctl('Ai'('AG'(->(!(22),checkpoint(21,22))))).