320 lines
7.7 KiB
Text
320 lines
7.7 KiB
Text
// File generated by SBML-to-PRISM converter
|
|
// Original file: Toggle_10_10.xml
|
|
// @GeneticLogicLab
|
|
|
|
ctmc
|
|
|
|
// const int MAX_AMOUNT = ADD VALUE
|
|
|
|
// Compartment size
|
|
const double Cell = 1.0;
|
|
|
|
// Model parameters
|
|
const double kr_f = 0.5; // Forward repression binding rate
|
|
const double kr_r = 1.0; // Reverse repression binding rate
|
|
const double ka_f = 0.0033; // Forward activation binding rate
|
|
const double ka_r = 1.0; // Reverse activation binding rate
|
|
const double ko_f = 0.033; // Forward RNAP binding rate
|
|
const double ko_r = 1.0; // Reverse RNAP binding rate
|
|
const double kao_f = 1.0; // Forward activated RNAP binding rate
|
|
const double kao_r = 1.0; // Reverse activated RNAP binding rate
|
|
const double nc = 2.0; // Stoichiometry of binding
|
|
const double nr = 30.0; // Initial RNAP count
|
|
const double ko = 0.05; // Open complex production rate
|
|
const double kb = 1.0E-4; // Basal production rate
|
|
const double ng = 2.0; // Initial promoter count
|
|
const double np = 10.0; // Stoichiometry of production
|
|
const double ka = 0.25; // Activated production rate
|
|
const double kd = 7.5E-4; // Degradation rate
|
|
|
|
// Species _A
|
|
// const int _A_MAX = MAX_AMOUNT;
|
|
module _A
|
|
|
|
// _A : [0.._A_MAX] init 0;
|
|
_A : int init 0;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species D
|
|
// const int D_MAX = MAX_AMOUNT;
|
|
module D
|
|
|
|
// D : [0..D_MAX] init 70;
|
|
D : int init 70;
|
|
|
|
// Production_P1
|
|
[Production_P1] D >= 0 -> (D'=D+10);
|
|
// Degradation_D
|
|
[Degradation_D] D > 9 -> (D'=D-10);
|
|
|
|
endmodule
|
|
|
|
// Species B
|
|
// const int B_MAX = MAX_AMOUNT;
|
|
module B
|
|
|
|
// B : [0..B_MAX] init 120;
|
|
B : int init 120;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species Y
|
|
// const int Y_MAX = MAX_AMOUNT;
|
|
module Y
|
|
|
|
// Y : [0..Y_MAX] init 70;
|
|
Y : int init 70;
|
|
|
|
// Production_P3
|
|
[Production_P3] Y >= 0 -> (Y'=Y+10);
|
|
// Production_P5
|
|
[Production_P5] Y >= 0 -> (Y'=Y+10);
|
|
// Degradation_Y
|
|
[Degradation_Y] Y > 9 -> (Y'=Y-10);
|
|
|
|
endmodule
|
|
|
|
// Species _E
|
|
// const int _E_MAX = MAX_AMOUNT;
|
|
module _E
|
|
|
|
// _E : [0.._E_MAX] init 0;
|
|
_E : int init 0;
|
|
|
|
// Production_P2
|
|
[Production_P2] _E >= 0 -> (_E'=_E+10);
|
|
// Degradation_E
|
|
[Degradation_E] _E > 9 -> (_E'=_E-10);
|
|
|
|
endmodule
|
|
|
|
// Species _X
|
|
// const int _X_MAX = MAX_AMOUNT;
|
|
module _X
|
|
|
|
// _X : [0.._X_MAX] init 70;
|
|
_X : int init 70;
|
|
|
|
// Production_P1
|
|
[Production_P1] _X >= 0 -> (_X'=_X+10);
|
|
// Production_P2
|
|
[Production_P2] _X >= 0 -> (_X'=_X+10);
|
|
// Degradation_X
|
|
[Degradation_X] _X > 9 -> (_X'=_X-10);
|
|
|
|
endmodule
|
|
|
|
// Species FF
|
|
// const int FF_MAX = MAX_AMOUNT;
|
|
module FF
|
|
|
|
// FF : [0..FF_MAX] init 70;
|
|
FF : int init 70;
|
|
|
|
// Production_P8
|
|
[Production_P8] FF >= 0 -> (FF'=FF+10);
|
|
// Production_P7
|
|
[Production_P7] FF >= 0 -> (FF'=FF+10);
|
|
// Degradation_FF
|
|
[Degradation_FF] FF > 9 -> (FF'=FF-10);
|
|
|
|
endmodule
|
|
|
|
// Species Z
|
|
// const int Z_MAX = MAX_AMOUNT;
|
|
module Z
|
|
|
|
// Z : [0..Z_MAX] init 0;
|
|
Z : int init 0;
|
|
|
|
// Production_P4
|
|
[Production_P4] Z >= 0 -> (Z'=Z+10);
|
|
// Production_P6
|
|
[Production_P6] Z >= 0 -> (Z'=Z+10);
|
|
// Degradation_Z
|
|
[Degradation_Z] Z > 9 -> (Z'=Z-10);
|
|
|
|
endmodule
|
|
|
|
// Species _C
|
|
// const int _C_MAX = MAX_AMOUNT;
|
|
module _C
|
|
|
|
// _C : [0.._C_MAX] init 70;
|
|
_C : int init 70;
|
|
|
|
// Production_P5
|
|
[Production_P5] _C >= 0 -> (_C'=_C+10);
|
|
// Degradation_C
|
|
[Degradation_C] _C > 9 -> (_C'=_C-10);
|
|
|
|
endmodule
|
|
|
|
// Species P8
|
|
// const int P8_MAX = MAX_AMOUNT;
|
|
module P8
|
|
|
|
// P8 : [0..P8_MAX] init 2;
|
|
P8 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species P1
|
|
// const int P1_MAX = MAX_AMOUNT;
|
|
module P1
|
|
|
|
// P1 : [0..P1_MAX] init 2;
|
|
P1 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species P2
|
|
// const int P2_MAX = MAX_AMOUNT;
|
|
module P2
|
|
|
|
// P2 : [0..P2_MAX] init 2;
|
|
P2 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species P3
|
|
// const int P3_MAX = MAX_AMOUNT;
|
|
module P3
|
|
|
|
// P3 : [0..P3_MAX] init 2;
|
|
P3 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species P4
|
|
// const int P4_MAX = MAX_AMOUNT;
|
|
module P4
|
|
|
|
// P4 : [0..P4_MAX] init 2;
|
|
P4 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species P5
|
|
// const int P5_MAX = MAX_AMOUNT;
|
|
module P5
|
|
|
|
// P5 : [0..P5_MAX] init 2;
|
|
P5 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species P6
|
|
// const int P6_MAX = MAX_AMOUNT;
|
|
module P6
|
|
|
|
// P6 : [0..P6_MAX] init 2;
|
|
P6 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Species P7
|
|
// const int P7_MAX = MAX_AMOUNT;
|
|
module P7
|
|
|
|
// P7 : [0..P7_MAX] init 2;
|
|
P7 : int init 2;
|
|
|
|
|
|
endmodule
|
|
|
|
// Reaction rates
|
|
module reaction_rates
|
|
|
|
// Production_P8: -> FF
|
|
[Production_P8] (((((P8 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) *_E) , nc))) > 0 -> ((((((P8 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) *_E) , nc)))) : true;
|
|
|
|
// Production_P1: -> D _X
|
|
[Production_P1] (((((P1 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) *_A) , nc))) > 0 -> ((((((P1 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) *_A) , nc)))) : true;
|
|
|
|
// Production_P2: -> _E _X
|
|
[Production_P2] (((((P2 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * B) , nc))) > 0 -> ((((((P2 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * B) , nc)))) : true;
|
|
|
|
// Production_P3: -> Y
|
|
[Production_P3] (((((P3 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) *_X) , nc))) > 0 -> ((((((P3 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) *_X) , nc)))) : true;
|
|
|
|
// Production_P4: -> Z
|
|
[Production_P4] (((((P4 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * FF) , nc))) > 0 -> ((((((P4 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * FF) , nc)))) : true;
|
|
|
|
// Production_P5: -> _C Y
|
|
[Production_P5] (((((P5 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * Z) , nc))) > 0 -> ((((((P5 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * Z) , nc)))) : true;
|
|
|
|
// Production_P6: -> Z
|
|
[Production_P6] (((((P6 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * Y) , nc))) > 0 -> ((((((P6 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * Y) , nc)))) : true;
|
|
|
|
// Production_P7: -> FF
|
|
[Production_P7] (((((P7 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * D) , nc))) > 0 -> ((((((P7 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * D) , nc)))) : true;
|
|
|
|
// Degradation_E: ->
|
|
[Degradation_E] (kd *_E) > 0 -> ((kd *_E)) : true;
|
|
|
|
// Degradation_C: ->
|
|
[Degradation_C] (kd *_C) > 0 -> ((kd *_C)) : true;
|
|
|
|
// Degradation_X: ->
|
|
[Degradation_X] (kd *_X) > 0 -> ((kd *_X)) : true;
|
|
|
|
// Degradation_D: ->
|
|
[Degradation_D] (kd * D) > 0 -> ((kd * D)) : true;
|
|
|
|
// Degradation_FF: ->
|
|
[Degradation_FF] (kd * FF) > 0 -> ((kd * FF)) : true;
|
|
|
|
// Degradation_Y: ->
|
|
[Degradation_Y] (kd * Y) > 0 -> ((kd * Y)) : true;
|
|
|
|
// Degradation_Z: ->
|
|
[Degradation_Z] (kd * Z) > 0 -> ((kd * Z)) : true;
|
|
|
|
endmodule
|
|
|
|
// Reward structures (one per species)
|
|
// Reward 1: _A
|
|
rewards "_A" true : _A; endrewards
|
|
// Reward 2: D
|
|
rewards "D" true : D; endrewards
|
|
// Reward 3: B
|
|
rewards "B" true : B; endrewards
|
|
// Reward 4: Y
|
|
rewards "Y" true : Y; endrewards
|
|
// Reward 5: _E
|
|
rewards "_E" true : _E; endrewards
|
|
// Reward 6: _X
|
|
rewards "_X" true : _X; endrewards
|
|
// Reward 7: FF
|
|
rewards "FF" true : FF; endrewards
|
|
// Reward 8: Z
|
|
rewards "Z" true : Z; endrewards
|
|
// Reward 9: _C
|
|
rewards "_C" true : _C; endrewards
|
|
// Reward 10: P8
|
|
rewards "P8" true : P8; endrewards
|
|
// Reward 11: P1
|
|
rewards "P1" true : P1; endrewards
|
|
// Reward 12: P2
|
|
rewards "P2" true : P2; endrewards
|
|
// Reward 13: P3
|
|
rewards "P3" true : P3; endrewards
|
|
// Reward 14: P4
|
|
rewards "P4" true : P4; endrewards
|
|
// Reward 15: P5
|
|
rewards "P5" true : P5; endrewards
|
|
// Reward 16: P6
|
|
rewards "P6" true : P6; endrewards
|
|
// Reward 17: P7
|
|
rewards "P7" true : P7; endrewards
|