Edinburgh/DivisionPopper/Modelling/Edinburgh/PRISMCode
From 2007.igem.org
Luca.Gerosa (Talk | contribs) |
Luca.Gerosa (Talk | contribs) (→The PRISM Code) |
||
Line 3: | Line 3: | ||
== The PRISM Code == | == The PRISM Code == | ||
- | ctmc | + | ''ctmc'' |
const int maxYFP=500; | const int maxYFP=500; | ||
+ | |||
const int maxGFP=500; | const int maxGFP=500; | ||
const double forwardPhaseRate =0.0001; | const double forwardPhaseRate =0.0001; | ||
+ | |||
const double backwardPhaseRate =0.0001; | const double backwardPhaseRate =0.0001; | ||
+ | |||
const double flipPhaseRate =0.0001; | const double flipPhaseRate =0.0001; | ||
const double expYFP =0.1; | const double expYFP =0.1; | ||
+ | |||
const double expGFP =0.1; | const double expGFP =0.1; | ||
const double degYFP =0.001; | const double degYFP =0.001; | ||
+ | |||
const double degGFP =0.001; | const double degGFP =0.001; | ||
- | module YFP | + | ''module YFP'' |
levelYFP:[0..maxYFP] init 0; | levelYFP:[0..maxYFP] init 0; | ||
+ | |||
[degYFP] (levelYFP>0) -> degYFP * levelYFP : levelYFP' = levelYFP-1; | [degYFP] (levelYFP>0) -> degYFP * levelYFP : levelYFP' = levelYFP-1; | ||
+ | |||
[expYFP] (phase=0)&(levelYFP<maxYFP) -> expYFP : levelYFP' = levelYFP+1; | [expYFP] (phase=0)&(levelYFP<maxYFP) -> expYFP : levelYFP' = levelYFP+1; | ||
- | endmodule | + | ''endmodule'' |
- | module GFP | + | ''module GFP'' |
levelGFP:[0..maxGFP] init 0; | levelGFP:[0..maxGFP] init 0; | ||
+ | |||
[degGFP] (levelGFP>0)-> degGFP * levelGFP : levelGFP'=levelGFP-1; | [degGFP] (levelGFP>0)-> degGFP * levelGFP : levelGFP'=levelGFP-1; | ||
+ | |||
[expGFP] (phase=2)&(levelGFP<maxGFP) -> expGFP : levelGFP'=levelGFP+1; | [expGFP] (phase=2)&(levelGFP<maxGFP) -> expGFP : levelGFP'=levelGFP+1; | ||
- | endmodule | + | ''endmodule'' |
- | module Phase | + | |
+ | ''module Phase'' | ||
phase:[0..3] init 0; | phase:[0..3] init 0; | ||
+ | |||
[changeFromForwardToFlip] (phase=0) -> forwardPhaseRate : phase'=1; | [changeFromForwardToFlip] (phase=0) -> forwardPhaseRate : phase'=1; | ||
+ | |||
[changeFromBackwardToFlip] (phase=2) -> backwardPhaseRate : phase'=3; | [changeFromBackwardToFlip] (phase=2) -> backwardPhaseRate : phase'=3; | ||
+ | |||
[changeFromFlipToForward] (phase=3) -> flipPhaseRate : phase'= 0; | [changeFromFlipToForward] (phase=3) -> flipPhaseRate : phase'= 0; | ||
- | |||
- | endmodule | + | [changeFromFlipToBackward] (phase=1) -> flipPhaseRate : phase'= 2; |
+ | '' | ||
+ | endmodule'' |
Revision as of 13:04, 27 September 2007
This is the PRISM code we developed for simulation and model checking of the stochastic model. It is a implementation of the Underlying Markov Chain of the Process Algebra model reported in the Modelling section.
The PRISM Code
ctmc
const int maxYFP=500;
const int maxGFP=500;
const double forwardPhaseRate =0.0001;
const double backwardPhaseRate =0.0001;
const double flipPhaseRate =0.0001;
const double expYFP =0.1;
const double expGFP =0.1;
const double degYFP =0.001;
const double degGFP =0.001;
module YFP
levelYFP:[0..maxYFP] init 0;
[degYFP] (levelYFP>0) -> degYFP * levelYFP : levelYFP' = levelYFP-1;
[expYFP] (phase=0)&(levelYFP<maxYFP) -> expYFP : levelYFP' = levelYFP+1;
endmodule
module GFP
levelGFP:[0..maxGFP] init 0;
[degGFP] (levelGFP>0)-> degGFP * levelGFP : levelGFP'=levelGFP-1;
[expGFP] (phase=2)&(levelGFP<maxGFP) -> expGFP : levelGFP'=levelGFP+1;
endmodule
module Phase
phase:[0..3] init 0;
[changeFromForwardToFlip] (phase=0) -> forwardPhaseRate : phase'=1;
[changeFromBackwardToFlip] (phase=2) -> backwardPhaseRate : phase'=3;
[changeFromFlipToForward] (phase=3) -> flipPhaseRate : phase'= 0;
[changeFromFlipToBackward] (phase=1) -> flipPhaseRate : phase'= 2; endmodule