Edinburgh/DivisionPopper/Modelling/Edinburgh/PRISMCode

From 2007.igem.org

Latest revision as of 17:04, 4 October 2007

This is the [http://www.prismmodelchecker.org/ 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

// maximal number of YFP molecules in the model

const int maxYFP=500;

// maximal number of GFP molecules in the model

const int maxGFP=500;

// reate for the forward phase duration const double forwardPhaseRate =0.0001;

// rate for the backward phase duration const double backwardPhaseRate =0.0001;

// rate for the flipping phase duartion const double flipPhaseRate =0.0001;

// rate of YPF expression

const double expYFP =0.1;

//rate of the GFP expression

const double expGFP =0.1;

// rate of the YFP degradation

const double degYFP =0.001;

// rate of he GFP degradation

const double degGFP =0.001;

//module representing YFP molecules and actions

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 representing GFP molecules and actions

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 representing the Phases' state

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