% %
-language(biospi).

FAST=>1000.0.
SLOW=>60.0.

public(bind(0.01), rel(0.1), deg(5.0), rbind(1.0), rrel(0.008), internal(0.008), phos(0.2), dephos(0.1), asyn(0.012), adeg(0.00167), bsyn(0.423), bdeg(0.001), rdeg(0.005)).
public(molcycle(0.0001), moldiff(0.00001), scycle(0.0014), dcycle(0.0014), sdie(0.0001), ddie(0.0005), die(SLOW), parent(infinite)) .
public(c1(infinite), c2(infinite), count(FAST), breakAB(infinite), breakRA(infinite), celldeg(infinite)).
public(one(15),two(30),three(50),four(100),five(50),six(30),seven(10),eight(1),nine(1),ten(0),nil(1),init(infinite),initQ(infinite)).

System ::= << move(infinite), next(infinite) .
        cell(<>) | 
	cell(<>) | 
	Lattice | Clock | Counter >> .

Axin10 ::= mol(<>) | mol(<>) | mol(<>) | mol(<>) | mol(<>) |
	mol(<>) | mol(<>) | mol(<>) | mol(<>) | mol(<>) .  

CellClock ::= p2c phos ? [], CellClock ;
	p2c dephos ? [], CellClock ;
	p2c asyn ? [], CellClock ;
	p2c adeg ? [], CellClock ;
	p2c bdeg ? [], CellClock ;
	p2c rdeg ? [], CellClock ;
	local bsyn ? [], CellClock .

CellSyn ::= local bsyn ! [], (CellSyn | mol(<>)) .

Rec ::= merge+ rbind, RecA ;
	c2p rdeg ! [], true ;
	c2p celldeg ? [], true .
RecA ::= local rrel ? [], expel breakRA, Rec ;
	local internal ? [], Rec ;
	local rdeg ! [], true ;
	c2p celldeg ? [], true .

Axin ::= c2p phos ! [], AxinP ;
	c2p adeg ! [], true ;
	c2p celldeg ? [], true .
AxinP ::= merge- bind, AxinP_Beta ;
	merge- rbind, AxinP_Rec ;
	c2p dephos ! [], Axin ;
	c2p adeg ! [], true ;
	c2p celldeg ? [], true .
AxinP_Beta ::= local rel ! [], mol(<>) ;
	local deg ! [], AxinP ;
	local bdeg ? [], AxinP ;
	local adeg ! [], true ;
	c2p celldeg ? [], true .
AxinP_Rec ::= local rrel ! [], mol(<>) ;
	local internal ! [], true ;
	local rdeg ? [], AxinP ;
	c2p celldeg ? [], true .

Beta ::= merge+ bind, BetaA ;
	c2p asyn ! [], (Beta | mol(<>)) ;
	c2p bdeg ! [], true ;
	c2p molcycle ! [], Beta ;
	c2p moldiff ! [], Beta ;
	c2p celldeg ? [], true .

BetaA ::= local rel ? [], expel breakAB, Beta ;
	local deg ? [], true ;
	local bdeg ! [], true ;
	local adeg ? [], Beta ;
	c2p celldeg ? [], true .

%Stem cell: divides producing two stem cells
SCell(pos,move,next) ::= << next1(infinite), mol(infinite) .
        << next=?=nil,
                ( c2p pos ! [], SDiffuse ;
                  s2s move ! {pos, next1}, SMoveNil ;
                  p2c molcycle ? [], SCycleNil(pos, move, next) ;
		  p2c moldiff ? [], DCell(pos, move, next) ;
                  c2p sdie ! [], SDie ) ;
           otherwise,
                ( c2p pos ! [], SDiffuse ;
                  s2s move ! {pos, next}, SMove ;
                  p2c molcycle ? [], SCycle(pos, move, next) ;
		  p2c moldiff ? [], DCell(pos, move, next) ;
                  c2p sdie ! [], SDie ) >> .

SDiffuse ::= SCell(pos,move,next) | mol(<>) .

SMoveNil ::= c2p initQ ! {pos}, c2p init ? {posNext}, SCell(posNext,next1,nil) .%| Counter .
SMove ::= s2s next ? {posNext, nextNext}, SCell(posNext,next,nextNext) .%| Counter .

SCycleNil(pos, move, next) ::= c2p scycle ! {pos,move,next1}, SDivideNil ;
		c2p pos ! [], SCycleNilDiffuse ;
		s2s move ! {pos, next1}, SCycleNilMove .
