From 2007.igem.org

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.

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