Edinburgh/DivisionPopper/Modelling/Edinburgh/PRISMCode
From 2007.igem.org
Luca.Gerosa (Talk | contribs) (→The PRISM Code) |
Luca.Gerosa (Talk | contribs) |
||
Line 1: | Line 1: | ||
- | 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 [[Edinburgh/DivisionPopper/Modelling|Modelling]] section. | + | 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 [[Edinburgh/DivisionPopper/Modelling|Modelling]] section. |
== The PRISM Code == | == The PRISM Code == | ||
''ctmc'' | ''ctmc'' | ||
+ | |||
+ | // maximal number of YFP molecules in the model | ||
const int maxYFP=500; | const int maxYFP=500; | ||
+ | |||
+ | // maximal number of GFP molecules in the model | ||
const int maxGFP=500; | const int maxGFP=500; | ||
+ | // reate for the forward phase duration | ||
const double forwardPhaseRate =0.0001; | const double forwardPhaseRate =0.0001; | ||
+ | // rate for the backward phase duration | ||
const double backwardPhaseRate =0.0001; | const double backwardPhaseRate =0.0001; | ||
+ | // rate for the flipping phase duartion | ||
const double flipPhaseRate =0.0001; | const double flipPhaseRate =0.0001; | ||
+ | |||
+ | // rate of YPF expression | ||
const double expYFP =0.1; | const double expYFP =0.1; | ||
+ | |||
+ | //rate of the GFP expression | ||
const double expGFP =0.1; | const double expGFP =0.1; | ||
+ | |||
+ | // rate of the YFP degradation | ||
const double degYFP =0.001; | const double degYFP =0.001; | ||
+ | |||
+ | // rate of he GFP degradation | ||
const double degGFP =0.001; | const double degGFP =0.001; | ||
+ | |||
+ | //module representing YFP molecules and actions | ||
''module YFP'' | ''module YFP'' | ||
Line 34: | Line 51: | ||
''endmodule'' | ''endmodule'' | ||
+ | |||
+ | //module representing GFP molecules and actions | ||
''module GFP'' | ''module GFP'' | ||
Line 45: | Line 64: | ||
''endmodule'' | ''endmodule'' | ||
+ | |||
+ | //module representing the Phases' state | ||
''module Phase'' | ''module Phase'' |
Revision as of 13:17, 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
// 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