SDivideNil ::= c2p initQ ! {pos}, c2p init ? {posNext}, c2p count ! [], SCell(posNext,next1,nil) .
SCycleNilDiffuse ::= SCycleNil(pos, move, next) | mol(<>) .
SCycleNilMove ::= c2p initQ ! {pos}, c2p init ? {posNext}, SCycleNil(posNext, next1, nil).

SCycle(pos, move, next) ::= c2p scycle ! {pos,move,next}, SDivide ;
		c2p pos ! [], SCycleDiffuse ;
		s2s move ! {pos, next}, SCycleMove.
SDivide ::= s2s next ? {posNext, nextNext}, c2p count ! [], SCell(posNext,next,nextNext) .
SCycleDiffuse ::= SCycle(pos, move, next) | mol(<>) .
SCycleMove ::= s2s next ? {posNext, nextNext}, SCycle(posNext, next, nextNext) .

SDie ::= p2c celldeg ! [], SDie ; 
	c2p die ! [], SDead .
SDead ::= s2s move ! {pos, next}, true >> .


%Differentiated cell: divides producing two differentiated cell, has limited lifespan
DCell(pos,move,next) ::= << next1(infinite), mol(infinite) .
        << next=?=nil,
                ( c2p pos ! [], DDiffuse ;
                  s2s move ! {pos, next1}, DMoveNil ;
                  p2c molcycle ? [], DCycleNil(pos, move, next) ;
                  c2p ddie ! [], DDie ) ;
           otherwise,
                ( c2p pos ! [], DDiffuse ;
                  s2s move ! {pos, next}, DMove ;
                  p2c molcycle ? [], DCycle(pos, move, next) ;
                  c2p ddie ! [], DDie ) >> .

DDiffuse ::= DCell(pos,move,next) | mol(<>) .

DMoveNil ::= c2p initQ ! {pos}, c2p init ? {posNext}, DCell(posNext,next1,nil) .
DMove ::= s2s next ? {posNext, nextNext}, DCell(posNext,next,nextNext) .

DCycleNil(pos, move, next) ::= c2p dcycle ! {pos,move,next1}, DDivideNil ;
		c2p pos ! [], DCycleNilDiffuse ;
		s2s move ! {pos, next1}, DCycleNilMove .
DDivideNil ::= c2p initQ ! {pos}, c2p init ? {posNext}, c2p count ! [], DCell(posNext,next1,nil) .
DCycleNilDiffuse ::= DCycleNil(pos, move, next) | mol(<>) .
DCycleNilMove ::= c2p initQ ! {pos}, c2p init ? {posNext}, DCycleNil(posNext, next1, nil).

DCycle(pos, move, next) ::= c2p dcycle ! {pos,move,next}, DDivide ;
		c2p pos ! [], DCycleDiffuse ;
		s2s move ! {pos, next}, DCycleMove.
DDivide ::= s2s next ? {posNext, nextNext}, c2p count ! [], DCell(posNext,next,nextNext) .
DCycleDiffuse ::= DCycle(pos, move, next) | mol(<>) .
DCycleMove ::= s2s next ? {posNext, nextNext}, DCycle(posNext, next, nextNext) .

DDie ::= p2c celldeg ! [], DDie ; 
	c2p die ! [], DDead .
DDead ::= s2s move ! {pos, next}, true >> .




Lattice ::= p2c initQ ? {pos}, << pos=?=one, p2c init ! {two}, Lattice ;
                             pos=?=two, p2c init ! {three}, Lattice ;
                             pos=?=three, p2c init ! {four}, Lattice ;
                             pos=?=four, p2c init ! {five}, Lattice ;
                             pos=?=five, p2c init ! {six}, Lattice ;
                             pos=?=six, p2c init ! {seven}, Lattice ;
                             pos=?=seven, p2c init ! {eight}, Lattice ;
                             pos=?=eight, p2c init ! {nine}, Lattice ;
                             pos=?=nine, p2c init ! {ten}, Lattice ;
                             otherwise, p2c init ! {ten}, Lattice >> .




Clock ::= p2c scycle ? {pos,move,next}, Clock | cell(<>) ;
	p2c dcycle ? {pos,move,next}, Clock | cell(<>) ;  
	p2c die ? [], Clock ;
        p2c sdie ? [], Clock ; p2c ddie ? [], Clock ; 
        p2c one ? [], Clock ; p2c two ? [], Clock ; 
	p2c three ? [], Clock ; p2c four ? [], Clock; 
	p2c five ? [], Clock; p2c six ? [], Clock; 
	p2c seven ? [], Clock; p2c eight ? [], Clock; 
	p2c nine ? [], Clock; p2c ten ? [], Clock .



Counter ::= p2c count ? [], Counter | Counter .

%
%