% =============================================================== % == Multi Affine Minimal Model Cell Model Checking Module == % == == % == Supplement of the work: == % == == % == From Cardiac Cells to Genetic Regulatory Networks == % == Parameter Estimation for Action Potential Duration == % == == % == Authors: == % == == % == E. Bartocci, G. Batt, C. Le Guernic and R. Grosu == % == == % == Date: 11/05/10 == % == == % == Free distribution with authors permission == % == == % == SUNY Stony Brook, Stony Brook, NY == % == == % =============================================================== % % ================================ % == State Space dDescription == % ================================ % % Number of state variables % ------------------------- 4 % Partition for u (voltage) % ------------------------- % %[ 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 ] [0.0 0.00322522522522523 0.0059999999999999 0.006 0.0197777777777778 0.0293353353353353 0.0520500500500501 0.0618558558558559 0.0765025025025025 0.1299999 0.13 0.176116116116116 0.219509509509509 0.260690690690691 0.299999 0.3 0.426376376376376 0.541491491491492 0.644094094094094 0.734184184184184 0.810510510510511 0.874324324324324 0.925625625625626 0.976926926926927 1.03948948948949 1.11581581581582 1.20590590590591 1.30850850850851 1.42362362362362 1.55] % % Partition for v (fast input gate) % --------------------------------- % %[1 2 3 ] [ 0.0 0.95 1.0] % % Partition for w (slow input gate) % --------------------------------- % %[ 1 2 3 ] [ 0.0 0.95 1.0] % % Partition for s (slow output gate) % ---------------------------------- % %[ 1 2 3 ] [ 0.0 0.01 1.0] % % % ==================================== % == variable description: u == % ==================================== % % ---------------------- % -- Production Terms -- % ---------------------- % % Number of terms % --------------- 5 % % 1st Term (the stimulus) % ----------------------- % % production rate % [1] % % Constant Stimulus 1 % % 2nd Term (Jfi) % -------------- % % production rate % [1] % * % ramp for (u-0.3)(1.55-u) g_fi r 1 [ 1 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 ] %[0.0 0.3 0.426376376376376 0.541491491491492 0.644094094094094 0.734184184184184 0.810510510510511 0.874324324324324 0.925625625625626 0.976926926926927 1.03948948948949 1.11581581581582 1.20590590590591 1.30850850850851 1.42362362362362 1.55] % previous values corresponding to g_fi * (u-0.3)(1.55-u): [ 0.0 0.0 1.29090438149497 2.21405658092345 2.83378974570166 3.22013022213222 3.43197415269487 3.52779068995285 3.55113280538706 3.52662358418114 3.43197415269487 3.22013022213222 2.83378974570166 2.21405658092345 1.29090438149497 0.0 ] [0 0 0.1420 0.2435 0.3117 0.3542 0.3775 0.3881 0.3906 0.3879 0.3775 0.3542 0.3117 0.2435 0.1420 0] % % ramp for v r 2 [ 1 3 ] %[0.0 1.0] [ 0.0 1.0] % % 3nd Term (slow input Jsi) % ------------------------- % % production rate % % -(1/EPI_TSI) degradation rate 1/EPI_TSI=0.529801324503311 % but because is considered degradation we take the positive % sign and consider it a production term EPI_TSI %[0.529801324503311] tau_si = 1/g_si = [1, 20] %[0.05 1.0] [0.1 100] %[0.529801324503311] % %jsi = 0.0 if u < 0.13 (\theta_w) and jsi = ws/EPI_TSI if u > 0.13 (\theta_w) * % ramp for H^{+}(u,0.13) r 1 [ 1 10 11 30] %[0.0 0.1299999 0.13 1.5] [ 0.0 0.0 1.0 1.0] % % ramp for w * r 3 [ 1 3 ] %[0.0 1.0] [ 0.0 1.0] % % ramp for s r 4 [ 1 3 ] %[0.0 1.0] [ 0.0 1.0] % % 4nd Term Jso (slow output g_{o3}) 0.13 < u < 0.3 % ------------------------- % % production rate 1/(EPI_TSO2 - EPI_TSO1) [-50 -0.9] % % Ramp for Jso (g_so) r 1 [ 1 10 11 12 13 14 15 16 30 ] %[ 0.0 0.1299999 0.13 0.176116116116116 0.219509509509509 0.260690690690691 0.299 0.3 1.55 ] [ 0.0 0.0 0.0371347486842788 0.0379245744529007 0.0388154159747791 0.0398184365529367 0.0409446073048625 0.0 0.0 ] % % 5th Term Jso (slow output g_{o4}) 0.3 < u < 1.55 % ------------------------- % % production rate [-1] % % Ramp for Jso (g_so) r 1 [ 1 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 ] %[ 0.0 0.299999 0.3 0.426376376376376 0.541491491491492 0.644094094094094 0.734184184184184 0.810510510510511 0.874324324324324 0.925625625625626 0.976926926926927 1.03948948948949 1.11581581581582 1.20590590590591 1.30850850850851 1.42362362362362 1.55 ] [ 0.0 0.0 0.0409446382840491 0.0460443086347673 0.0535437875115028 0.0637664813337137 0.0767333519436878 0.0916925245941391 0.107774773920785 0.123549833090718 0.142260797964051 0.169583455745153 0.210423641565343 0.270114601421950 0.352978734119542 0.460653839673183 0.585471819608690] % % ----------------------- % -- Degradation terms -- % ----------------------- % % Number of terms % --------------- 2 % % % 1st Term (Jso) % -------------- % % degradation rate % [1 180] % % Ramp for Jso (u g_{o_1}) r 1 [ 1 3 4 30] %[0.0 0.005999999 0.006 1.55] [ 1.0 1.0 0.0 0.0] % % % %[0.1 0.5] [0 10] % % Ramp for Jso (u g_{o2}) r 1 [ 1 3 4 10 11 30] %[ 0.0 0.005999999 0.006 0.1299999 0.0 0.0] [ 0.0 0.0 1.0 1.0 0.0 0.0] % % % % % % % ============================================== % == variable description: v == % ============================================== % % ---------------------- % -- Production Terms -- % ---------------------- % % The equation for v is % v = (1 - v)g_{v_1} if u < 0.006 (\theta_v) or % v = -vg_{v_2} if u >= 0.006 and u < 0.3 % v = -vg_v if u >= 0.3 % % Number of terms % --------------- 1 % 1st Term % --------- % % production rate 1/EPI_TV1M % [0.0166666666666667] * % ramp for H^{-}(u,0.006) r 1 [ 1 3 4 30] %[0.0 0.005999999 0.006 1.5] [ 1.0 1.0 0.0 0.0] % % ramp for (1-v) - r 2 [ 1 3 ] %[0.0 1.0] [ 0.0 1.0] % % ----------------------- % -- Degradation Terms -- % ----------------------- % % Number of terms % --------------- 2 % % 1st Term % -------- % % degradation rate 1/EPI_TV2M % [0.000869565217391304] % ramp for H^{+}(u,0.006)H^{-}(u,0.3) r 1 [ 1 3 4 15 16 30] %[0.0 0.005999999 0.006 0.299999 0.3 1.5] [ 0.0 0.0 1.0 1.0 0.0 0.0] % % % 2nd Term % -------- % % degradation rate 1/EPI_TVP % [0.689369915896870] % ramp for r 1 [ 1 15 16 30] %[0.0 0.299999 0.3 1.5] [ 0.0 0.0 1.0 1.0] % % % % ================================================ % == variable description: w == % ================================================ % % ------------------------ % -- Production terms -- % ------------------------ % % Number of production terms 3 % (1.0 - (u/0.07) - w) / f(u) for u < 0.006 % f(u) = TWM1 + (TWM2 - TWM1) * Sigmoid (u) % Flavio to get the Alternans suggested to put TWM1 = TWM2 = TWM % Production Term 1 % (1.0 - w)(1/TWM) % % Degradation Term 1 % % (u/0.07)/(1/TWM) % % (0.94 - w)/ f(u) for 0.006 < u < 0.13 % f(u) = TWM1 + (TWM2 - TWM1) * Sigmoid (u) % TWM1 = TWM2 = TWM % % Production term 1 % % 0.94(1/TWM) % % Degradation Term 2 % % w(1/TWM) % % - w / TWP for 0.13 < u < 1.55 % % Degradation Term 3 % % w (1/TWP) % % % 1st Term (u < 0.006) % -------------------- % %[1/TWM] [0.005] * % the first ramp mimics the Heaviside H^{-}(u,0.006) r 1 [ 1 3 4 30] %[0.0 0.005999999 0.006 1.5] [ 1.0 1.0 0.0 0.0] % % the second Ramp is (1.0 - w) - r 3 [ 1 3 ] %[0.0 1.0] [ 0.0 1.0] % % 2nd Term (0.006 < u < 0.13) % --------------------------- % %[1/TWM] [0.005] % % ramp for H^{+}(u,0.006)H^{+}(u,0.006)H^{-}(u,0.13)w_{\infty} r 1 [ 1 3 4 10 11 30] %[0.0 0.005999999 0.006 0.1299999 0.13 1.5] [ 0.0 0.0 0.94 0.94 0.0 0.0] % % % 3st Term is -u g_{w_\infty} g_{w}^{-} on (u < 0.006) % ---------------------------------------------------- % % degradation rate % % [1/(TWM*0.07)] [-0.071428571428571] % % ramp modeling -u r 1 [ 1 3 4 30] %[0.0 0.005999999 0.006 1.5] [ 0.0 0.005999999 0.0 0.0] % %-------------------------- % -- Degradation terms -- % ------------------------- % % Number of terms % ---------------- 2 % % 1st Term is -w g_{w}^{-} on 0.006 < u < 0.13 % ----------------------------------------------- % % degradation rate % %[1/TWM] [0.005] % ramp for H^{+}(u,0.006)H^{+}(u,0.006)H^{-}(u,0.13) r 1 [ 1 3 4 10 11 30] %[0.0 0.005999999 0.006 0.1299999 0.13 1.5] [ 0.0 0.0 1.0 1.0 0.0 0.0] % % % 2nd Term is -w g_{w}^{+} on (0.13 < u < 1.55) % ------------------------------------------------- % % degradation rate % % [1/TWP] [0.0025] % ramp for H^{+}(u,0.13) r 1 [ 1 10 11 30] %[0.0 0.1299999 0.13 1.5] [ 0.0 0.0 1.0 1.0] % % % ================================================ % == variable description: s == % ================================================ % % ------------------- % -- Production terms % ------------------- % % Number of terms % --------------- % 2 % % 1st Term % -------- % % production rate EPI_GS1 = 1/EPI_TS1 [0.365737692926633] % r 1 [ 1 2 3 4 5 6 7 8 9 10 11 30 ] %[0.0 0.00322522522522523 0.005999999 0.006 0.0197777777777778 0.0293353353353353 0.0520500500500501 0.0618558558558559 0.0765025025025025 0.1299999 0.13 1.55] [ 0.0215530430802808 0.0218404832501762 0.0220907746541382 0.0220907747448439 0.0233756631454813 0.0243095439036467 0.0266773222136253 0.0277674867419459 0.0294768269421839 0.0366287295501185 0.0 0.0 ] % % 2nd Term % -------- % % production rate 1/EPI_TS2 [0.0625000000000000] % r 1 [ 1 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 ] %[0.0 0.1299999 0.13 0.176116116116116 0.219509509509509 0.260690690690691 0.299999 0.3 0.426376376376376 0.541491491491492 0.644094094094094 0.734184184184184 0.810510510510511 0.874324324324324 0.925625625625626 0.976926926926927 1.03948948948949 1.11581581581582 1.20590590590591 1.30850850850851 1.42362362362362 1.55 ] [ 0.0 0.0 0.0366287443664546 0.0441092881834653 0.0524622441859381 0.0617535327747815 0.0720368814519242 0.0720371621320020 0.116584384855182 0.176268665677548 0.247679421847480 0.324590012929517 0.398366018652226 0.463978368245852 0.517759355285649 0.571132010712343 0.633940429340140 0.704670344322184 0.776937543225223 0.842734428913138 0.896790494026689 0.936593943204126] % % % -------------------- % -- Degradation Terms % -------------------- % % Number of terms % --------------- 2 % % 1st Term % -------- % % degradation rate EPI_GS1 = 1/EPI_TS1 % [0.365737692926633] % % ramp for heaviside H^{-}(u,0.13) r 1 [ 1 10 11 30 ] %[0.0 0.1299999 0.13 1.55] [ 1.0 1.0 0.0 0.0 ] % % % 2nd Term % --------- % % degradation rate 1/EPI_TS2 % [0.0625000000000000] % % ramp for H^{+}(u,0.13) r 1 [ 1 10 11 30 ] %[0.0 0.1299999 0.13 1.55] [ 0.0 0.0 1.0 1.0 ] % % % % ============================================== % == Behavior Specifications == % ============================================== % % Number of atomic propositions % ----------------------------- 10 % % The atomic propositions (see explanations in web page) % ------------------------------------------------------ % {1 '>' 1} % prop1: u > 0 {1 '<' 2} % prop2: u < 0.006 % % [1 2 3 ] v index % [0.0 0.95 1.0] v threshold % {2 '>' 2} % prop3: v > 0.95 {2 '<' 3} % prop4: v < 1 % % [ 1 2 3 ] w index % [0.0 0.95 1.0] w threshold % {3 '>' 2} % prop5: w > 0.95 {3 '<' 3} % prop6: w <1 % % [ 1 2 3 ] s index % [ 0.0 0.01 1.0] s threshold % {4 '>' 1} % prop7: s > 0 {4 '<' 2} % prop8: s < 0.01 % % additional properties for u % {1 '>' 11} % prop9: u > 0.13 %{1 '<' 3} % prop10: u < 0.006 {1 '<' 16} % prop10: u < 0.3 % % Initial states for verification (NuSMV predicate or "All") % ---------------------------------------------------------- % %All (prop1 & prop2 & prop3 & prop4 & prop5 & prop6 & prop7 & prop8) % % Property type (0: CTL; 1:LTL); % note: CTL is not supported yet! % ---------------------------------------------------------------- 1 % Property to check (initial state implies finally state with property % -------------------------------------------------------------------- % %G(prop10) %F(prop13 & prop14) %F (q > 590) -> F (z>200) G (prop10) % % Compute liveness of SCCs (0: No; 1:Yes)? % ---------------------------------------- 0