%
%-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 . %