% two_genes
% a simple model of two mutually inhibiting genes
% the two protein concentrations are xa and xb
%
% ------------- state space description --------------
% number of genes 
2
% partition for xa
[0 8 12 18 22 30]
% partition for xb
[0 8 12 20]
%
% ------------- variable description -------------- 
% -- xa --
% number of production terms
1
% production rate (ie constant kappa)
[6 27]
% this is an uncertain parameter
% production expression (ie regulation function)
% prefix notation is used! more explanations in web page
*	
-
r		
1
[1 4 5 6]
[0 0 1 1]
-
r
2
[1 2 3 4]
[0 0 1 1]
% number of degradation terms
1
% degradation rate (ie constant gamma)
[1]
% this is a known parameter
% degradation expression (ie regulation function)
1
% -- xb --
% number of production terms
1
% production rate
[34]
% degradation expression
-
r
1
[1 2 3 6]
[0 0 1 1]
% number of degradation terms
1
% degreadation rate
[2]
% degradation expression
1
%
% -------------  expected behavior specifications -------------- 
% number of atomic propositions
4
% the atomic propositions 
% see explanations in web page
{1 '>' 2} 
{2 '>' 2}
{1 '>' 3}
{2 '>' 3}
% initial states for verification (NuSMV predicate or "All")
All
% property type (0: CTL; 1:LTL); % note: CTL is not supported yet!
1
% property text
F ( (prop1 | prop2) & !(prop3 & prop4))
% compute liveness of SCCs (0: No; 1:Yes)?
1