%
%
-language(spifcp).
public(wntbind(0.002), lrpbind(0.002)).
public(albind(1.0)).
public(agbind(0.0015)).
public(axinph(0.2), axindph(0.1)).
public(aabind(0.001)).
public(apcph(0.2), apcdph(0.1)).
public(abbind(0.00003), apbbind(0.01)).
public(tcfbind(0.0003)).
public(betaph(5.0)).
public(betadeg1(0.001)).
public(transcription(0.02), axinsyn(0.012)).
public(betasyn(0.423)).
public(wntsyn(10.0)).
public(wntdeg1(0.008)).
System(N1,N2,N3) ::= << %All, Axin
Clock | Syn |
CREATE_FZ(N1) | CREATE_LRP(N1) |
CREATE_Axin(N2) | CREATE_APC(N1) | CREATE_GSK(N1) | CREATE_TCF(N1) .
% CREATE_Beta(N3) .
CREATE_FZ(N) ::= {N =< 0}, true ; {N > 0}, {N--} | Fz | self .
CREATE_LRP(N) ::= {N =< 0}, true ; {N > 0}, {N--} | LRP | self .
CREATE_Axin(N) ::= {N =< 0}, true ; {N > 0}, {N--} | Axin | self .
CREATE_APC(N) ::= {N =< 0}, true ; {N > 0}, {N--} | APC | self .
CREATE_GSK(N) ::= {N =< 0}, true ; {N > 0}, {N--} | Gsk | self .
CREATE_Beta(N) ::= {N =< 0}, true ; {N > 0}, {N--} | Beta | self .
CREATE_TCF(N) ::= {N =< 0}, true ; {N > 0}, {N--} | TCF | self >> .
%Wnt
Wnt ::= << wntrel(0.1), wntdeg(0.008), internal(0.008), lrprel(0.1), lrprem(infinite), alrel(0.000000001), axinrem(infinite), axindeg(infinite) .
wntbind ! {wntrel, wntdeg, internal}, WntFz ;
wntdeg1 ! [], true .
WntFz ::= lrpbind ! {lrprel, lrprem}, WntFzLRP ;
wntrel ? [], Wnt ;
wntdeg ! [], true .
WntFzLRP ::= albind ! {alrel, axinrem, axindeg}, WntFzLRPAxinGsk ;
lrprel ? [], WntFz ;
wntdeg ! [], lrprem ! [], true .
WntFzLRPAxinGsk ::= alrel ? [], WntFzLRP ;
wntrel ? [], lrprem ! [], axinrem ! [], Wnt ;
wntdeg ! [], lrprem ! [], axinrem ! [], true ;
internal ! [], lrprem ! [], axindeg ! [], Wnt >> .
%Fz
Fz ::= << wntrel(0.1), wntdeg(0.008), internal(0.008) .
wntbind ? {wntrel, wntdeg, internal}, FzBound .
FzBound ::= wntrel ! [], Fz ;
wntdeg ? [], Fz ;
internal ? [], Fz >> .
%LRP
%is activated by Wnt and recruits Axin leading to its deactivation and degradation
LRP ::= << lrprel(0.1), lrprem(infinite) .
lrpbind ? {lrprel, lrprem}, LRPBound .
LRPBound ::= lrprel ! [], LRP ;
lrprem ? [], LRP >> .
%GSK
Gsk ::= << agrel(0.1), apgrel(0.01), gskrem(infinite) .
agbind ! {agrel, apgrel, gskrem}, GskBound .
GskBound ::= agrel ? [], Gsk ;
apgrel ? [], Gsk ;
gskrem ? [], Gsk >> .
%Phosphorylated Axin binds APC (fast) or beta-catenin (slow)
%Axin
Axin ::= << phmsg(infinite), dphmsg(infinite), degmsg(0.00167), degpmsg(0.00167), degimsg(infinite), agrel(0.1), apgrel(0.01), gskrem(infinite), alrel(0.000000001), wntrem(infinite), wntdeg(infinite), aarel(0.1), apcrem(infinite) .
Axin_GskBinding | Axin_APCBinding .
Axin_GskBinding ::= agbind ? {agrel, apgrel, gskrem}, Axin_GskBound ;
dphmsg ! [], Axin_GskBinding ;
degmsg ! [], true .
AxinP_GskBinding ::= axindph ! [], Axin_GskBinding ;
phmsg ! [], AxinP_GskBinding .
Axin_GskBound ::= axinph ! [], AxinP_GskBound ;
albind ? {alrel, wntrem, wntdeg}, Axin_WntGskBound ;
agrel ! [], Axin_GskBinding ;
dphmsg ! [], Axin_GskBound .
AxinP_GskBound ::= apgrel ! [], AxinP_GskBinding ;
albind ? {alrel, wntrem, wntdeg}, AxinP_WntGskBound ;
degpmsg ! [], gskrem ! [], true ;
phmsg ! [], AxinP_GskBound .
Axin_WntGskBound ::=
alrel ! [], Axin_GskBound ;
wntrem ? [], Axin_GskBound ;
wntdeg ? [], gskrem ! [], degimsg ! [], true ;
dphmsg ! [], Axin_WntGskBound .
AxinP_WntGskBound ::=
alrel ! [], AxinP_GskBound ;
wntrem ? [], AxinP_GskBound ;
wntdeg ? [], gskrem ! [], degimsg ! [], true ;
phmsg ! [], AxinP_WntGskBound .
Axin_APCBinding ::= phmsg ? [], AxinP_APCBinding ;
degmsg ? [], true ;
degimsg ? [], true .
AxinP_APCBinding ::= aabind ? {aarel, apcrem}, AxinP_APCBound ;
degimsg ? [], true ;
dphmsg ? [], Axin_APCBinding .
Axin_APCBound ::= aarel ! [], Axin_APCBinding ;
degpmsg ? [], apcrem ! [], true ;
degimsg ? [], apcrem ! [], true ;
phmsg ? [], AxinP_APCBound .
AxinP_APCBound ::= aarel ! [], AxinP_APCBinding ;
degpmsg ? [], apcrem ! [], true ;
degimsg ? [], apcrem ! [], true ;
dphmsg ? [], Axin_APCBound >> .
%APC
APC ::= << phmsg(infinite), dphmsg(infinite), aarel(0.1), apcrem(infinite), abrel(0.1), betadeg(0.001), betapdeg(5.0) .
APC_AxinBinding | APC_BetaBinding .
APC_AxinBinding ::= aabind ! {aarel, apcrem}, APC_AxinBound ;
dphmsg ! [], APC_AxinBinding .
APCP_AxinBinding ::= apcdph ! [], APC_AxinBinding ;
phmsg ! [], APCP_AxinBinding .
APC_AxinBound ::= apcph ! [], APCP_AxinBound ;
aarel ? [], APC_AxinBinding ;
apcrem ? [], APC_AxinBinding ;
dphmsg ! [], APC_AxinBound .
APCP_AxinBound ::= apcdph ! [], APC_AxinBound ;
apcrem ? [], APCP_AxinBinding ;
phmsg ! [], APCP_AxinBound .
APC_BetaBinding ::= abbind ! {abrel, betadeg, betapdeg}, APC_BetaBound ;
phmsg ? [], APCP_BetaBinding .
APCP_BetaBinding ::= apbbind ! {abrel, betadeg, betapdeg}, APCP_BetaBound ;
dphmsg ? [], APC_BetaBinding .
APC_BetaBound ::= abrel ? [], APC_BetaBinding ;
betadeg ? [], APC_BetaBinding ;
phmsg ? [], APCP_BetaBound .
APCP_BetaBound ::= betaph ! [], APCP_BetaPBound ;
abrel ? [], APCP_BetaBinding ;
betadeg ? [], APCP_BetaBinding ;
dphmsg ? [], APC_BetaBound .
APCP_BetaPBound ::= betapdeg ? [], APCP_BetaBinding >> .
%Beta
Beta ::= << tcfrel(0.01), betadeg(0.001), abrel(0.1), betapdeg(5.0) .
tcfbind ? {tcfrel, betadeg}, Beta_TCFBound ;
abbind ? {abrel, betadeg, betapdeg}, Beta_APCBound ;
apbbind ? {abrel, betadeg, betapdeg}, Beta_APCBound ;
betadeg1 ! [], true .
Beta_TCFBound ::= tcfrel ! [], Beta ;
betadeg ! [], true .
Beta_APCBound ::= abrel ! [], Beta ;
betadeg ! [], true ;
betapdeg ! [], true >> .
%TCF
TCF ::= << tcfrel(0.01), betadeg(0.001) .
tcfbind ! {tcfrel, betadeg}, TCFBound .
TCFBound ::= tcfrel ? [], TCF ;
betadeg ? [], TCF ;
transcription ! [], TCFTrans .
TCFTrans ::= axinsyn ! [], (TCFTrans | Axin) ;
tcfrel ? [], TCF ;
betadeg ? [], TCF >> .
Syn ::= betasyn ! [], (Beta | Syn) ;
wntsyn ! [], (Wnt | Syn) .
Clock ::= wntdeg1 ? [], Clock ;
axinph ? [], Clock ;
axindph ? [], Clock ;
apcph ? [], Clock ;
apcdph ? [], Clock ;
betaph ? [], Clock ;
betadeg1 ? [], Clock ;
transcription ? [], Clock ;
axinsyn ? [], Clock ;
betasyn ? [], Clock ;
wntsyn ? [], Clock .
%
%