RiSE4fun samples for Z34BioList of built-in samples for the Z34Bio in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Z34Biohttp://rise4fun.com/Z34Biology/Chem_NetworkChem_Network//Specification Gate[0] = 3 and GateA[0] = 0 and GateB[0] = 0 and GateAB[0] = 0; C[5] = 3; //Model: Describes a DSD model of a logic AND gate Gate + A <-> GateA Gate + B <-> GateB GateA + B -> GateAB + C GateB + A -> GateAB + C http://rise4fun.com/Z34Biology/Boolean_NetworkBoolean_Network//Specification: Show that oscillations are possible //1) first, proove that path depth k=6 guarantees completeness for finding cycles: //the following should be UNSAT simple(#path,6); //2) Then, proove that it is possible to reach a cycle (a path that does not reach a fixed point) //not (C[6] = C[5]); //Settings directive constEncoding BitVector directive encoding BitVector directive plot A, B //Model: Describes a toy Boolean network used for illustration A' = not(A) B' = A and B C' = A or B http://rise4fun.com/Z34Biology/Mixed_ModelMixed_Model//Settings: //plotting directive plot A,GateA,GateAB,D //maximal number of molecules directive maxMols 20 //chemical species are described by an integer directive encoding Integer //constants are encoded as integers directive constEncoding Integer //individual state components are separated directive splitStates //SPECIFICATION cycle(#path,6); let $mass := {A + GateA + GateAB = 5}; //conservation of mass #path |= $mass; #path[6] |= (D=0); //MODEL: CRN component Gate + A <-> GateA Gate + B <-> GateB GateA + B -> GateAB + C(e) GateB + A -> GateAB + C(e) //MODEL: BN component D' = C(e)>5 E' = D and E F' = D or Ehttp://rise4fun.com/Z34Biology/thelperthelper// Boolean network model of the control of T-helper cell differentiation from // "A method for the generation of standardized qualitative dynamical systems // of regulatory networks", L. Mendoza and I. Xenarios // J. Theor. Biol. and Medical Modelling, 2006, vol. 3, no. 13 // // Originally studied in // "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks." // E. Dubrova and M. Teslenko.IEEE/ACM Trans. on Comput. Biology and Bioinformatics, 8:1393{1399, 2011. // // Converted automatically from BLIF representation using Z34Bio //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To for oscillations, search for a cycle of any length. lasso(#path,12); //Model: TCR' = false NFAT' = (TCR) IFN-bX' = false IFN-bR' = (IFN-bX) IL-18X' = false IL-18R' = (IL-18X and not (STAT6)) IRAK' = (IL-18R) SOCS1' = (STAT1) or (T-bet) IL-12X' = false IL-12R' = (IL-12X and not (STAT6)) STAT4' = (IL-12R and not (GATA3)) T-bet' = (STAT1 and not (GATA3)) or (T-bet and not (GATA3)) IFN-gX' = (T-bet and not (STAT3)) or (STAT4 and not (STAT3)) or (IRAK and not (STAT3)) or (NFAT and not (STAT3)) IFN-gR' = (IFN-gX) JAK1' = (IFN-gR and not (SOCS1)) STAT1' = (JAK1) or (IFN-bR) IL-4X' = (GATA3 and not (STAT1)) IL-4R' = (IL-4X and not (SOCS1)) STAT6' = (IL-4R) GATA3' = (GATA3 and not (T-bet)) or (STAT6 and not (T-bet)) IL-10X' = (GATA3) IL-10R' = (IL-10X) STAT3' = (IL-10R) http://rise4fun.com/Z34Biology/arabidopsisarabidopsis// Boolean network model of the control of flower morphogenesis in Arabidobis thaliana // "From Genes to Flower Patterns and Evolution: Dynamic Models of Gene Regulatory Networks" // A. Chaos, M. Aldana, C. Espinosa-Soto, B. G. P. de Leon, A. G. Arroyo, E. R. Alvarez-Buylla, // Journal of Plant Growth Regulation, vol. 25, n. 4, 2006, pp. 278-289 // // Originally studied in // "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks." // E. Dubrova and M. Teslenko.IEEE/ACM Trans. on Comput. Biology and Bioinformatics, 8:1393{1399, 2011. // // Converted automatically from BLIF representation using Z34Bio //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To for oscillations, search for a cycle of any length. lasso(#path,11); //Model: AG' = (LFY and AG and SEP) or (not (AP2) and not (TFL1)) or (LFY and not (CLF)) or (LFY and not (LUG)) or (LFY and WUS) or (not (AP1) and LFY) or (LFY and not (AP2)) AP3' = (AG and PI and SEP and AP3) or (AP1 and PI and SEP and AP3) or (LFY and UFO) UFO' = (UFO) FUL' = (not (AP1) and not (TFL1)) FT' = (not (EMF1)) AP1' = (not (AG) and not (TFL1)) or (LFY and not (AG)) or (FT and not (AG)) EMF1' = (not (LFY)) LFY' = (not (TFL1)) or (not (EMF1)) AP2' = (not (TFL1)) WUS' = (WUS and not (SEP)) or (WUS and not (AG)) LUG' = true CLF' = true TFL1' = (not (AP1) and EMF1 and not (LFY)) PI' = (AP1 and PI and SEP and AP3) or (AG and PI and SEP and AP3) or (LFY and AG) or (LFY and AP3) SEP' = (LFY) http://rise4fun.com/Z34Biology/mammalianmammalian// Boolean network model of the control of the mammalian cell cycle from // "Dynamical Analysis of a Generic Boolean Model for the Control of the // Mammalian Cell Cycle", A. Faure, A. Naldi, C. Chaouiya, D. Thieffry, // Bioinformatics, 2006, vol. 22, no. 14, pp. e124-e131. // // Originally studied in // "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks." // E. Dubrova and M. Teslenko.IEEE/ACM Trans. on Comput. Biology and Bioinformatics, 8:1393{1399, 2011. // // Converted automatically from BLIF representation using Z34Bio //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To for oscillations, search for a cycle of any length. lasso(#path,12); //Model: CycD' = (CycD) CycE' = (not (Rb) and E2F) Rb' = (not (CycD) and not (CycE) and not (CycA) and not (CycB)) or (not (CycD) and p27 and not (CycB)) E2F' = (not (Rb) and p27 and not (CycB)) or (not (Rb) and not (CycA) and not (CycB)) CycA' = (not (Rb) and CycA and not (Cdc20) and not (Cdh1)) or (not (Rb) and E2F and not (Cdc20) and not (Cdh1)) or (not (Rb) and CycA and not (Cdc20) and not (UbcH10)) or (not (Rb) and E2F and not (Cdc20) and not (UbcH10)) p27' = (not (CycD) and not (CycA) and p27 and not (CycB)) or (not (CycD) and not (CycE) and p27 and not (CycB)) or (not (CycD) and not (CycE) and not (CycA) and not (CycB)) Cdc20' = (CycB) UbcH10' = (UbcH10 and CycB) or (Cdc20 and UbcH10) or (CycA and UbcH10) or (not (Cdh1)) Cdh1' = (p27 and not (CycB)) or (not (CycA) and not (CycB)) or (Cdc20) CycB' = (not (Cdc20) and not (Cdh1)) http://rise4fun.com/Z34Biology/tcrtcr// Boolean network model of the T-cell receptor signalling pathway from // "A methodology for the structural and functional analysis of signaling and // regulatory networks", S. Klamt, J. Saez-Rodriguez, J. A. Lindquist, L. Simeoni, E. D. Gilles, // JBMC Bioinformatics 7: 56, 2006. // // Originally studied in // "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks." // E. Dubrova and M. Teslenko.IEEE/ACM Trans. on Comput. Biology and Bioinformatics, 8:1393{1399, 2011. //rasX // Converted automatically from BLIF representation using Z34Bio //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To for oscillations, search for a cycle of any length. lasso(#path,19); //Model: CD45' = (CD45) CD8' = (CD8) TCRlig' = (TCRlig) TCbind' = (TCRlig and not (cCbl)) PAGCsk' = (not (TCbind)) or (Fyn) LCK' = (CD45 and CD8 and not (PAGCsk)) Fyn' = (CD45 and LCK) or (CD45 and TCbind) Rlk' = (LCK) TCRphos' = (TCbind and LCK) or (Fyn) ZAP70' = (LCK and TCRphos and not (cCbl)) cCbl' = (ZAP70) Itk' = (ZAP70 and Slp76) LAT' = (ZAP70) Gads' = (LAT) Slp76' = (Gads) PLCg_b' = (LAT) Grb2Sos' = (LAT) DAG' = (PLCg_a) PLCg_a' = (ZAP70 and Itk and Slp76 and PLCg_b) or (Rlk and ZAP70 and Slp76 and PLCg_b) RasX' = (RasGRP1) or (Grb2Sos) RasGRP1' = (DAG and PKCth) PKCth' = (DAG) IP3' = (PLCg_a) Raf' = (RasX) MEK' = (Raf) CaX' = (IP3) ERK' = (MEK) SEK' = (PKCth) IKK' = (PKCth) Calcin' = (CaX) Rsk' = (ERK) Fos' = (ERK) JNK' = (SEK) IkB' = (not (IKK)) CREB' = (Rsk) Jun' = (JNK) CRE' = (CREB) AP1' = (Fos and Jun) NFkB' = (not (IkB)) NFAT' = (Calcin) http://rise4fun.com/Z34Biology/fission_yeastfission_yeast// Boolean network model of the control of the fission yeast cell cycle regulation from // "Boolean Network Model Predicts Cell Cycle Sequence of Fission Yeast", // M. I. Davidich, S. Bornholdt, PLoS ONE. 2008 Feb 27, 3(2):e1672. // // Originally studied in // "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks." // E. Dubrova and M. Teslenko.IEEE/ACM Trans. on Comput. Biology and Bioinformatics, 8:1393{1399, 2011. // // Converted automatically from BLIF representation using Z34Bio //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To for oscillations, search for a cycle of any length. lasso(#path,7); //Model: Start' = false SK' = (Start) Ste9' = (not (SK) and Ste9 and not (Cdc2_Cdc13x) and not (Cdc2_Cdc13s)) or (Ste9 and not (Cdc2_Cdc13x) and PP and not (Cdc2_Cdc13s)) or (not (SK) and Ste9 and PP and not (Cdc2_Cdc13s)) or (not (SK) and Ste9 and not (Cdc2_Cdc13x) and PP) or (not (SK) and not (Cdc2_Cdc13x) and PP and not (Cdc2_Cdc13s)) Cdc2_Cdc13x' = (Cdc2_Cdc13x and not (Rum1) and not (Slp1)) or (not (Ste9) and Cdc2_Cdc13x and not (Slp1)) or (not (Ste9) and Cdc2_Cdc13x and not (Rum1)) or (not (Ste9) and not (Rum1) and not (Slp1)) Rum1' = (not (Cdc2_Cdc13x) and Rum1 and PP and Cdc2_Cdc13s) or (not (SK) and not (Cdc2_Cdc13x) and Rum1 and not (Cdc2_Cdc13s)) or (not (SK) and Rum1 and PP and not (Cdc2_Cdc13s)) or (not (SK) and not (Cdc2_Cdc13x) and PP and not (Cdc2_Cdc13s)) PP' = (Slp1) Cdc25' = (not (PP) and Cdc25) or (Cdc2_Cdc13x and Cdc25) or (Cdc2_Cdc13x and not (PP)) Slp1' = (Cdc2_Cdc13s) Wee1_Mik1' = (not (Cdc2_Cdc13x) and Wee1_Mik1) or (PP and Wee1_Mik1) or (not (Cdc2_Cdc13x) and PP) Cdc2_Cdc13s' = (not (Ste9) and not (Rum1) and Cdc25 and not (Slp1) and not (Wee1_Mik1) and Cdc2_Cdc13s) http://rise4fun.com/Z34Biology/drosophila4drosophila4// Boolean network model of Drosophila melanogaster from // "The topology of the regulatory interactions predicts the expression pattern of the // segment polarity genes in Drosophila melanogaster", R. Albert and H. G. Othmer, // Journal of Theoretical Biology, 2003, vol. 223, no. 1, pp. 1-18. // // Originally studied in // "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks." // E. Dubrova and M. Teslenko.IEEE/ACM Trans. on Comput. Biology and Bioinformatics, 8:1393{1399, 2011. // // Converted automatically from BLIF representation using Z34Bio //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To for oscillations, search for a cycle of any length. lasso(#path,35); //Model: SLP1' = false SLP2' = false SLP3' = true SLP4' = true wg1' = (CIA1 and SLP1 and not (CIR1)) or (wg1 and SLP1 and not (CIR1)) or (wg1 and CIA1 and not (CIR1)) wg2' = (CIA2 and SLP2 and not (CIR2)) or (wg2 and SLP2 and not (CIR2)) or (wg2 and CIA2 and not (CIR2)) wg3' = (CIA3 and SLP3 and not (CIR3)) or (wg3 and SLP3 and not (CIR3)) or (wg3 and CIA3 and not (CIR3)) wg4' = (CIA4 and SLP4 and not (CIR4)) or (wg4 and SLP4 and not (CIR4)) or (wg4 and CIA4 and not (CIR4)) WG1' = (wg1) WG2' = (wg2) WG3' = (wg3) WG4' = (wg4) en1' = (WG2 and not (SLP1)) en2' = (WG3 and not (SLP2)) or (WG1 and not (SLP2)) en3' = (WG4 and not (SLP3)) or (WG2 and not (SLP3)) en4' = (WG3 and not (SLP4)) EN1' = (en1) EN2' = (en2) EN3' = (en3) EN4' = (en4) hh1' = (EN1 and not (CIR1)) hh2' = (EN2 and not (CIR2)) hh3' = (EN3 and not (CIR3)) hh4' = (EN4 and not (CIR4)) HH1' = (hh1) HH2' = (hh2) HH3' = (hh3) HH4' = (hh4) ptc1' = (CIA1 and not (EN1) and not (CIR1)) ptc2' = (CIA2 and not (EN2) and not (CIR2)) ptc3' = (CIA3 and not (EN3) and not (CIR3)) ptc4' = (CIA4 and not (EN4) and not (CIR4)) PTC1' = (PTC1 and not (HH2)) or (ptc1) PTC2' = (PTC2 and not (HH1) and not (HH3)) or (ptc2) PTC3' = (PTC3 and not (HH2) and not (HH4)) or (ptc3) PTC4' = (PTC4 and not (HH3)) or (ptc4) ci1' = (not (EN1)) ci2' = (not (EN2)) ci3' = (not (EN3)) ci4' = (not (EN4)) CI1' = (ci1) CI2' = (ci2) CI3' = (ci3) CI4' = (ci4) CIA1' = (CI1 and hh2) or (CI1 and HH2) or (CI1 and not (PTC1)) CIA2' = (CI2 and hh3) or (CI2 and hh1) or (CI2 and HH3) or (CI2 and HH1) or (CI2 and not (PTC2)) CIA3' = (CI3 and hh4) or (CI3 and hh2) or (CI3 and HH4) or (CI3 and HH2) or (CI3 and not (PTC3)) CIA4' = (CI4 and hh3) or (CI4 and HH3) or (CI4 and not (PTC4)) CIR1' = (CI1 and PTC1 and not (HH2) and not (hh2)) CIR2' = (CI2 and PTC2 and not (HH1) and not (HH3) and not (hh1) and not (hh3)) CIR3' = (CI3 and PTC3 and not (HH2) and not (HH4) and not (hh2) and not (hh4)) CIR4' = (CI4 and PTC4 and not (HH3) and not (hh3)) http://rise4fun.com/Z34Biology/budding_yeastbudding_yeast// Boolean network model of the control of the budding yeast cell cycle regulation from // "The yeast cell-cycle network is robustly designed", // Fangting Li, Tao Long, Ying Lu, Qi Ouyang, Chao Tang, // PNAS April 6, 2004, vol. 101 no. 14 4781-4786. // // Originally studied in // "A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks." // E. Dubrova and M. Teslenko.IEEE/ACM Trans. on Comput. Biology and Bioinformatics, 8:1393{1399, 2011. // // Converted automatically from BLIF representation using Z34Bio //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To for oscillations, search for a cycle of any length. lasso(#path,19); //Model: Cell size' = false Cln3' = (Cell size) SBF' = (SBF and not (Clb1_2)) or (Cln3 and SBF) or (Cln3 and not (Clb1_2)) MBF' = (MBF and not (Clb1_2)) or (Cln3 and MBF) or (Cln3 and not (Clb1_2)) Cln1_2' = (SBF) Sic1' = (not (Cln1_2) and Sic1 and not (Cln5_6) and not (Clb1_2)) or (Sic1 and not (Cln5_6) and not (Clb1_2) and Cdc20_Cdc14) or (not (Cln1_2) and Sic1 and not (Clb1_2) and Cdc20_Cdc14) or (not (Cln1_2) and Sic1 and not (Cln5_6) and Cdc20_Cdc14) or (Sic1 and not (Cln5_6) and not (Clb1_2) and Swi5) or (not (Cln1_2) and Sic1 and not (Clb1_2) and Swi5) or (not (Cln1_2) and Sic1 and not (Cln5_6) and Swi5) or (Sic1 and not (Clb1_2) and Cdc20_Cdc14 and Swi5) or (Sic1 and not (Cln5_6) and Cdc20_Cdc14 and Swi5) or (not (Cln1_2) and Sic1 and Cdc20_Cdc14 and Swi5) or (not (Cln1_2) and not (Cln5_6) and not (Clb1_2) and Swi5) or (not (Cln5_6) and not (Clb1_2) and Cdc20_Cdc14 and Swi5) or (not (Cln1_2) and not (Clb1_2) and Cdc20_Cdc14 and Swi5) or (not (Cln1_2) and not (Cln5_6) and Cdc20_Cdc14 and Swi5) or (not (Cln1_2) and not (Cln5_6) and not (Clb1_2) and Cdc20_Cdc14) Cln5_6' = (not (Sic1) and Cln5_6 and not (Cdc20_Cdc14)) or (MBF and Cln5_6 and not (Cdc20_Cdc14)) or (MBF and not (Sic1) and Cln5_6) or (MBF and not (Sic1) and not (Cdc20_Cdc14)) Cdh1' = (not (Cln1_2) and not (Cln5_6) and Cdh1 and not (Clb1_2)) or (not (Cln5_6) and Cdh1 and not (Clb1_2) and Cdc20_Cdc14) or (not (Cln1_2) and Cdh1 and not (Clb1_2) and Cdc20_Cdc14) or (not (Cln1_2) and not (Cln5_6) and Cdh1 and Cdc20_Cdc14) or (not (Cln1_2) and not (Cln5_6) and not (Clb1_2) and Cdc20_Cdc14) Clb1_2' = (not (Sic1) and Cln5_6 and not (Cdh1) and Clb1_2) or (not (Sic1) and not (Cdh1) and Clb1_2 and Mcm1_SFF) or (Cln5_6 and not (Cdh1) and Clb1_2 and Mcm1_SFF) or (not (Sic1) and Cln5_6 and Clb1_2 and Mcm1_SFF) or (not (Sic1) and not (Cdh1) and Clb1_2 and not (Cdc20_Cdc14)) or (Cln5_6 and not (Cdh1) and Clb1_2 and not (Cdc20_Cdc14)) or (not (Sic1) and Cln5_6 and Clb1_2 and not (Cdc20_Cdc14)) or (not (Cdh1) and Clb1_2 and Mcm1_SFF and not (Cdc20_Cdc14)) or (not (Sic1) and Clb1_2 and Mcm1_SFF and not (Cdc20_Cdc14)) or (Cln5_6 and Clb1_2 and Mcm1_SFF and not (Cdc20_Cdc14)) or (not (Sic1) and Cln5_6 and not (Cdh1) and not (Cdc20_Cdc14)) or (not (Sic1) and not (Cdh1) and Mcm1_SFF and not (Cdc20_Cdc14)) or (Cln5_6 and not (Cdh1) and Mcm1_SFF and not (Cdc20_Cdc14)) or (not (Sic1) and Cln5_6 and Mcm1_SFF and not (Cdc20_Cdc14)) or (not (Sic1) and Cln5_6 and not (Cdh1) and Mcm1_SFF) Mcm1_SFF' = (Clb1_2) or (Cln5_6) Cdc20_Cdc14' = (Mcm1_SFF) or (Clb1_2) Swi5' = (not (Clb1_2) and Cdc20_Cdc14) or (Mcm1_SFF and Cdc20_Cdc14) or (not (Clb1_2) and Mcm1_SFF) http://rise4fun.com/Z34Biology/DNA_transducersDNA_transducers//-------------------------------------------------------------------------- //Transducer DNA Circuits. Four transducers in series. Model generated by Visual DSD //-------------------------------------------------------------------------- //-------------------------------------------------------------------------- //SPECIFICATIONS //-------------------------------------------------------------------------- //FIND REACHABLE VIOLATION STATE //at 0 $init; //$no_rxn_enabled; //not $no_reactive_species; //FIND REACHABLE SAT STATE at 0 $init; at 50 $no_rxn_enabled; at 50 $no_reactive_species; //TEST INVARIANT //#path[0]|=$invariant; //not(#path[1]|=$invariant); //-------------------------------------------------------------------------- //MODEL //-------------------------------------------------------------------------- T_2 + S<->sp_1 + sp_0 sp_1 + T->sp_4 + sp_3 + sp_2 T_15 + sp_2<->sp_9 + sp_5 T_11 + sp_2<->sp_8 + sp_5 T_7 + sp_2<->sp_7 + sp_5 T_3 + sp_2<->sp_6 + sp_5 sp_9 + T_13->sp_12 + sp_11 + sp_10 sp_4 + sp_5->sp_14 + sp_13 sp_8 + T_9->sp_17 + sp_16 + sp_15 T_14 + sp_15<->sp_19 + sp_18 sp_19 + T_12->sp_20 + sp_11 + sp_2 sp_20 + sp_5->sp_21 + sp_13 sp_12 + sp_18->sp_23 + sp_22 sp_7 + T_5->sp_26 + sp_25 + sp_24 T_10 + sp_24<->sp_28 + sp_27 sp_28 + T_8->sp_29 + sp_16 + sp_2 sp_29 + sp_5->sp_30 + sp_13 sp_17 + sp_27->sp_32 + sp_31 sp_6 + T_1->sp_34 + sp_3 + sp_33 T_6 + sp_33<->sp_36 + sp_35 sp_36 + T_4->sp_37 + sp_25 + sp_2 sp_37 + sp_5->sp_38 + sp_13 sp_26 + sp_35->sp_40 + sp_39 sp_34 + sp_0->sp_42 + sp_41 //-------------------------------------------------------------------------- //PROPERTY DEFINITIONS //-------------------------------------------------------------------------- let $init := { sp_2 = 0 and sp_13 = 0 and sp_25 = 0 and sp_16 = 0 and sp_11 = 0 and sp_3 = 0 and sp_5 = 0 and T = 1 and T_4 = 1 and T_8 = 1 and T_12 = 1 and S = 1 and sp_33 = 0 and sp_24 = 0 and sp_15 = 0 and sp_10 = 0 and sp_0 = 0 and sp_41 = 0 and T_1 = 1 and sp_35 = 0 and sp_39 = 0 and T_5 = 1 and sp_27 = 0 and sp_31 = 0 and T_9 = 1 and sp_18 = 0 and sp_22 = 0 and T_13 = 1 and sp_14 = 0 and sp_4 = 0 and sp_1 = 0 and sp_38 = 0 and sp_37 = 0 and sp_36 = 0 and sp_30 = 0 and sp_29 = 0 and sp_28 = 0 and sp_21 = 0 and sp_20 = 0 and sp_19 = 0 and sp_42 = 0 and T_3 = 1 and sp_6 = 0 and sp_34 = 0 and sp_40 = 0 and T_7 = 1 and sp_7 = 0 and sp_26 = 0 and sp_32 = 0 and T_11 = 1 and sp_8 = 0 and sp_17 = 0 and sp_23 = 0 and T_15 = 1 and sp_9 = 0 and sp_12 = 0 and T_2 = 1 and T_6 = 1 and T_10 = 1 and T_14 = 1 }; let $no_rxn_enabled := { ( T_2<1 or S<1) and ( sp_1<1 or sp_0<1) and ( sp_1<1 or T<1) and ( T_15<1 or sp_2<1) and ( sp_9<1 or sp_5<1) and ( T_11<1 or sp_2<1) and ( sp_8<1 or sp_5<1) and ( T_7<1 or sp_2<1) and ( sp_7<1 or sp_5<1) and ( T_3<1 or sp_2<1) and ( sp_6<1 or sp_5<1) and ( sp_9<1 or T_13<1) and ( sp_4<1 or sp_5<1) and ( sp_8<1 or T_9<1) and ( T_14<1 or sp_15<1) and ( sp_19<1 or sp_18<1) and ( sp_19<1 or T_12<1) and ( sp_20<1 or sp_5<1) and ( sp_12<1 or sp_18<1) and ( sp_7<1 or T_5<1) and ( T_10<1 or sp_24<1) and ( sp_28<1 or sp_27<1) and ( sp_28<1 or T_8<1) and ( sp_29<1 or sp_5<1) and ( sp_17<1 or sp_27<1) and ( sp_6<1 or T_1<1) and ( T_6<1 or sp_33<1) and ( sp_36<1 or sp_35<1) and ( sp_36<1 or T_4<1) and ( sp_37<1 or sp_5<1) and ( sp_26<1 or sp_35<1) and ( sp_34<1 or sp_0<1) }; let $no_reactive_species := { T_15 = 0 and T_14 = 0 and T_13 = 0 and T_12 = 0 and T_11 = 0 and T_10 = 0 and T_9 = 0 and T_8 = 0 and T_7 = 0 and T_6 = 0 and T_5 = 0 and T_4 = 0 and T_3 = 0 and T_2 = 0 and T_1 = 0 and T = 0 and S = 0 }; let $invariant := { sp_38 + sp_30 + sp_21 + sp_14 + sp_5 + T_3 + T_7 + T_11 + T_15 = 4 and sp_14 + sp_4 + T = 1 and sp_38 + sp_37 + T_4 = 1 and sp_30 + sp_29 + T_8 = 1 and sp_21 + sp_20 + T_12 = 1 and sp_14 + sp_4 + sp_1 + S = 1 and sp_38 + sp_37 + sp_36 + sp_33 + sp_6 + T_3 = 1 and sp_30 + sp_29 + sp_28 + sp_24 + sp_7 + T_7 = 1 and sp_21 + sp_20 + sp_19 + sp_15 + sp_8 + T_11 = 1 and sp_10 + sp_9 + T_15 = 1 and sp_37 + sp_36 + sp_29 + sp_28 + sp_20 + sp_19 + sp_13 + sp_4 + sp_1 + T_2 + T_6 + T_10 + T_14 = 4 and sp_42 + sp_40 + sp_36 + sp_34 + sp_6 + sp_32 + sp_28 + sp_26 + sp_7 + sp_23 + sp_19 + sp_17 + sp_8 + sp_12 + sp_9 + sp_2 + sp_1 + T_2 + T_6 + T_10 + T_14 = 4 and sp_6 + sp_3 + sp_1 + T_2 + T_3 = 2 and sp_36 + sp_25 + sp_7 + T_6 + T_7 = 2 and sp_28 + sp_16 + sp_8 + T_10 + T_11 = 2 and sp_19 + sp_11 + sp_9 + T_14 + T_15 = 2 and sp_41 + sp_34 + sp_6 + T_3 = 1 and sp_42 + sp_0 + T_2 = 1 and sp_39 + sp_26 + sp_7 + T_7 = 1 and sp_40 + sp_35 + T_6 = 1 and sp_42 + sp_34 + T_1 = 1 and sp_31 + sp_17 + sp_8 + T_11 = 1 and sp_32 + sp_27 + T_10 = 1 and sp_40 + sp_26 + T_5 = 1 and sp_22 + sp_12 + sp_9 + T_15 = 1 and sp_23 + sp_18 + T_14 = 1 and sp_32 + sp_17 + T_9 = 1 and sp_23 + sp_12 + T_13 = 1 and sp_14 + sp_4 + sp_1 + T_2 = 1 and sp_38 + sp_37 + sp_36 + T_6 = 1 and sp_30 + sp_29 + sp_28 + T_10 = 1 and sp_21 + sp_20 + sp_19 + T_14 = 1 and sp_42 + sp_34 + sp_6 + T_3 = 1 and sp_40 + sp_26 + sp_7 + T_7 = 1 and sp_32 + sp_17 + sp_8 + T_11 = 1 and sp_23 + sp_12 + sp_9 + T_15 = 1 }; http://rise4fun.com/Z34Biology/DNA_square_rootDNA_square_root//-------------------------------------------------------------------------- //Qian and Winfree 4 bit square root circuit. Model generated by Visual DSD //-------------------------------------------------------------------------- //-------------------------------------------------------------------------- //SPECIFICATION: TEST INVARIANT //-------------------------------------------------------------------------- #path[0]|=$invariant; not(#path[1]|=$invariant); //-------------------------------------------------------------------------- //MODEL //-------------------------------------------------------------------------- thresholdL_15 + signal_7->sp_1 + sp_0 thresholdL_15 + signal_7->sp_1 + sp_0 thresholdL_14 + signal_6->sp_3 + sp_2 thresholdL_14 + signal_6->sp_3 + sp_2 thresholdL_13 + signal_5->sp_5 + sp_4 thresholdL_13 + signal_5->sp_5 + sp_4 thresholdL_12 + signal_4->sp_7 + sp_6 thresholdL_12 + signal_4->sp_7 + sp_6 gateL_37 + signal_7<->sp_9 + sp_8 sp_9 + signal_23<->sp_10 + signal_7 gateL_36 + signal_7<->sp_9 + sp_11 gateL_35 + signal_7<->sp_9 + sp_12 gateL_34 + signal_6<->sp_14 + sp_13 sp_14 + signal_22<->sp_15 + signal_6 gateL_33 + signal_6<->sp_14 + sp_16 gateL_32 + signal_6<->sp_14 + sp_17 gateL_31 + signal_5<->sp_19 + sp_18 sp_19 + signal_21<->sp_20 + signal_5 gateL_30 + signal_5<->sp_19 + sp_21 gateL_29 + signal_5<->sp_19 + sp_22 gateL_28 + signal_4<->sp_24 + sp_23 sp_24 + signal_20<->sp_25 + signal_4 gateL_27 + signal_4<->sp_24 + sp_26 gateL_26 + signal_4<->sp_24 + sp_27 gateL_16 + sp_13<->sp_30 + sp_28 gateL_16 + sp_23<->sp_29 + sp_28 thresholdL_7 + sp_28->sp_34 + sp_33 thresholdL_7 + sp_28->sp_34 + sp_33 gateL_17 + sp_28<->sp_32 + sp_31 sp_32 + signal_15<->sp_35 + sp_28 gateL_22 + sp_31<->sp_37 + sp_36 thresholdL_10 + sp_36->sp_41 + sp_40 thresholdL_10 + sp_36->sp_41 + sp_40 gateL_23 + sp_36<->sp_39 + sp_38 sp_39 + signal_18<->sp_42 + sp_36 reporter_2 + sp_38->sp_44 + sp_43 gateL_14 + sp_8<->sp_47 + sp_45 gateL_14 + sp_18<->sp_46 + sp_45 thresholdL_6 + sp_45->sp_51 + sp_50 thresholdL_6 + sp_45->sp_51 + sp_50 gateL_15 + sp_45<->sp_49 + sp_48 sp_49 + signal_14<->sp_52 + sp_45 gateL_24 + sp_48<->sp_54 + sp_53 thresholdL_11 + sp_53->sp_58 + sp_57 thresholdL_11 + sp_53->sp_58 + sp_57 gateL_25 + sp_53<->sp_56 + sp_55 sp_56 + signal_19<->sp_59 + sp_53 reporter_3 + sp_55->sp_61 + sp_60 gateL_12 + sp_11<->sp_64 + sp_62 gateL_12 + sp_21<->sp_63 + sp_62 thresholdL_5 + sp_62->sp_68 + sp_67 thresholdL_5 + sp_62->sp_68 + sp_67 gateL_13 + sp_62<->sp_66 + sp_65 sp_66 + signal_13<->sp_69 + sp_62 reporter_1 + sp_65->sp_71 + sp_70 gateL_10 + sp_16<->sp_74 + sp_72 gateL_10 + sp_26<->sp_73 + sp_72 thresholdL_4 + sp_72->sp_78 + sp_77 thresholdL_4 + sp_72->sp_78 + sp_77 gateL_11 + sp_72<->sp_76 + sp_75 sp_76 + signal_12<->sp_79 + sp_72 reporter + sp_75->sp_81 + sp_80 gateL_8 + sp_17<->sp_84 + sp_82 gateL_8 + sp_22<->sp_83 + sp_82 thresholdL_3 + sp_82->sp_88 + sp_87 thresholdL_3 + sp_82->sp_88 + sp_87 gateL_9 + sp_82<->sp_86 + sp_85 sp_86 + signal_11<->sp_89 + sp_82 gateL_20 + sp_85<->sp_91 + sp_90 thresholdL_9 + sp_90->sp_95 + sp_94 thresholdL_9 + sp_90->sp_95 + sp_94 gateL_21 + sp_90<->sp_93 + sp_92 sp_93 + signal_17<->sp_96 + sp_90 gateL_22 + sp_92<->sp_97 + sp_36 gateL_6 + sp_12<->sp_100 + sp_98 gateL_6 + sp_27<->sp_99 + sp_98 thresholdL_2 + sp_98->sp_104 + sp_103 thresholdL_2 + sp_98->sp_104 + sp_103 gateL_7 + sp_98<->sp_102 + sp_101 sp_102 + signal_10<->sp_105 + sp_98 gateL_18 + sp_101<->sp_107 + sp_106 thresholdL_8 + sp_106->sp_111 + sp_110 thresholdL_8 + sp_106->sp_111 + sp_110 gateL_19 + sp_106<->sp_109 + sp_108 sp_109 + signal_16<->sp_112 + sp_106 gateL_24 + sp_108<->sp_113 + sp_53 gateL_3 + signal_2<->sp_116 + sp_114 gateL_3 + signal<->sp_115 + sp_114 thresholdL_1 + sp_114->sp_121 + sp_120 thresholdL_1 + sp_114->sp_121 + sp_120 gateL_5 + sp_114<->sp_118 + sp_119 gateL_4 + sp_114<->sp_118 + sp_117 sp_118 + signal_9<->sp_122 + sp_114 gateL_20 + sp_119<->sp_123 + sp_90 gateL_14 + sp_117<->sp_124 + sp_45 gateL + signal_3<->sp_127 + sp_125 gateL + signal_1<->sp_126 + sp_125 thresholdL + sp_125->sp_132 + sp_131 thresholdL + sp_125->sp_132 + sp_131 gateL_2 + sp_125<->sp_129 + sp_130 gateL_1 + sp_125<->sp_129 + sp_128 sp_129 + signal_8<->sp_133 + sp_125 gateL_18 + sp_130<->sp_134 + sp_106 gateL_16 + sp_128<->sp_135 + sp_28 //-------------------------------------------------------------------------- //Property definitions //-------------------------------------------------------------------------- let $invariant := { sp_60 + reporter_3 = 75 and sp_127 + signal_3 = 5 and sp_24 + sp_7 + signal_4 = 5 and sp_6 + thresholdL_12 = 10 and sp_99 + sp_27 + gateL_26 = 50 and sp_73 + sp_26 + gateL_27 = 50 and sp_29 + sp_23 + gateL_28 = 50 and sp_25 + signal_20 = 300 and sp_19 + sp_5 + signal_5 = 45 and sp_4 + thresholdL_13 = 10 and sp_83 + sp_22 + gateL_29 = 50 and sp_63 + sp_21 + gateL_30 = 50 and sp_46 + sp_18 + gateL_31 = 50 and sp_20 + signal_21 = 300 and sp_14 + sp_3 + signal_6 = 45 and sp_2 + thresholdL_14 = 10 and sp_84 + sp_17 + gateL_32 = 50 and sp_74 + sp_16 + gateL_33 = 50 and sp_30 + sp_13 + gateL_34 = 50 and sp_15 + signal_22 = 300 and sp_9 + sp_1 + signal_7 = 5 and sp_0 + thresholdL_15 = 10 and sp_100 + sp_12 + gateL_35 = 50 and sp_64 + sp_11 + gateL_36 = 50 and sp_47 + sp_8 + gateL_37 = 50 and sp_10 + signal_23 = 300 and sp_129 + sp_132 + sp_125 + gateL = 100 and sp_131 + thresholdL = 30 and sp_135 + sp_128 + gateL_1 = 50 and sp_134 + sp_130 + gateL_2 = 50 and sp_133 + signal_8 = 200 and sp_118 + sp_121 + sp_114 + gateL_3 = 100 and sp_120 + thresholdL_1 = 60 and sp_124 + sp_117 + gateL_4 = 50 and sp_123 + sp_119 + gateL_5 = 50 and sp_122 + signal_9 = 200 and sp_102 + sp_104 + sp_98 + gateL_6 = 100 and sp_103 + thresholdL_2 = 30 and sp_107 + sp_101 + gateL_7 = 50 and sp_105 + signal_10 = 100 and sp_86 + sp_88 + sp_82 + gateL_8 = 100 and sp_87 + thresholdL_3 = 60 and sp_91 + sp_85 + gateL_9 = 50 and sp_89 + signal_11 = 100 and sp_76 + sp_78 + sp_72 + gateL_10 = 100 and sp_77 + thresholdL_4 = 60 and sp_81 + sp_75 + gateL_11 = 50 and sp_79 + signal_12 = 100 and sp_66 + sp_68 + sp_62 + gateL_12 = 100 and sp_67 + thresholdL_5 = 30 and sp_71 + sp_65 + gateL_13 = 50 and sp_69 + signal_13 = 100 and sp_49 + sp_51 + sp_45 + gateL_14 = 150 and sp_50 + thresholdL_6 = 110 and sp_54 + sp_48 + gateL_15 = 50 and sp_52 + signal_14 = 100 and sp_32 + sp_34 + sp_28 + gateL_16 = 150 and sp_33 + thresholdL_7 = 30 and sp_37 + sp_31 + gateL_17 = 50 and sp_35 + signal_15 = 100 and sp_109 + sp_111 + sp_106 + gateL_18 = 100 and sp_110 + thresholdL_8 = 60 and sp_113 + sp_108 + gateL_19 = 50 and sp_112 + signal_16 = 100 and sp_93 + sp_95 + sp_90 + gateL_20 = 100 and sp_94 + thresholdL_9 = 30 and sp_97 + sp_92 + gateL_21 = 50 and sp_96 + signal_17 = 100 and sp_39 + sp_41 + sp_36 + gateL_22 = 100 and sp_40 + thresholdL_10 = 60 and sp_44 + sp_38 + gateL_23 = 50 and sp_42 + signal_18 = 100 and sp_56 + sp_58 + sp_53 + gateL_24 = 100 and sp_57 + thresholdL_11 = 30 and sp_61 + sp_55 + gateL_25 = 50 and sp_59 + signal_19 = 100 and sp_80 + reporter = 75 and sp_70 + reporter_1 = 75 and sp_43 + reporter_2 = 75 and sp_115 + signal = 45 and sp_126 + signal_1 = 5 and sp_116 + signal_2 = 45 and sp_7 + thresholdL_12 = 10 and sp_5 + thresholdL_13 = 10 and sp_3 + thresholdL_14 = 10 and sp_1 + thresholdL_15 = 10 and sp_132 + thresholdL = 30 and sp_121 + thresholdL_1 = 60 and sp_104 + thresholdL_2 = 30 and sp_88 + thresholdL_3 = 60 and sp_78 + thresholdL_4 = 60 and sp_68 + thresholdL_5 = 30 and sp_51 + thresholdL_6 = 110 and sp_34 + thresholdL_7 = 30 and sp_111 + thresholdL_8 = 60 and sp_95 + thresholdL_9 = 30 and sp_41 + thresholdL_10 = 60 and sp_58 + thresholdL_11 = 30 and sp_61 + reporter_3 = 75 and gateL_26 + gateL_27 + sp_25 + sp_24 + gateL_28 = 150 and gateL_29 + gateL_30 + sp_20 + sp_19 + gateL_31 = 150 and gateL_32 + gateL_33 + sp_15 + sp_14 + gateL_34 = 150 and gateL_35 + gateL_36 + sp_10 + sp_9 + gateL_37 = 150 and sp_126 + sp_127 + gateL = 100 and sp_133 + sp_129 + gateL_1 + gateL_2 = 100 and sp_115 + sp_116 + gateL_3 = 100 and sp_122 + sp_118 + gateL_4 + gateL_5 = 100 and sp_99 + sp_100 + gateL_6 = 100 and sp_105 + sp_102 + gateL_7 = 50 and sp_83 + sp_84 + gateL_8 = 100 and sp_89 + sp_86 + gateL_9 = 50 and sp_73 + sp_74 + gateL_10 = 100 and sp_79 + sp_76 + gateL_11 = 50 and sp_63 + sp_64 + gateL_12 = 100 and sp_69 + sp_66 + gateL_13 = 50 and sp_124 + sp_46 + sp_47 + gateL_14 = 150 and sp_52 + sp_49 + gateL_15 = 50 and sp_135 + sp_29 + sp_30 + gateL_16 = 150 and sp_35 + sp_32 + gateL_17 = 50 and sp_134 + sp_107 + gateL_18 = 100 and sp_112 + sp_109 + gateL_19 = 50 and sp_123 + sp_91 + gateL_20 = 100 and sp_96 + sp_93 + gateL_21 = 50 and sp_97 + sp_37 + gateL_22 = 100 and sp_42 + sp_39 + gateL_23 = 50 and sp_113 + sp_54 + gateL_24 = 100 and sp_59 + sp_56 + gateL_25 = 50 and sp_81 + reporter = 75 and sp_71 + reporter_1 = 75 and sp_44 + reporter_2 = 75 }; let $init := { signal_3 = 5 and sp_127 = 0 and signal_4 = 5 and sp_24 = 0 and sp_7 = 0 and sp_27 = 0 and sp_26 = 0 and sp_23 = 0 and signal_20 = 300 and sp_6 = 0 and sp_99 = 0 and sp_73 = 0 and sp_29 = 0 and signal_5 = 45 and sp_19 = 0 and sp_5 = 0 and sp_22 = 0 and sp_21 = 0 and sp_18 = 0 and signal_21 = 300 and sp_4 = 0 and sp_83 = 0 and sp_63 = 0 and sp_46 = 0 and signal_6 = 45 and sp_14 = 0 and sp_3 = 0 and sp_17 = 0 and sp_16 = 0 and sp_13 = 0 and signal_22 = 300 and sp_2 = 0 and sp_84 = 0 and sp_74 = 0 and sp_30 = 0 and signal_7 = 5 and sp_9 = 0 and sp_1 = 0 and sp_12 = 0 and sp_11 = 0 and sp_8 = 0 and signal_23 = 300 and sp_0 = 0 and sp_100 = 0 and sp_64 = 0 and sp_47 = 0 and sp_125 = 0 and sp_129 = 0 and sp_132 = 0 and sp_128 = 0 and sp_130 = 0 and signal_8 = 200 and sp_131 = 0 and sp_135 = 0 and sp_134 = 0 and sp_114 = 0 and sp_118 = 0 and sp_121 = 0 and sp_117 = 0 and sp_119 = 0 and signal_9 = 200 and sp_120 = 0 and sp_124 = 0 and sp_123 = 0 and sp_98 = 0 and sp_102 = 0 and sp_104 = 0 and sp_101 = 0 and signal_10 = 100 and sp_103 = 0 and sp_107 = 0 and sp_82 = 0 and sp_86 = 0 and sp_88 = 0 and sp_85 = 0 and signal_11 = 100 and sp_87 = 0 and sp_91 = 0 and sp_72 = 0 and sp_76 = 0 and sp_78 = 0 and sp_75 = 0 and signal_12 = 100 and sp_77 = 0 and sp_81 = 0 and sp_62 = 0 and sp_66 = 0 and sp_68 = 0 and sp_65 = 0 and signal_13 = 100 and sp_67 = 0 and sp_71 = 0 and sp_45 = 0 and sp_49 = 0 and sp_51 = 0 and sp_48 = 0 and signal_14 = 100 and sp_50 = 0 and sp_54 = 0 and sp_28 = 0 and sp_32 = 0 and sp_34 = 0 and sp_31 = 0 and signal_15 = 100 and sp_33 = 0 and sp_37 = 0 and sp_106 = 0 and sp_109 = 0 and sp_111 = 0 and sp_108 = 0 and signal_16 = 100 and sp_110 = 0 and sp_113 = 0 and sp_90 = 0 and sp_93 = 0 and sp_95 = 0 and sp_92 = 0 and signal_17 = 100 and sp_94 = 0 and sp_97 = 0 and sp_36 = 0 and sp_39 = 0 and sp_41 = 0 and sp_38 = 0 and signal_18 = 100 and sp_40 = 0 and sp_44 = 0 and sp_53 = 0 and sp_56 = 0 and sp_58 = 0 and sp_55 = 0 and signal_19 = 100 and sp_57 = 0 and sp_61 = 0 and sp_80 = 0 and sp_70 = 0 and sp_43 = 0 and sp_60 = 0 and signal = 45 and sp_115 = 0 and signal_1 = 5 and sp_126 = 0 and signal_2 = 45 and sp_116 = 0 and thresholdL_12 = 10 and thresholdL_13 = 10 and thresholdL_14 = 10 and thresholdL_15 = 10 and thresholdL = 30 and thresholdL_1 = 60 and thresholdL_2 = 30 and thresholdL_3 = 60 and thresholdL_4 = 60 and thresholdL_5 = 30 and thresholdL_6 = 110 and thresholdL_7 = 30 and thresholdL_8 = 60 and thresholdL_9 = 30 and thresholdL_10 = 60 and thresholdL_11 = 30 and gateL_26 = 50 and gateL_27 = 50 and gateL_28 = 50 and sp_25 = 0 and gateL_29 = 50 and gateL_30 = 50 and gateL_31 = 50 and sp_20 = 0 and gateL_32 = 50 and gateL_33 = 50 and gateL_34 = 50 and sp_15 = 0 and gateL_35 = 50 and gateL_36 = 50 and gateL_37 = 50 and sp_10 = 0 and gateL = 100 and gateL_1 = 50 and gateL_2 = 50 and sp_133 = 0 and gateL_3 = 100 and gateL_4 = 50 and gateL_5 = 50 and sp_122 = 0 and gateL_6 = 100 and gateL_7 = 50 and sp_105 = 0 and gateL_8 = 100 and gateL_9 = 50 and sp_89 = 0 and gateL_10 = 100 and gateL_11 = 50 and sp_79 = 0 and gateL_12 = 100 and gateL_13 = 50 and sp_69 = 0 and gateL_14 = 150 and gateL_15 = 50 and sp_52 = 0 and gateL_16 = 150 and gateL_17 = 50 and sp_35 = 0 and gateL_18 = 100 and gateL_19 = 50 and sp_112 = 0 and gateL_20 = 100 and gateL_21 = 50 and sp_96 = 0 and gateL_22 = 100 and gateL_23 = 50 and sp_42 = 0 and gateL_24 = 100 and gateL_25 = 50 and sp_59 = 0 and reporter = 75 and reporter_1 = 75 and reporter_2 = 75 and reporter_3 = 75 }; let $no_rxn_enabled := { ( thresholdL_15<1 or signal_7<1) and ( thresholdL_15<1 or signal_7<1) and ( thresholdL_14<1 or signal_6<1) and ( thresholdL_14<1 or signal_6<1) and ( thresholdL_13<1 or signal_5<1) and ( thresholdL_13<1 or signal_5<1) and ( thresholdL_12<1 or signal_4<1) and ( thresholdL_12<1 or signal_4<1) and ( gateL_37<1 or signal_7<1) and ( sp_9<1 or sp_8<1) and ( sp_9<1 or signal_23<1) and ( sp_10<1 or signal_7<1) and ( gateL_36<1 or signal_7<1) and ( sp_9<1 or sp_11<1) and ( gateL_35<1 or signal_7<1) and ( sp_9<1 or sp_12<1) and ( gateL_34<1 or signal_6<1) and ( sp_14<1 or sp_13<1) and ( sp_14<1 or signal_22<1) and ( sp_15<1 or signal_6<1) and ( gateL_33<1 or signal_6<1) and ( sp_14<1 or sp_16<1) and ( gateL_32<1 or signal_6<1) and ( sp_14<1 or sp_17<1) and ( gateL_31<1 or signal_5<1) and ( sp_19<1 or sp_18<1) and ( sp_19<1 or signal_21<1) and ( sp_20<1 or signal_5<1) and ( gateL_30<1 or signal_5<1) and ( sp_19<1 or sp_21<1) and ( gateL_29<1 or signal_5<1) and ( sp_19<1 or sp_22<1) and ( gateL_28<1 or signal_4<1) and ( sp_24<1 or sp_23<1) and ( sp_24<1 or signal_20<1) and ( sp_25<1 or signal_4<1) and ( gateL_27<1 or signal_4<1) and ( sp_24<1 or sp_26<1) and ( gateL_26<1 or signal_4<1) and ( sp_24<1 or sp_27<1) and ( gateL_16<1 or sp_13<1) and ( sp_30<1 or sp_28<1) and ( gateL_16<1 or sp_23<1) and ( sp_29<1 or sp_28<1) and ( thresholdL_7<1 or sp_28<1) and ( thresholdL_7<1 or sp_28<1) and ( gateL_17<1 or sp_28<1) and ( sp_32<1 or sp_31<1) and ( sp_32<1 or signal_15<1) and ( sp_35<1 or sp_28<1) and ( gateL_22<1 or sp_31<1) and ( sp_37<1 or sp_36<1) and ( thresholdL_10<1 or sp_36<1) and ( thresholdL_10<1 or sp_36<1) and ( gateL_23<1 or sp_36<1) and ( sp_39<1 or sp_38<1) and ( sp_39<1 or signal_18<1) and ( sp_42<1 or sp_36<1) and ( reporter_2<1 or sp_38<1) and ( gateL_14<1 or sp_8<1) and ( sp_47<1 or sp_45<1) and ( gateL_14<1 or sp_18<1) and ( sp_46<1 or sp_45<1) and ( thresholdL_6<1 or sp_45<1) and ( thresholdL_6<1 or sp_45<1) and ( gateL_15<1 or sp_45<1) and ( sp_49<1 or sp_48<1) and ( sp_49<1 or signal_14<1) and ( sp_52<1 or sp_45<1) and ( gateL_24<1 or sp_48<1) and ( sp_54<1 or sp_53<1) and ( thresholdL_11<1 or sp_53<1) and ( thresholdL_11<1 or sp_53<1) and ( gateL_25<1 or sp_53<1) and ( sp_56<1 or sp_55<1) and ( sp_56<1 or signal_19<1) and ( sp_59<1 or sp_53<1) and ( reporter_3<1 or sp_55<1) and ( gateL_12<1 or sp_11<1) and ( sp_64<1 or sp_62<1) and ( gateL_12<1 or sp_21<1) and ( sp_63<1 or sp_62<1) and ( thresholdL_5<1 or sp_62<1) and ( thresholdL_5<1 or sp_62<1) and ( gateL_13<1 or sp_62<1) and ( sp_66<1 or sp_65<1) and ( sp_66<1 or signal_13<1) and ( sp_69<1 or sp_62<1) and ( reporter_1<1 or sp_65<1) and ( gateL_10<1 or sp_16<1) and ( sp_74<1 or sp_72<1) and ( gateL_10<1 or sp_26<1) and ( sp_73<1 or sp_72<1) and ( thresholdL_4<1 or sp_72<1) and ( thresholdL_4<1 or sp_72<1) and ( gateL_11<1 or sp_72<1) and ( sp_76<1 or sp_75<1) and ( sp_76<1 or signal_12<1) and ( sp_79<1 or sp_72<1) and ( reporter<1 or sp_75<1) and ( gateL_8<1 or sp_17<1) and ( sp_84<1 or sp_82<1) and ( gateL_8<1 or sp_22<1) and ( sp_83<1 or sp_82<1) and ( thresholdL_3<1 or sp_82<1) and ( thresholdL_3<1 or sp_82<1) and ( gateL_9<1 or sp_82<1) and ( sp_86<1 or sp_85<1) and ( sp_86<1 or signal_11<1) and ( sp_89<1 or sp_82<1) and ( gateL_20<1 or sp_85<1) and ( sp_91<1 or sp_90<1) and ( thresholdL_9<1 or sp_90<1) and ( thresholdL_9<1 or sp_90<1) and ( gateL_21<1 or sp_90<1) and ( sp_93<1 or sp_92<1) and ( sp_93<1 or signal_17<1) and ( sp_96<1 or sp_90<1) and ( gateL_22<1 or sp_92<1) and ( sp_97<1 or sp_36<1) and ( gateL_6<1 or sp_12<1) and ( sp_100<1 or sp_98<1) and ( gateL_6<1 or sp_27<1) and ( sp_99<1 or sp_98<1) and ( thresholdL_2<1 or sp_98<1) and ( thresholdL_2<1 or sp_98<1) and ( gateL_7<1 or sp_98<1) and ( sp_102<1 or sp_101<1) and ( sp_102<1 or signal_10<1) and ( sp_105<1 or sp_98<1) and ( gateL_18<1 or sp_101<1) and ( sp_107<1 or sp_106<1) and ( thresholdL_8<1 or sp_106<1) and ( thresholdL_8<1 or sp_106<1) and ( gateL_19<1 or sp_106<1) and ( sp_109<1 or sp_108<1) and ( sp_109<1 or signal_16<1) and ( sp_112<1 or sp_106<1) and ( gateL_24<1 or sp_108<1) and ( sp_113<1 or sp_53<1) and ( gateL_3<1 or signal_2<1) and ( sp_116<1 or sp_114<1) and ( gateL_3<1 or signal<1) and ( sp_115<1 or sp_114<1) and ( thresholdL_1<1 or sp_114<1) and ( thresholdL_1<1 or sp_114<1) and ( gateL_5<1 or sp_114<1) and ( sp_118<1 or sp_119<1) and ( gateL_4<1 or sp_114<1) and ( sp_118<1 or sp_117<1) and ( sp_118<1 or signal_9<1) and ( sp_122<1 or sp_114<1) and ( gateL_20<1 or sp_119<1) and ( sp_123<1 or sp_90<1) and ( gateL_14<1 or sp_117<1) and ( sp_124<1 or sp_45<1) and ( gateL<1 or signal_3<1) and ( sp_127<1 or sp_125<1) and ( gateL<1 or signal_1<1) and ( sp_126<1 or sp_125<1) and ( thresholdL<1 or sp_125<1) and ( thresholdL<1 or sp_125<1) and ( gateL_2<1 or sp_125<1) and ( sp_129<1 or sp_130<1) and ( gateL_1<1 or sp_125<1) and ( sp_129<1 or sp_128<1) and ( sp_129<1 or signal_8<1) and ( sp_133<1 or sp_125<1) and ( gateL_18<1 or sp_130<1) and ( sp_134<1 or sp_106<1) and ( gateL_16<1 or sp_128<1) and ( sp_135<1 or sp_28<1) }; let $no_reactive_species := { thresholdL_15 = 0 and thresholdL_14 = 0 and thresholdL_13 = 0 and thresholdL_12 = 0 and thresholdL_11 = 0 and thresholdL_10 = 0 and thresholdL_9 = 0 and thresholdL_8 = 0 and thresholdL_7 = 0 and thresholdL_6 = 0 and thresholdL_5 = 0 and thresholdL_4 = 0 and thresholdL_3 = 0 and thresholdL_2 = 0 and thresholdL_1 = 0 and thresholdL = 0 and signal_23 = 0 and signal_22 = 0 and signal_21 = 0 and signal_20 = 0 and signal_19 = 0 and signal_18 = 0 and signal_17 = 0 and signal_16 = 0 and signal_15 = 0 and signal_14 = 0 and signal_13 = 0 and signal_12 = 0 and signal_11 = 0 and signal_10 = 0 and signal_9 = 0 and signal_8 = 0 and signal_7 = 0 and signal_6 = 0 and signal_5 = 0 and signal_4 = 0 and signal_3 = 0 and signal_2 = 0 and signal_1 = 0 and signal = 0 and reporter_3 = 0 and reporter_2 = 0 and reporter_1 = 0 and reporter = 0 and gateL_37 = 0 and gateL_36 = 0 and gateL_35 = 0 and gateL_34 = 0 and gateL_33 = 0 and gateL_32 = 0 and gateL_31 = 0 and gateL_30 = 0 and gateL_29 = 0 and gateL_28 = 0 and gateL_27 = 0 and gateL_26 = 0 and gateL_25 = 0 and gateL_24 = 0 and gateL_23 = 0 and gateL_22 = 0 and gateL_21 = 0 and gateL_20 = 0 and gateL_19 = 0 and gateL_18 = 0 and gateL_17 = 0 and gateL_16 = 0 and gateL_15 = 0 and gateL_14 = 0 and gateL_13 = 0 and gateL_12 = 0 and gateL_11 = 0 and gateL_10 = 0 and gateL_9 = 0 and gateL_8 = 0 and gateL_7 = 0 and gateL_6 = 0 and gateL_5 = 0 and gateL_4 = 0 and gateL_3 = 0 and gateL_2 = 0 and gateL_1 = 0 and gateL = 0 }; http://rise4fun.com/Z34Biology/met_regulationmet_regulation//Regulatory network of E. coli metabolism model // // Originally studied in //"The regulatory network of E. coli metabolism as a Boolean dynamical system exhibits both homeostasis and exibility of response." //A. Samal and S. Jain. //BMC Systems Biology, 2(1):21, 2008. //Settings: directive constantInputs directive constEncoding BitVector //Specification: //To check for oscillations, search for a cycle of any length. lasso(#path,8); //Model: nhaA' = ((NhaR) or (RpoS)) thrA' = (not (thr-L(e) > 0 or ile-L(e) > 0)) thrB' = (not (thr-L(e) > 0 or ile-L(e) > 0)) thrC' = (not (thr-L(e) > 0 or ile-L(e) > 0)) yaaJ' = talB' = nhaR' = (na1(e) > 0) ribF' = lytB' = dapB' = (not lys-L(e) > 0) carA' = (not ArgR) carB' = (not ArgR) caiF' = (Fnr and Crp and not NarL) caiD' = (Crp and CaiF) caiB' = (Crp and CaiF) caiT' = (Crp and CaiF) folA' = apaH' = pdxA' = (RpoE) araD' = (AraC or (AraC and Crp)) araA' = (AraC or (AraC and Crp)) araB' = (AraC or (AraC and Crp)) araC' = (arab-L(e) > 0) sfuC' = sfuB' = sfuA' = leuD' = (not(leu-L(e) > 0) or Lrp) leuC' = (not(leu-L(e) > 0) or Lrp) leuB' = (not(leu-L(e) > 0) or Lrp) leuA' = (not(leu-L(e) > 0) or Lrp) ilvI' = (Lrp and not (leu-L(e) > 0)) ilvH' = (Lrp and not (leu-L(e) > 0)) fruR' = true murE' = murF' = mraY' = murD' = murG' = murC' = ddlB' = lpxC' = mutT' = guaC' = (not ((gln-L(e) > 0) or (gua(e) > 0))) nadC' = aroP' = (not (TyrR and ((phe-L(e)>0) or (tyr-L(e)>0) or (trp-L(e)>0)))) pdhR' = true aceE' = ((not(PdhR)) or (Fis)) aceF' = ((not(PdhR)) or (Fis)) lpdA' = (true) acnB' = (true) speD' = speE' = gcd' = (not Crp) hpt' = (Crp) yadF' = pand' = panC' = panB' = folK' = hemL' = yadT' = mtn' = dgt' = sdaR' = ((glcr(e)>0) or (galct-D(e)>0)) dapD' = glnD' = (Lrp) pyrH' = dxr' = uppS' = cdsA' = lpxD' = fabZ' = true lpxA' = lpxB' = accA' = ldcC' = yaeC' = (not MetJ) yaeE' = (not MetJ) abc' = (not MetJ) yaeD' = yafB' = gloB' = fadF' = (not (FaDR2) or not (ArcA)) gmhA' = gpt' = proB' = proA' = argF' = (not ArgR) betB' = (not (ArcA or BetI)) betI' = (chol(e) > 0) betT' = (not (BetI)) yahI' = prpB' = (ppa(e)>0) prpC' = (ppa(e)>0) prpD' = (ppa(e)>0) prpE' = (ppa(e)>0) codB' = (not (PurR) or (NRI_hi)) codA' = (not (PurR) or NRI_hi) cynR' = (cynt(e)>0) cynT' = cynS' = (CynR) cynX' = (cynt(e)>0) lacY' = ((not((glcn(e) > 0) or (glc-D(e) > 0))) and not(LacI)) lacZ' = ((not((glcn(e) > 0) or (glc-D(e) > 0))) and not(LacI)) lacI' = ( not ( lcts(e)>0 ) ) mhpR' = (3hPppn(e)>0) mhpA' = (MhpR) mhpB' = (MhpR) mhpC' = (MhpR) mhpD' = (MhpR) mhpF' = (MhpR) mhpE' = (MhpR) mhpT' = adhC' = tauA' = (Cbl and CysB) tauB' = (Cbl and CysB) tauC' = (Cbl and CysB) tauD' = (Cbl and CysB) hemB' = ddlA' = proC' = aroL' = (not( (TyrR and (tyr-L(e)>0)) or (TyrR and (tyr-L(e)>0) and TrpR) )) phoB' = (Phor) phor' = (not (pi(e) > 0)) brnQ' = malZ' = (MalT) ribD' = ribH' = thiL' = pgpA' = dxs' = ispA' = thiI' = panE' = cyoE' = (not (ArcA or Fnr)) cyoD' = (not (ArcA or Fnr)) cyoC' = (not (ArcA or Fnr)) cyoB' = (not (ArcA or Fnr)) cyoA' = (not (ArcA or Fnr)) amtB' = apt' = adk' = hemH' = gsk' = ushA' = ybaS' = ybbS' = (not(ox2(e)>0) and not AllR and not (nh4(e)>0)) allA' = (not AllR) allR' = (false) gcl' = (not AllR) hyi' = glxR' = (not AllR) allP' = allB' = (not AllR) glxK' = (not AllR) allC' = (AllS) arcC' = purK' = (not (PurR)) purE' = (not (PurR)) folD' = appY' = (not CitB) pheP' = entD' = (not (Fur)) entF' = entC' = (not (Fur)) entE' = (not (Fur)) entB' = (not (Fur)) entA' = (not (Fur)) citT' = (CitB and (not (ox2(e) > 0))) citF' = (CitB) citE' = (CitB) citD' = (CitB) dpiB' = (cit(e)>0) dpiA' = (CitA) dcuC' = (Fnr or ArcA) phpB' = nadD' = gltL' = (not (glc-D(e) > 0)) gltK' = (not (glc-D(e) > 0)) gltJ' = (not (glc-D(e) > 0)) gltI' = (not (glc-D(e) > 0)) ubiF' = asnB' = nagC' = (not((acGam(e) > 0) or AGDC(e)>0)) nagA' = (not (NagC)) nagB' = (not (NagC) or (gam(e)>0)) nagE' = (not (NagC)) fur' = ((fe2(e) > 0) and (OxyR or SoxS)) pgm' = potE' = speF' = kdpE' = (KdpD) kdpD' = (not (k(e) > 0)) kdpC' = (KdpE) kdpB' = (KdpE) kdpA' = (KdpE) gltA' = sdhC' = (not((ArcA) or (Fnr)) or (Crp) or (Fis)) sdhD' = (not((ArcA) or (Fnr)) or (Crp) or (Fis)) sdhA' = (not((ArcA) or (Fnr)) or (Crp) or (Fis)) sdhB' = (not((ArcA) or (Fnr)) or (Crp) or (Fis)) sucA' = sucB' = sucC' = sucD' = cydA' = ((not Fnr) or (ArcA)) cydB' = ((not Fnr) or (ArcA)) nadA' = pnuC' = aroG' = ( not(( (phe-L(e)>0) or (trp-L(e)>0) ) and TyrR )) gpmA' = galK' = (not(glc-D(e) > 0) and (not(GalR or GalS)) or not (Rob)) galT' = (not(glc-D(e) > 0) and (not(GalR or GalS)) or not (Rob)) galE' = (not(glc-D(e) > 0) and (not(GalR or GalS)) or not (Rob)) bioA' = (not (BirA)) bioB' = (not (BirA)) bioF' = (not (BirA)) bioD' = (not (BirA)) glnQ' = glnP' = glnH' = fsa' = ybiK' = deor' = (not PPM2(e)) potF' = potG' = potH' = potI' = artJ' = artM' = artQ' = artP' = ltaA' = poxB' = ((not (Growth(e) > 0)) and (RpoS)) trxB' = lrp' = (not leu-L(e) >0) dmsA' = (Fnr and not NarL) dmsB' = (Fnr and not NarL) dmsC' = (Fnr and not NarL) pflA' = (ArcA or Fnr and (Crp or not(NarL))) pflB' = (ArcA or Fnr and (Crp or not(NarL))) focA' = (ArcA or Fnr and (Crp or not (NarL))) serC' = (Lrp or (not (Crp))) aroA' = cmk' = lpxK' = kdsB' = aspC' = pncB' = (not (NadR)) pyrD' = ((not (csn(e) > 0)) or (gua(e) > 0) or not PurR) fabA' = true mgsA' = hyaA' = ((ArcA or Fnr) and (AppY)) hyaB' = ((ArcA or Fnr) and (AppY)) hyaC' = ((ArcA or Fnr) and (AppY)) torS' = (tmao(e)>0) torR' = (TorS) torC' = (TorR or not (NarL)) torA' = (TorR or not (NarL)) agp' = ycdG' = putA' = ( (pro-L(e) > 0) or Crp or Nac) putP' = ( (pro-L(e) > 0) or Crp or Nac) ycdW' = lpxL' = pyrC' = ((not (csn(e) > 0)) or (gua(e) > 0) or not PurR) fabH' = true fabD' = true fabG' = true fabF' = true pabC' = tmk' = ptsG' = (not(Mlc) or not(Cra)) ndh' = (not (Fnr)) potD' = potC' = potB' = potA' = purB' = (not (PurR)) icdA' = nhaB' = fadR' = ( glc-D(e) > 0 or not (ac(e) > 0 ) ) dadA' = (ala-L(e) > 0 and not Crp) dadX' = (((ala-L(e) > 0) or (ala-D(e) > 0)) and Crp) treA' = (RpoS) dhaH' = dhaK2' = dhaK1' = prsA' = (not PurR) ispE' = hemA' = kdsA' = chaA' = narL' = ((NO3(e)>0) or (NO2(e)>0)) narK' = (Fnr or NarL) narG' = (Fnr and NarL) narH' = (Fnr and NarL) narJ' = (Fnr and NarL) narI' = (Fnr and NarL) purU' = galU' = tdk' = adhE' = (not (ox2(e) > 0) or (not ((ox2(e) > 0) and (Cra))) or (Fis) or not (NarL) or (RpoS)) cls' = trpA' = (not TrpR) trpB' = (not TrpR) trpC' = (not TrpR) trpD' = (not TrpR) trpE' = (not TrpR) btuR' = cysB' = (not (cys-L(e) > 0)) acnA' = (SoxS) ribA' = pgpB' = pyrF' = fabI' = true ycjK' = aldH' = goaG' = tyrR' = ( (trp-L(e)>0) or (tyr-L(e)>0) or (phe-L(e)>0) ) fnr' = ( not ( ox2(e)>0 ) ) trkG' = ldhA' = feaR' = (Crp) feaB' = (FeaR) tynA' = (FeaB) paaK' = aldA' = gapC_2' = gapC_1' = ydcS' = ydcT' = ydcU' = ydcV' = narU' = fdnG' = (Fnr or NarL) fdnH' = (Fnr or NarL) fdnI' = (Fnr or NarL) sfcA' = xasA' = gadB' = ((not (Growth(e) > 0))) tam' = (not (Growth(e)>0)) uxaB' = (not ExuR) yneH' = ((not (glc-D(e) > 0) or ((nh4(e) > 0) and not Crp))) marA' = false speG' = mlc' = ( not ( glc-D(e)>0 ) ) pntB' = pntA' = arcD' = fumC' = (MarA or Rob or SoxS and (not(ArcA))) fumA' = (not(ArcA or Fnr)) manA' = malI' = (not (malt(e) > 0)) malX' = ((MalT and Crp) or MalT) malY' = (not (MalI)) add' = ((ade(e) > 0) or (hxan(e) > 0)) pdxY' = pdxH' = sodC' = (not(Growth(e)>0) and not Fnr) gloA' = sodB' = purR' = ((hxan(e) > 0) or (gua(e) > 0)) ribE' = pykF' = (not(Cra)) ydiB' = aroD' = pps' = (Cra) aroH' = (not TrpR) btuD' = btuC' = pfkB' = katE' = (not(Growth(e)>0)) nadE' = astE' = ((not(Growth(e)>0) and RpoS) or (NRI_hi and RpoN)) astB' = ((not(Growth(e)>0) and RpoS) or (NRI_hi and RpoN)) astD' = ((not(Growth(e)>0) and RpoS) or (NRI_hi and RpoN)) astA' = ((not(Growth(e)>0) and RpoS) or (NRI_hi and RpoN)) astC' = ((not(Growth(e)>0) and RpoS) or (NRI_hi and RpoN)) gdhA' = (not ((Nac) or (glu-L(e) > 0)) ) selD' = ansA' = pncA' = b1773' = gapA' = yeaV' = fadD' = (not (FaDR2) or not (ArcA)) pabB' = sdaA' = ((gly(e) > 0 or leu-L(e) > 0 or not (ox2(e) > 0)) and ((not Lrp) or (Lrp and leu-L(e) > 0))) manX' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0) or (sbt-D(e) > 0) or (lac-D(e) > 0))) or (not (Mlc))) manY' = (((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0) or (sbt-D(e) > 0) or (lac-D(e) > 0)))) or (not (Mlc))) manZ' = (((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0) or (sbt-D(e) > 0) or (lac-D(e) > 0)))) or (not (Mlc))) kdgR' = (not(2ddGxcn(e)>0) and not(MNNH(e)>0) and not(ALTRH(e)>0)) purT' = (not (PurR)) eda' = ((true) or (not (GntR))) edd' = (not (GntR)) zwf' = pykA' = msbB' = ntpA' = torZ' = torY' = otsA' = (RpoS) otsB' = (RpoS) araH_2' = (AraC or (AraC and Crp)) araH_1' = (AraC or (AraC and Crp)) araG' = (AraC or (AraC and Crp)) araF' = (AraC or (AraC and Crp)) tyrP' = (not(TyrR and (tyr-L(e)>0))) pgsA' = amn' = cbl' = (not ((so4(e) > 0) or (cys-L(e) > 0 )) and CysB ) nac' = (NRI_low and RpoN) cobT' = (cbi(e)>0) cobS' = (cbi(e)>0) cobU' = (cbi(e)>0) hisG' = hisD' = hisC' = hisB' = hisH' = hisA' = hisF' = hisI' = ugd' = gnd' = glf' = rfbC' = rfbA' = rfbD' = rfbB' = galF' = wcaK' = cpsG' = manC' = fcl' = gmd' = dcd' = udk' = (not ((thym(e) > 0) or (csn(e) > 0) or (ura(e) > 0))) gatR_1' = (not (galt(e) > 0)) gatR_2' = (not (galt(e) > 0)) gatD' = (not (GaTR)) gatC' = (not (GaTR)) gatB' = (not (GaTR)) gatA' = (not (GaTR)) gatZ' = (not (GaTR)) gatY' = (not (GaTR)) fbaB' = ((pyr(e)>0) or (lac-D(e)>0) and not(glc-D(e)>0)) thiD' = thiM' = yehW' = yehX' = yehY' = yehZ' = bglX' = dld' = cdd' = (Crp and not (CytR)) mglC' = (Crp and not (GalS)) mglA' = (Crp and not (GalS)) mglB' = (Crp and not (GalS)) galS' = ( not ( lcts(e)>0 ) or not (gal(e)>0) ) folE' = lysP' = fruA' = (not (Cra)) fruK' = (not (Cra)) fruB' = (not (Cra)) mqo' = (not ArcA) atoS' = (acAXc(e) > 0) atoC' = (AtoS) atoD' = (AtoC) atoA' = (AtoC) atoE' = (AtoC) atoB' = (AtoC) ubiG' = ((ox2(e) > 0) and Crp) nrdA' = (not (ArcA)) nrdB' = (not (ArcA)) glpQ' = ((not GlpR or Fnr) and Crp) glpT' = (not (GlpR) and Crp) glpA' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0))) and (Fnr or ArcA) and (not(GlpR))) glpB' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0))) and (Fnr or ArcA) and (not(GlpR))) glpC' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0))) and (Fnr or ArcA) and (not(GlpR))) menE' = menC' = menB' = menD' = menF' = nutrue' = (not (ArcA or Fnr) or NarL) nuoM' = (not (ArcA or Fnr) or NarL) nuoL' = (not (ArcA or Fnr) or NarL) nuoK' = (not (ArcA or Fnr) or NarL) nuoJ' = (not (ArcA or Fnr) or NarL) nuoI' = (not (ArcA or Fnr) or NarL) nuoH' = (not (ArcA or Fnr) or NarL) nuoG' = (not (ArcA or Fnr) or NarL) nuoF' = (not (ArcA or Fnr) or NarL) nuoE' = (not (ArcA or Fnr) or NarL) nuoC' = (not (ArcA or Fnr) or NarL) nuoB' = (not (ArcA or Fnr) or NarL) nuoA' = (not (ArcA or Fnr) or NarL) ackA' = pta' = hisP' = (not (lys-L(e) > 0)) hisM' = (not (lys-L(e) > 0)) hisQ' = (not (lys-L(e) > 0)) hisJ' = (not (lys-L(e) > 0)) argT' = (not (lys-L(e) > 0)) ubiX' = (not (PurR)) purF' = (not (PurR)) folC' = accD' = pdxB' = fabB' = true aroC' = fadL' = ((not (Crp or FadR or OmpR))) dsdC' = (ser-D(e) > 0) dsdA' = ((Crp and DsdC) or DsdC) lpxP' = glk' = nupC' = (Crp or not (CytR)) gltX' = xapR' = (xtsn(e) > 0) xapB' = (XapR) xapA' = (XapR) lig' = cysZ' = (CysB) cysK' = (CysB) ptsH' = (true) ptsI' = (true) crr' = (true) pdxK' = cysM' = (CysB) cysA' = (CysB) cysW' = (CysB) cysU' = (CysB) cysP' = (CysB) yfeV' = hemF' = eutC' = eutB' = eutD' = maeB' = talA' = tktB' = dapE' = purC' = (not (PurR)) dapA' = gcvR' = (not (gly(e) > 0)) focB' = (ArcA or Fnr and (Crp or not (NarL))) uraA' = upp' = purM' = (not (PurR)) purN' = (not (PurR)) guaA' = (not (PurR and Crp)) guaB' = (not (PurR and Crp)) gcpE' = ndk' = iscS' = suhB' = hcaT' = hcaR' = (pppn(e)>0) hcaE' = (HcaR) hcaF' = (HcaR) hcaC' = (HcaR) hcaB' = (HcaR) hcaD' = (HcaR) glyA' = (not (gly(e) > 0) or MetR or not (PurR)) glnB' = (Lrp) purL' = (not (PurR)) acpS' = pdxJ' = (RpoE) rpoE' = false nadB' = (not (NadR)) pssA' = kgtP' = pheA' = (not (phe-L(e)>0) ) tyrA' = ( not(( (phe-L(e)>0) or (tyr-L(e)>0) ) and TyrR )) aroF' = ( not(( (phe-L(e)>0) or (tyr-L(e)>0) ) and TyrR )) yfjB' = gabD' = gabT' = gabP' = nrdE' = nrdF' = proV' = proW' = proX' = luxS' = gshA' = yqaB' = srlA' = ((not GutR) and (not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0)))) srlE' = ((not GutR) and (not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0)))) srlB' = ((not GutR) and (not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0)))) srlD' = (GutM and (not GutR) and (not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0)))) gutM' = (true) srlR' = (not (sbt-D(e) > 0)) hycG' = (FhlA and RpoN and (not (ox2(e) > 0))) hycF' = (FhlA and RpoN and (not (ox2(e) > 0))) hycE' = (FhlA and RpoN and (not (ox2(e) > 0))) hycD' = (FhlA and RpoN and (not (ox2(e) > 0))) hycC' = (FhlA and RpoN and (not (ox2(e) > 0))) hycB' = (FhlA and RpoN and (not (ox2(e) > 0))) fhlA' = ((not (ox2(e) > 0)) and (not (NO3(e) > 0)) and (not (NO2(e) > 0)) and (not (tmao(e) > 0)) and (not (dmso(e) > 0)) and (for(e)>0)) ygbL' = rpoS' = (not (Growth(e) > 0)) ispF' = ispD' = cysC' = (CysB) cysN' = (CysB) cysD' = (CysB) cysH' = (CysB) cysI' = (CysB) cysJ' = (CysB) eno' = pyrG' = mazG' = gudD' = (SdaR) ygcY' = gudP' = sdaC' = (Crp or (not (Lrp) and (leu-L(e) > 0) and Crp)) sdaB' = (true) fucO' = (((((FucR) or (rmn(e) > 0)) and (not (ox2(e) > 0))) and Crp) or (((FucR) or (rmn(e) > 0)) and (not (ox2(e) > 0)))) fucA' = ((FucR and Crp) or FucR) fucP' = ((FucR and Crp) or FucR) fucI' = ((FucR and Crp) or FucR) fucK' = ((FucR and Crp) or FucR) fucR' = (fuc-L(e) > 0) gcvA' = (not GcvR) argA' = (not ArgR) thyA' = aas' = galR' = ( not ( lcts(e)>0 ) or not (gal(e)>0) ) lysA' = (LysR and not lys-L(e) > 0) lysR' = (not (lys-L(e) > 0)) araE' = (Crp) yqeA' = ygfP' = idi' = bglA' = gcvP' = ((Fis and not PdhR) and ((not(GcvR) and GcvA) or Lrp or not PurR)) gcvH' = ((Fis and not PdhR) and ((not(GcvR) and GcvA) or Lrp or not PurR)) gcvT' = ((Fis and not PdhR) and ((not(GcvR) and GcvA) or Lrp or not PurR)) ubiH' = serA' = rpiA' = sbm' = ygfG' = ygfH' = fbaA' = pgk' = (true) epd' = (Crp) tktA' = speB' = speA' = (not (PurR)) metK' = galP' = ((not (GalR)) or (GalS) and (Crp or not (Crp))) gshB' = ansB' = (Fnr and Crp) nupG' = (Crp or not (CytR) or not (Deor)) speC' = (not (Crp)) glcA' = (not ArcA and GlcC) glcB' = (not (ArcA) and (GlcC)) glcF' = glcD' = glcC' = ((ac(e)>0) or (glyclt(e)>0)) pitB' = (not (PhoB)) gsp' = hybC' = (FhlA and RpoN and (not (ox2(e) > 0))) hybO' = (FhlA and RpoN and (not (ox2(e) > 0))) metC' = (not MetJ) yqhE' = plsC' = ribB' = rfaE' = folB' = ttdA' = (not(ox2(e)>0) and (tartr-L(e)>0)) ttdB' = (not(ox2(e)>0) and (tartr-L(e)>0)) ygjE' = ygjG' = sstT' = uxaA' = (not ExuR) uxaC' = (not ExuR) exuT' = (not ExuR) exuR' = (not(GUI1(e)>0) and not(GUI2(e)>0) and not(MANAO(e)>0) and not(TAGURr(e)>0)) tdcGa' = (Crp or not(ox2(e)>0)) tdcGb' = (Crp or not(ox2(e)>0)) tdcE' = (Crp or Fnr or LysR or TdcA or not TdcR) tdcD' = (Crp or Fnr or LysR or TdcA or not TdcR) tdcC' = (Crp or Fnr or LysR or TdcA or not TdcR) tdcB' = (Crp or Fnr or LysR or TdcA or not TdcR) tdcA' = ((thr-L(e) > 0) and (ser-L(e) > 0) and (val-L(e) > 0) and (ile-L(e) > 0) and not (ox2(e) > 0)) tdcR' = ((thr-L(e) > 0) and (ser-L(e) > 0) and (val-L(e) > 0) and (ile-L(e) > 0) and not (ox2(e) > 0)) garK' = (SdaR) garR' = (SdaR) garL' = (SdaR) garP' = garD' = (SdaR) agaZ' = agaY' = mtr' = (not TrpR or (TyrR and ((phe-L(e)>0) or (tyr-L(e)>0)))) argG' = mrsA' = folP' = ispB' = murA' = rpoN' = (true) gltB' = ( (Lrp and not (leu-L(e) > 0)) or not(NRI_hi and ((glu-L(e) > 0) or (arg-L(e) > 0) or (asp-L(e) > 0) or (his-L(e) > 0) or (pro-L(e) > 0) ))) gltD' = ( (Lrp and not (leu-L(e) > 0)) or not(NRI_hi and ((glu-L(e) > 0) or (arg-L(e) > 0) or (asp-L(e) > 0) or (his-L(e) > 0) or (pro-L(e) > 0) ))) nanK' = nanE' = nanT' = nanA' = mdh' = (not(ArcA)) argR' = (arg-L(e) > 0) accB' = accC' = panF' = fis' = (Growth(e) > 0) acrE' = acrF' = aroE' = crp' = (not((glcn(e) > 0) or (glc-D(e) > 0))) argD' = (not ArgR) pabA' = nirB' = (Fnr and NarL) nirD' = (Fnr and NarL) nirC' = (Fnr and NarL) cysG' = (Fnr or NarL) yhfW' = gph' = rpe' = aroB' = aroK' = pckA' = ompR' = false feoB' = gntT' = (not (GntR) and (glcn(e) > 0)) malQ' = (MalT) malP' = (MalT) malT' = ((malt(e) > 0) or (malttr(e) > 0) or (maltttr(e) > 0) or (malthx(e) > 0) or (maltpt(e) >0)) glpR' = ( not ( glyc(e)>0 ) ) glpE' = (Crp) glpD' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0))) and (not(ArcA or GlpR))) glgP' = (Crp) glgA' = glgC' = asd' = gntK' = (not (GntR) and (glcn(e) > 0)) gntR' = (not (glcn(e) > 0)) ugpC' = (Crp or PhoB) ugpE' = (Crp or PhoB) ugpA' = (Crp or PhoB) ugpB' = (Crp or PhoB) livF' = (not(leu-L(e) > 0) or Lrp) livG' = (not(leu-L(e) > 0) or Lrp) livM' = (not(leu-L(e) > 0) or Lrp) livH' = (not(leu-L(e) > 0) or Lrp) livK' = (not(leu-L(e) > 0) or Lrp) livJ' = (not(leu-L(e) > 0) or Lrp) pitA' = gor' = (OxyR or RpoS) gadA' = ((not (Growth(e) > 0 ) and not Crp) ) treF' = (RpoS) kdgK' = (not KdgR) dctA' = ((((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0) or (sbt-D(e) > 0) or (lac-D(e) > 0) or (man(e) > 0)))) and not(ArcA) and (DcuR)) and RpoN) bisC' = yiaE' = xylB' = ((XylR and Crp) or XylR) xylA' = ((XylR and Crp) or XylR) xylF' = ((XylR and Crp) or XylR) xylG' = ((XylR and Crp) or XylR) xylH' = ((XylR and Crp) or XylR) xylR' = (xyl-D(e) > 0) avtA' = (not (ala-L(e) > 0 or leu-L(e) > 0 )) yiaJ' = (not (fuc-L(e)>0)) yiaK' = ((not YiaJ) and Crp) yiaO' = (Crp or YiaJ) sgbH' = (not YiaJ) sgbE' = (not YiaJ) aldB' = (RpoS and (Crp)) mtlA' = (not (MtlR)) mtlD' = (not MtlR) mtlR' = (not (mnl(e) > 0)) lldP' = (not (ArcA)) lldD' = (lac-L(e) > 0 and ox2(e) > 0) cysE' = (CysB) gpsA' = yibO' = tdh' = (not (Lrp) and (leu-L(e) > 0)) kbl' = (not (Lrp) and (leu-L(e) > 0)) rfaD' = rfaF' = rfaC' = rfaL' = rfaJ' = rfaI' = rfaG' = kdtA' = coaD' = dut' = pyrE' = (not (ura(e) > 0 or gua(e) > 0)) gmk' = gltS' = (asp-L(e) > 0) yicE' = yicP' = uhpT' = (Crp or UhpA) uhpB' = (g6p(e) > 0) uhpA' = (UhpB) ilvN' = (not(leu-L(e) > 0 or val-L(e) > 0) and Crp) ilvB' = (not(leu-L(e) > 0 or val-L(e) > 0) and Crp) dgoT' = (galctn-D(e)>0) dgoA' = (galctn-D(e)>0) dgoK' = (galctn-D(e)>0) tnaA' = (Crp and (trp-L(e)>0 or cys-L(e) > 0) ) tnaB' = (Crp and (trp-L(e)>0) ) pstB' = (PhoB) pstA' = (PhoB) pstC' = (PhoB) pstS' = (PhoB) glmS' = glmU' = (NagC) atpC' = atpD' = atpG' = atpA' = atpH' = atpF' = atpE' = atpB' = atpI' = asnC' = ( not ( asn-L(e) > 0 ) and NRI_hi ) asnA' = (not (asn-L(e) > 0) and AsnC) rbsD' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0))) and not(RbsR)) rbsA' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0))) and not(RbsR)) rbsC' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0))) and not(RbsR)) rbsB' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0))) and not(RbsR)) rbsK' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0))) and not(RbsR)) rbsR' = ( not ( rib-D(e)>0 ) ) ilvG_1' = (not(leu-L(e) > 0 or ile-L(e) > 0 or val-L(e) > 0) and Lrp) ilvG_2' = (not(leu-L(e) > 0 or ile-L(e) > 0 or val-L(e) > 0) and Lrp) ilvM' = (not(leu-L(e) > 0 or ile-L(e) > 0 or val-L(e) > 0) and Lrp) ilvE' = ilvD' = ilvA' = ilvY' = (not val-L(e) > 0 ) ilvC' = (IlvY) wecA' = wecB' = wecC' = rffG' = rffH' = wecD' = wecE' = wecF' = wecG' = hemX' = hemD' = hemC' = cyaA' = (not Crp) dapF' = pldA' = pldB' = metR' = (not (met-L(e) > 0)) metE' = ((not MetJ) and MetR) udp' = (not (CytR) or Crp) ubiE' = ubiB' = yigC' = fadA' = (not (FaDR2) or not (ArcA)) fadB' = (not (FaDR2) or not (ArcA)) trkH' = hemG' = glnG' = (not (nh4(e) > 0)) glnL' = (true) glnA' = (Crp and RpoN) fdoI' = ((ox2(e) > 0) or ((not (ox2(e) > 0) and (NO3(e) > 0)))) fdoH' = ((ox2(e) > 0) or ((not (ox2(e) > 0) and (NO3(e) > 0)))) fdoG' = ((ox2(e) > 0) or ((not (ox2(e) > 0) and (NO3(e) > 0)))) rhaD' = (RhaS or (RhaS and Crp)) rhaA' = (RhaS or (RhaS and Crp)) rhaB' = (RhaS or (RhaS and Crp)) rhaS' = (RhaR) rhaR' = (rmn(e) > 0) rhaT' = (RhaS or (RhaS and Crp)) sodA' = (not (ArcA or Fur) or (MarA or Rob or SoxS)) kdgT' = (not KdgR) cpxR' = false pfkA' = sbp' = (CysB) cdh' = tpiA' = glpK' = ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0))) and (not(GlpR))) glpF' = menG' = menA' = cytR' = (cytd(e) > 0) metJ' = (met-L(e) > 0) metB' = (not MetJ) metL' = (not MetJ) metF' = katG' = ((Growth(e)>0) and OxyR and RpoS) gldA' = talC' = pflD' = (ArcA or Fnr) pflC' = (ArcA or Fnr) ppc' = argE' = (not ArgR) argC' = (not ArgR) argB' = (not ArgR) argH' = (not ArgR) oxyR' = (h2O2(e) > 0) sthA' = btuB' = murI' = murB' = birA' = (btn(e) > 0) coaA' = thiH' = thiG' = thiF' = thiE' = thiC' = hemE' = purD' = (not (PurR)) purH' = metA' = (not (MetJ) or MetR) aceB' = (not (IclR) and (not (ArcA) or not (Cra))) aceA' = (not (IclR) and (not (ArcA) or not (Cra))) iclR' = ( FadR ) metH' = (MetR) lysC' = (not lys-L(e) > 0) pgi' = xylE' = (XylR) malG' = ((MalT and Crp) or MalT) malF' = ((MalT and Crp) or MalT) malE' = ((MalT and Crp) or MalT) malK' = ((MalT and Crp) or MalT) lamB' = ((MalT and Crp) or MalT) ubiC' = ((not Fnr) and Crp) ubiA' = ((not Fnr) and Crp) plsB' = dgkA' = alr' = tyrB' = (not(( (phe-L(e)>0) or (tyr-L(e)>0) ) and TyrR )) soxS' = (SoxR) soxR' = (h2O2(e) > 0) acs' = (RpoS or Fnr or ((not IclR) and ((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0) or (sbt-D(e) > 0) or (lac-D(e) > 0) or (man(e) > 0) or (succ(e) > 0)))))) gltP' = fdhF' = (FhlA and RpoN and (not (ox2(e) > 0))) rpiR' = ( not ( rib-D(e)>0 ) ) rpiB' = (not(RpiR)) proP' = (not (Crp) and Fis and RpoS) adiY' = (not (ox2(e) > 0)) adiA' = (AdiY) melR' = ((melib(e) > 0) or (melib(e) > 0 and Crp)) melA' = ((MelR) or (MelR and Crp)) melB' = ((MelR) or (MelR and Crp)) fumB' = ((Fnr) or not (Crp) or (DcuR) or not (NarL)) dcuB' = ((((not((glcn(e) > 0) or (glc-D(e) > 0) or (arab-L(e) > 0) or (xyl-D(e) > 0) or (rib-D(e) > 0) or (mal-L(e) > 0) or (glyc(e) > 0) or (sbt-D(e) > 0) or (lac-D(e) > 0) or (man(e) > 0)))) and (Fnr) and (DcuR)) and not (NarL)) dcuR' = ( DcuS ) dcuS' = ( (succ(e) > 0) or (asp-L(e) > 0) or (fum(e) > 0) or (mal-L(e) > 0) ) cadA' = (ArcA or CadC) cadB' = (ArcA or CadC) cadC' = (lys-L(e) > 0) dcuA' = aspA' = ((Crp and not (Fnr)) or Fnr) frdD' = (Fnr or DcuR or not (NarL)) frdC' = (Fnr or DcuR or not (NarL)) frdB' = (Fnr or DcuR or not (NarL)) frdA' = (Fnr or DcuR or not (NarL)) psd' = purA' = (not (PurR) or RpoE) sgaH' = sgaU' = sgaE' = cycA' = ytfQ' = ytfR' = ytfS' = ytfT' = yjfF' = fbp' = nrdD' = (Fnr) treC' = (((not TreR) and Crp) or (not TreR)) treB' = (((not TreR) and Crp) or (not TreR)) treR' = (not (tre(e) > 0)) pyrI' = (not (ura(e) > 0 or gua(e) > 0)) pyrB' = (not (ura(e) > 0 or gua(e) > 0)) argI' = (not ArgR) idnR' = ((idon-L(e)>0) or (5dGlXcn(e)>0)) idnT' = (IdnR) idnO' = (IdnR) idnD' = (IdnR) idnK' = sgcE' = gntP' = (Crp and not (glcn(e)>0)) uxuA' = (not ExuR and not UxuR) uxuB' = (not ExuR and not UxuR) uxuR' = (not(MANAO(e)>0) and not(GUI1(e)>0)) deoC' = ((not Deor) or ((not Deor) and (Crp) and (not CytR))) deoA' = (not (Deor or CytR) and Crp) deoB' = ((not Deor) or ((not Deor) and (Crp) and (not CytR)) or ((ins(e) > 0) or (gua(e) > 0))) deoD' = ((not Deor) or ((not Deor) and (not CytR)) or (ins(e) > 0) or (gua(e) > 0)) serB' = nadR' = false trpR' = (trp-L(e)>0) gpmB' = rob' = false arcA' = ( not ( ox2(e) > 0 ) ) thiS' = NRI_hi' = (NRI_low and RpoN) NRI_low' = (GlnG and GlnB and GlnD) allS' = (AllS) citB' = (CitB) citA' = (CitA) cra' = (Cra) gaTR' = (GaTR) gutR' = (GutR) faDR2' = (FaDR2)