%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Analysis of the tuning of a synthetic transcriptional cascade 
% built by Hooshangi et al. (PNAS, 2005)
%
% Author: Gregory Batt
%         Boston University, 
%         Brookline, MA, USA
% email: batt@bu.edu
% Website: http://iasi.bu.edu/~batt/
% Oct. 2006 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% ------------- state space description --------------
% number of variables
5
% partition for TetR (describe the "lambda values")
[0 4500 5500 24000]
% partition for LacI
[0 241.04 750 1213.21 2841.26 8611.29 1000000]
% partition for cI
[0 342.87 5766.3 15045 25729 3200000]
% partition for EYFP
[0 250 500 500000 1000000 5000000]
% partition for aTc
[0 70.353 100 238.49 400 1859.5 7797.8 240000]
%
% ------------- variable description -------------- 
%
% -- TetR --
% number of production terms for TetR (ie "kappas")
1
% production term for TetR
[260]
% ramp expr for production term for TetR ("1" means that the function is constant)
1
% number of degradation terms for TetR (ie "gammas")
1
% degradation rate
[0.013]
% ramp expr for degradation term
1
% -- LacI --
% number of production terms for LacI
2
% production term 1 for LacI; constitutive expression
[2.405]
% ramp expr for production term 1 for LacI
1
% production term 2 for LacI
% this is an uncertain parameter
[70 7000]
% ramp expr for production term 2 for LacI (ie regulation function)
% prefix notation is used! more explanations in web page
-
*
-
r
5
[1 2 4 6 7 8]
[0 0 0.0106 0.7902 1 1]
r
1
[1 2 3 4]
[0 0 1 1]
% number of degradation terms
1
% degradation rate
[0.013]
% ramp expr for degradation term
1
% -- cI --
% number of production terms for cI
2
% production term 1 for cI
[3.63]
% ramp expr for production term 1 for cI
1
% production term 2 for cI
[75 8000]
% ramp expr for production term 2 for cI
r
2
[1 2 4 5 6 7]
[1 1 0.1700 0.0220 0 0]
% number of degradation terms
1
% degradation rate
[0.013]
% ramp expr for degradation term
1
% -- EYFP --
% number of production terms for EYFP
2
% production term 1 for EYFP
[4.59]
% ramp expr for production term 1 for EYFP
1
% production term 2 for EYFP
[30 30000]
% ramp expr for production term 2 for EYFP
r
3
[1 2 3 4 5 6]
[1 1 0.3084 0.0896 0 0]
% number of degradation terms
1
% degradation rate
[0.013]
% ramp expr for degradation term
1
% -- aTc -- (constant input variable)
% number of production terms for aTc
0
% number of degradation terms
0
%
% -------------  expected behavior specifications -------------- 
%
% number of atomic propositions
6
% atomic proposition 1; for syntax, see explanations in web page
{5 '<' 3}
% atomic proposition 2
{4 '<' 3}
% atomic proposition 3
{4 '>' 2}
% atomic proposition 4
{5 '>' 5}
% atomic proposition 5  
{4 '>' 4}
% atomic proposition 6  
{4 '<' 5}
% initial states for verification (NuSMV predicate or "All")
All
% property type (0: CTL; 1:LTL); CTL not supported yet
1
% property text; in NuSMV syntax
(prop1 -> F G (prop2 & prop3)) & (prop4 -> F G (prop5 & prop6)) & ((!prop1 & !prop4)  -> F G (prop3 & prop6))
% compute SCCs ?
0