% %
-language(spifcp).
-include(fgfrates). %rates file

public(fb(FGFBind), frb(FRSBind), sb(SRCBind), grb(GRBBind), srb(SPRYBind), shb(SHPBind), pb(PLCBind), cb(CBLBind), sosb(SOSBind), gsb(GSBind), ph653(FGFRPh1), ph766(FGFRPh2), phFRS(FRSPh), phSpry(SPRYPh), dph4(FRSDph), create_spry(SPRYIn), dph196(FRSDph), dph306(FRSDph), dph471(FRSDph)). 

System(N1,N2,N3) ::= << 
	CREATE_FGFR(N1) | CREATE_FGF(N2) | CREATE_FRS(N3) | CREATE_SRC(N1) | CREATE_SHP(N1) |
	CREATE_GRB(N1)  | CREATE_PLC(N1) | CREATE_CBL(N1) | CREATE_SOS(N1) | CREATE_DSPRY(N1) | Clock .

CREATE_FGF(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | FGF  | self .
CREATE_FGFR(N) ::= {N =< 0}, true ; {N > 0}, {N--} | FGFR | self .
CREATE_FRS(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | FRS2 | self .
CREATE_SRC(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | Src  | self .
CREATE_GRB(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | Grb2 | self .
CREATE_SHP(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | Shp  | self .
CREATE_DSPRY(N) ::= {N =< 0}, true ; {N > 0}, {N--} | Spry | Dself(N) .
Dself(N) ::= create_spry ! [], CREATE_DSPRY(N) .
CREATE_CBL(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | Cbl  | self .
CREATE_PLC(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | Plc  | self .
CREATE_SOS(N)  ::= {N =< 0}, true ; {N > 0}, {N--} | Sos  | self >> .

%FGF graphical representation
FGF ::= << f(FGFUn), remFgf(infinite), degFgf(infinite) .		%private channels
	fb ? {f, remFgf, degFgf}, FGF_Bound .				%binding to the receptor

FGF_Bound ::= f ! [], FGF ;						%dissociation from FGFR 
	remFgf ? [], FGF ; 						%immediate dissociation
	degFgf ? [], true >> . 						%degradation


%FGFR graphical representation
FGFR ::= << f(FGFUn), fr(FRSUn), p(PLCUn), degPlc(PLCDeg), degPlcInf(infinite), pre653(infinite), preFRS1(10000), preFRS2(10000), pre766(infinite), remFgfr(infinite), remFrs(infinite), degFrs(infinite), remFgf(infinite), degFgf(infinite), degFGFR10(infinite), degFGFR11(infinite), degFGFR12(infinite), degFGFR20(infinite), degFGFR22(infinite), degFGFR23(infinite), degFGFR14(infinite), degFGFR24(infinite) .
%the rates of phosphorylation notification messages are not infinite because of the memory error in the BioSPI implementation

	FGFR_Ligand_Binding | FGFR_FRS2_Binding | FGFR_653 | FGFR_766 . %four independent domains (activities) 

FGFR_Ligand_Binding ::= fb ! {f, remFgf, degFgf}, FGFR_Ligand_Bound ;	%binding to FGF, allow phosphorylation of res 653 
		degFGFR10 ? [], true;					%requested degradation
		degFGFR20 ? [], true .					%requested degradation
FGFR_Ligand_Bound ::= f ? [], FGFR_Ligand_Binding ;			%dissociation from FGF
		pre653 ! [], FGFR_Ligand_Bound ;			%while bound, allow phosphorylation of res 653
		degFGFR10 ? [], remFgf ! [], true ;			%requested degradation, remove FGF
		degFGFR20 ? [], degFgf ! [], true .   			%requested degradation, pass to FGF

FGFR_FRS2_Binding ::= 
		frb ! {fr, preFRS2, remFrs, degFrs, remFgfr}, FGFR_FRS2_Bound ;	%binding to FRS2 
		degFGFR11 ? [], true . 						%requested degradation
FGFR_FRS2_Bound ::= 
		fr ? [], FGFR_FRS2_Binding ; 					%FRS2 dissociation
		preFRS1 ? [], FGFR_FRS2_BoundP ;
		remFrs ? [], FGFR_FRS2_Binding ;
		degFrs ? [], degFGFR20 ! [], degFGFR22 ! [], degFGFR23 ! [], true ; %remove FGFR together with all bound partners 
		degFGFR11 ? [], remFgfr ! [], true .
FGFR_FRS2_BoundP ::=
		preFRS2 ! [], FGFR_FRS2_BoundP ; 
		fr ? [], FGFR_FRS2_Binding ; 
		remFrs ? [], FGFR_FRS2_Binding ;
		degFrs ? [], degFGFR20 ! [], degFGFR22 ! [], degFGFR23 ! [], true; 
		degFGFR11 ? [], remFgfr ! [], true .
 
FGFR_653 ::= pre653 ? [], (ph653 ! [], FGFR_653P ;			%phosphorylate, once condition pre653 is satisfied 
			degFGFR12 ? [], true ;
			degFGFR22 ? [], true ) ;
		degFGFR12 ? [], true ;
		degFGFR22 ? [], true .
FGFR_653P ::= 
		preFRS1 ! [], FGFR_653P ; 				%allow phosphorylation of FRS2 if bound 
		pre766 ! [], FGFR_653P ; 				%allow phosphorylation of res 766
		degFGFR12 ? [], true ;
		degFGFR22 ? [], true .

FGFR_766 ::= pre766 ? [], (ph766 ! [], FGFR_766P ; degFGFR23 ? [], true ) ;
		degFGFR23 ? [], true .
FGFR_766P ::= pb ! {p, degPlc, degPlcInf}, FGFR_Plc_Bound ; 		%bind Plc if phosphorylated
		degFGFR23 ? [], true .
FGFR_Plc_Bound ::= p ? [], FGFR_766P ; 
		degPlc ? [], ( degFGFR10 ! [], degFGFR11 ! [], degFGFR12 ! [], true ; degFGFR23 ? [], true ) ; %remove FGFR but leave all bound partners
		degFGFR23 ? [], degPlcInf ! [], true >> . 


%FRS2 graphical representation
FRS2 ::= << s(SRCUn), fr(FRSUn), degSrc(SRCDeg), remFrs(infinite), degFrs(infinite), remFgfr(infinite), remSrc(infinite), degCbl3(infinite), remShp(infinite), degShp(infinite), remGrb(infinite), degGrb(infinite), gr(GRBUn), sh(SHPUn), pre196(infinite), pre306(infinite), pre471(infinite), preFRS2(10000), preFRS3(10000), post196(infinite), post306(infinite), degFRS11(infinite), degFRS12(infinite), degFRS13(infinite), degFRS20(infinite), degFRS22(infinite), degFRS23(infinite) .  

	FRS2_FBinding | FRS2_196 | FRS2_306 | FRS2_471 . 		%four independent domains

FRS2_FBinding ::= 
	frb ? {fr, preFRS2, remFrs, degFrs, remFgfr}, FRS2_FBound ; 	%FGF binding site
	degFRS20 ? [], true ;
	degCbl3 ? [], degFRS12 ! [], degFRS11 ! [], degFRS13 ! [], true .
FRS2_FBound ::= preFRS2 ? [], FRS2_FBoundP ;
	fr ! [], FRS2_FBinding ;
	remFgfr ? [], FRS2_FBinding ; 
	degCbl3 ? [], degFRS12 ! [], degFRS11 ! [], degFRS13 ! [], remFrs ! [], true ;
	degFRS20 ? [], (degFrs ! [], true ; remFgfr ? [], true) .
FRS2_FBoundP ::= fr ! [], FRS2_FBinding ; 				%no subsequent dephosphorylation of 196, 306, 471
	remFgfr ? [], FRS2_FBinding ; 
	degCbl3 ? [], degFRS12 ! [], degFRS11 ! [], degFRS13 ! [], remFrs ! [], true ;
	degFRS20 ? [], (degFrs ! [], true ;  remFgfr ? [], true) ;
	preFRS3 ! [], FRS2_FBoundP . 					%allow phosphorylation of res 196, 306, 471 whenever bound

FRS2_196 ::= preFRS3 ? [], (phFRS ! [], FRS2_196P; 			%Src binding site, precondition for phosphorylation
		post196 ? [], FRS2_196 ;
		degFRS11 ? [], true ) ;
	post196 ? [], FRS2_196 ;
	degFRS11 ? [], true .
FRS2_196P ::= sb ! {s, degCbl3, remSrc, degSrc}, FRS2_Src_Bound ;
	post196 ? [], FRS2_196 ;
	degFRS11 ? [], true . 
FRS2_Src_Bound ::= s ? [], FRS2_196P ;
	degSrc ! [], ( degFRS20 ! [], degFRS22 ! [], degFRS23 ! [], true ; %degrade together with all bound partners
		degFRS11 ? [], true ) ;
	post196 ? [], remSrc ! [], FRS2_196 ;
	degFRS11 ? [], true .

FRS2_306 ::= preFRS3 ? [], (phFRS ! [], FRS2_306P ;			%Grb binding site 
		post306 ? [], FRS2_306 ; degFRS12 ? [], true ; 
		degFRS22 ? [], true) ;
	post306 ? [], FRS2_306 ; 
	degFRS12 ? [], true ;
	degFRS22 ? [], true .
FRS2_306P ::= grb ! {gr, remGrb, degGrb}, FRS2_Grb_Bound ;
	post306 ? [], FRS2_306 ; 
	degFRS12 ? [], true ;
	degFRS22 ? [], true .
FRS2_Grb_Bound ::= gr ? [], FRS2_306P ; 
	post306 ? [], remGrb ! [], FRS2_306 ;
	degFRS12 ? [], remGrb ! [], true ; 
	degFRS22 ? [], degGrb ! [], true . 

FRS2_471 ::= preFRS3 ? [], (phFRS ! [], FRS2_471P ;			%Shp binding site
		degFRS13 ? [], true ;
		degFRS23 ? [], true) ;
	degFRS13 ? [], true ;
	degFRS23 ? [], true .
FRS2_471P ::= shb ! {sh, remShp, degShp}, FRS2_Shp_Bound ; 
	degFRS13 ? [], true ;
	degFRS23 ? [], true .
FRS2_Shp_Bound ::= sh ? [], FRS2_471P ; 				%Shp dissociation
	dph196 ! [], post196 ! [], FRS2_Shp_Bound ; 			%dephosphorylation of res 196
	dph306 ! [], post306 ! [], FRS2_Shp_Bound ; 			%dephosphorylation of res 306
	dph471 ! [], remShp ! [], FRS2_471 ; 				%dephosphorylation of res 471
	degFRS13 ? [], remShp ! [], true ; 				%request for degradation
	degFRS23 ? [], degShp ! [], true >> . 				%request for degradation


%Src graphical representation
Src ::= << degCbl3(infinite), degCbl2(infinite), cbl3(infinite), degSpry(infinite), sr(SPRYUn), srp(SPRYPUn), remSpry(infinite), s(SRCUn), remSrc(infinite), degSrc(SRCDeg). 
	
	Src_FBinding | Src_SBinding . 					%independent FRS2 and Spry binding sites

Src_FBinding ::= 
	sb ? {s, degCbl3, remSrc, degSrc}, Src_FBound ; 		%Src binding
	cbl3 ? [], Src_FBinding .
Src_FBound ::= s ! [], Src_FBinding ; 
	remSrc ? [], Src_FBinding ;
	degSrc ? [], degSpry ! [], true ; 		
	cbl3 ? [], ( degCbl3 ! [], Src_FBinding ;
		 remSrc ? [], Src_FBinding ;
		 degSrc ? [], degSpry ! [], true ) .

Src_SBinding ::= srb ! {sr, srp, remSpry, degCbl2},  Src_SBound ;
	degSpry ? [], true .
Src_SBound ::= sr ? [], Src_SBinding ;
	srp ? [], Src_SBinding ;
	degSpry ? [], remSpry ! [], true ; 
	degCbl2 ? [], cbl3 ! [], Src_SBound >> .


%Spry graphical representation
Spry ::= << c(CBLUn), sr(SPRYUn), srp(SPRYPUn), remSpry(infinite), gs(GSUn), degSpry(infinite), degGrb(infinite), degCbl(infinite), degCbl2(infinite), degCbl1(CBLDeg), remGrb(infinite), remCbl(infinite), spryp(infinite), dspryp(infinite) . 

	Spry_SBinding | Spry_CBinding | Spry_GBinding . 		%independent binding to Src, Cbl and Grb

Spry_GBinding ::= spryp ? [], SpryP_GBinding ; 				%can bind Grb after being phosphorylated 
	degSpry ? [], true .
SpryP_GBinding ::= gsb ! {gs, remGrb, degGrb}, SpryP_GBound ; 
	dspryp ? [], Spry_GBinding ; 
	degSpry ? [], true .
SpryP_GBound ::= gs ? [], SpryP_GBinding ; 
	dspryp ? [], ( remGrb ! [], Spry_GBinding ; 
		      degSpry ? [], degGrb ! [], true) ;
	degSpry ? [], degGrb ! [], true .

Spry_CBinding ::= spryp ? [], SpryP_CBinding ; 				%can bind Cbl after being phosphorylated 
	degSpry ? [], true .
SpryP_CBinding ::= cb ! {c, remCbl, degCbl1, degCbl}, SpryP_CBound ; 
	dspryp ? [], Spry_CBinding ; 
	degSpry ? [], true .
SpryP_CBound ::= c ? [], SpryP_CBinding ;
	dspryp ? [], ( remCbl ! [], Spry_CBinding ; 
		      degSpry ? [], degCbl ! [], true) ;
	degSpry ? [], degCbl ! [],  true .

Spry_SBinding ::= srb ? {sr, srp, remSpry, degCbl2}, Spry_SBound ;
	dspryp ! [], Spry_SBinding .
Spry_SBound ::= phSpry ! [], SpryP_SBound ;
	sr ! [], Spry_SBinding ;
	remSpry ? [], degSpry ! [], degSpry ! [], true ; 
	dspryp ! [], Spry_SBound .
SpryP_SBound ::= 
	srp ! [], SpryP_SBinding ;
	remSpry ? [], degSpry ! [], degSpry ! [], true ; 
	degCbl1 ? [], ( degCbl2 ! [], SpryP_SBound ; 
			remSpry ? [], degSpry ! [], degSpry ! [], true) ;
	spryp ! [], SpryP_SBound .
SpryP_SBinding ::= srb ? {sr, srp, remSpry, degCbl2}, SpryP_SBound ;
	degCbl1 ? [], SpryP_SBinding ;
	spryp ! [], SpryP_SBinding >> .


%Cbl graphical representation
Cbl ::= << degCbl1(CBLDeg), c(CBLUn), remCbl(infinite), degCbl(infinite) . 
	cb ? {c, remCbl, degCbl1, degCbl}, Cbl_Bound .
Cbl_Bound ::= c ! [], Cbl ; 
	remCbl ? [], Cbl ;
	degCbl ? [], true ;  
	degCbl1 ! [], Cbl_Bound >> .


%Grb2 graphical representation
Grb2 ::= << gr(GRBUn), gs(GSUn), remGrb(infinite), degGrb(infinite), sos(SOSUn), remSos(infinite), degSos(infinite) .
	grb ? {gr, remGrb, degGrb}, Grb2_FBound ;
	gsb ? {gs, remGrb, degGrb}, Grb2_Spry_Bound .

Grb2_FBound ::= sosb ! {sos, remSos, degSos}, Grb2_FSBound ;
	gr ! [], Grb2 ; 
	remGrb ? [], Grb2 ;
	degGrb ? [], true . 				
Grb2_FSBound ::= sos ? [], Grb2_FBound ;
	gr ! [], remSos ! [], Grb2 ;
	remGrb ? [], remSos ! [], Grb2 ;
	degGrb ? [], degSos ! [], true . 

Grb2_Spry_Bound ::= gs ! [], Grb2 ;
	degGrb ? [], true ; 						%request for degradation
	remGrb ? [], Grb2 >> .


%Sos graphical representation
Sos ::= << sos(SOSUn), remSos(infinite), degSos(infinite) . 
	sosb ? {sos, remSos, degSos}, Sos_Bound .
Sos_Bound ::= sos ! [], Sos ;
	degSos ? [], true ; 
	remSos ? [], Sos >> .


%Shp graphical representation
Shp ::= << sh(SHPUn), remShp(infinite), degShp(infinite) . 
	shb ? {sh, remShp, degShp}, Shp_FBound .

Shp_FBound ::= sh ! [], Shp ;
	remShp ? [], Shp; 
	degShp ? [], true >> . 


%Plc graphical representation
Plc ::= << p(PLCUn), degPlc(PLCDeg), degPlcInf(infinite). 
	pb ? {p, degPlc, degPlcInf}, Plc_Bound.
Plc_Bound ::= p ! [], Plc; degPlc ! [], true ; degPlcInf ? [], true >>.


Clock ::=
	ph653 ? [], Clock ; 
	ph766 ? [], Clock ;
	phFRS ? [], Clock ;
	phSpry ? [], Clock ;
	dph196 ? [], Clock ;
	dph306 ? [], Clock ;
	dph471 ? [], Clock ; 
	create_spry ? [], Clock .

%
%