Atrial Fibrillation Model

We studied the Atrial Fibrillation model as developed in Grosu et al. The model has four discrete control locations, four state variables, and nonlinear ODEs.


Benchmarks

Benchmark #Mode #Depth #ODEs #Vars Precision(δ) Result Time(sec) Trace Size
AF-GOOD 4 3 20 53 0.001 SAT 0.425 793K
AF-BAD 4 3 20 53 0.001 UNSAT 0.074 --
AF-TO1-GOOD 4 3 20 62 0.001 SAT 2.750 224K
AF-TO1-BAD 4 3 20 62 0.005 UNSAT 5.189 --
AF-TO2-GOOD 4 3 20 62 0.001 SAT 3.876 553K
AF-TO2-BAD 4 3 20 62 0.001 UNSAT 8.857 --
AF-TSO1-TSO2 4 3 20 62 0.001 UNSAT 0.027 --
AF8-K7 8 7 40 101 0.001 SAT 10.478 3.8M
AF8-K23 8 23 40 293 0.005 SAT 135.29 11M

Dynamics

"Minimal Resistor Model"

A typical set of ODEs in the model is:

\begin{aligned} \frac{du}{dt} & = e + (u-\theta_v)(u_u-u ) v g_{fi} + wsg_{si}-g_{so}(u) \\ \ \frac{ds}{dt} & = \displaystyle\frac{g_{s2}}{(1+\exp(-2k(u-us)))} - g_{s2}s \\ \ \frac{dv}{dt} & = -g_v^+\cdot v \\ \ \frac{dw}{dt} & = -g_w^+\cdot w \end{aligned}

The exponential term on the right-hand side of the ODE is the sigmoid function, which often appears in modelling biological switches.


Hybrid System Model

//Translated to drh by Sicun Gao on Apr-18-2013
// ===============================================================
// ==   Minimal Resistor Model (4 state variables)              ==
// ==                                                           ==
// ==   Author:  E. Bartocci                                    ==
// ==                                                           ==
// ==   Date:  11/05/10                                         ==
// ==                                                           ==
// ==   Free distribution with authors permission               ==
// ==                                                           ==
// ==   SUNY Stony Brook, Stony Brook, NY                       ==
// ==                                                           ==
// ===============================================================
// The following are the parameters that you can find in the paper
// A. Bueno-Orovio, M. Cherry, and F. Fenton, ?Minimal model for
// human ventricular action potentials in tissue,? Journal of
// Theoretical Biology, no. 253, pp. 544?560, 2008.
// ===============================================================

#define    EPI_TVP      1.4506
#define    EPI_TV1M       60.0
#define    EPI_TV2M     1150.0

#define    EPI_TWP       200.0

#define    EPI_TW1M       60.0
#define    EPI_TW2M       15.0

#define    EPI_TS1        2.7342
#define    EPI_TS2       16.0     //The same with Flavio's paper
#define    EPI_TFI        0.11    //The same with Flavio's paper
//#define    EPI_TO1      0.0055    //The same with Flavio's paper
#define    EPI_TO2       6      //The same with Flavio's paper
#define    EPI_TSO1      30.0181 //The same with Flavio's paper
#define    EPI_TSO2       0.9957  //The same with Flavio's paper

#define    EPI_TSI        1.8875  // We have TSI1 and TSI2   TSI in Flavio's paper


#define    EPI_TWINF     0.07    //The same with Flavio's paper
#define    EPI_THV       0.3     //EPUM The same of Flavio's paper
#define    EPI_THVM      0.006   //EPUQ The same of Flavio's paper
#define    EPI_THVINF    0.006   //EPUQ The same of Flavio's paper
#define    EPI_THW       0.13    //EPUP The same of Flavio's paper
#define    EPI_THWINF    0.006    //EPURR In Flavio's paper 0.13
#define    EPI_THSO      0.13    //EPUP The same of Flavio's paper
#define    EPI_THSI      0.13    //EPUP The same of Flavio's paper
#define    EPI_THO       0.006    //EPURR The same of Flavio's paper

#define    EPI_KWM       65.0     //The same of Flavio's paper
#define    EPI_KS        2.0994  //The same of Flavio's paper
#define    EPI_KSO       2.0458  //The same of Flavio's paper

#define    EPI_UWM       0.03    //The same of Flavio's paper
#define    EPI_US        0.9087  //The same of Flavio's paper
#define    EPI_UO        0.0     // The same of Flavio's paper
#define    EPI_UU        1.55   // The same of Flavio's paper
#define    EPI_USO       0.65   // The same of Flavio's paper

#define    jfi1 0.0
#define    jso1  (u/EPI_TO1)
#define    jsi1  0.0

#define    jfi2  0.0
#define    jso2  (u/EPI_TO2)
#define    jsi2 0.0


#define    jfi3 0.0
#define    jso3 1.0/(EPI_TSO1+((EPI_TSO2- EPI_TSO1)*(1/(1+exp(-2*EPI_KSO*(u- EPI_USO))))))
#define    jsi3 (0 - (w * s)/EPI_TSI)

#define    jfi4  (0 - v * (u - EPI_THV) * (EPI_UU - u)/EPI_TFI)
#define    jso4  (1.0 / (EPI_TSO1+((EPI_TSO2 - EPI_TSO1)*(1/(1+exp(-2*EPI_KSO*(u- EPI_USO)))))))
#define    jsi4  ( 0 - (w * s)/EPI_TSI)
#define    stim  1.0 // The external stimulation is a rectangular pulse of height 1 and length 1ms. Since u reach its max during the stimulation, time scale is set to be [0,1]

[0, 2.0] u;
[0, 2.0] v;
[0, 2.0] w;
[0, 2.0] s;

[0.0061, 0.007] EPI_TO1;

[0, 1] tau;
[0, 1] time;

{mode 1;

invt:           (u >= 0);
        (u <= 0.006);
        (v >= 0);
                (w >= 0);
                (s >= 0);
                (tau >= 0);
        (EPI_TO1 >= 0.0061);
        (EPI_TO1 <= 0.007);

flow:
              d/dt[EPI_TO1] = 0.0;
              d/dt[tau] = 1.0;
              d/dt[u] = (stim - jfi1) - (jso1 + jsi1);
              d/dt[w] = ((1.0 -(u/EPI_TWINF) - w)/(EPI_TW1M + (EPI_TW2M - EPI_TW1M) * (1/(1+exp(-2*EPI_KWM*(u - EPI_UWM))))));
              d/dt[v] = ((1.0 - v)/EPI_TV1M);
              d/dt[s] = (((1/(1+exp( -2 * EPI_KS * (u - EPI_US) ))) - s)/EPI_TS1);
jump:
              (u >= 0.006) ==> @2 (and (tau' = tau) (u' = u) (v'= v) (w' = w) (s' = s) (EPI_TO1' =  EPI_TO1));
}

{mode 2;

invt:
                (u >= 0.006);
                (u <= 0.013);
                        (v >= 0);
                (w >= 0);
                (s >= 0);
                (tau >= 0);
        (EPI_TO1 >= 0.0061);
        (EPI_TO1 <= 0.007);

flow:
              d/dt[EPI_TO1] = 0.0;
              d/dt[tau] = 1.0;
              d/dt[u] = (stim - jfi2) - (jso2 + jsi2);
              d/dt[w] = ((0.94-w)/(EPI_TW1M + (EPI_TW2M - EPI_TW1M) * (1/(1+exp(-2*EPI_KWM*(u - EPI_UWM))))));
              d/dt[v] = (-v/EPI_TV2M);
              d/dt[s] = (((1/(1+exp( -2 * EPI_KS * (u - EPI_US) ))) - s)/EPI_TS1);
jump:
                ( u >= 0.013) ==> @3 (and (tau' = tau) (u' = u) (v'= v) (w' = w) (s' = s) (EPI_TO1' =  EPI_TO1));

}

{mode 3;

invt:
                (u >= 0.013);
                (u <= 0.3);
                (v >= 0);
                (w >= 0);
                (s >= 0);
                (tau >= 0);
        (EPI_TO1 >= 0.0061);
        (EPI_TO1 <= 0.007);

flow:
              d/dt[EPI_TO1] = 0.0;
              d/dt[tau] = 1.0;
              d/dt[u] = (stim - jfi3) - (jso3 + jsi3);
              d/dt[w] = (-w/EPI_TWP);
              d/dt[v] = (-v/EPI_TV2M);
              d/dt[s] = (((1/(1+exp( -2 * EPI_KS * (u - EPI_US) ))) - s)/EPI_TS2);
jump:
                ( u >= 0.3) ==> @4 (and (tau' = tau) (u' = u) (v'= v) (w' = w) (s' = s) (EPI_TO1' =  EPI_TO1));
}

{mode 4;

invt:
                (u >= 0.3);
                (v >= 0);
                (w >= 0);
                (s >= 0);
                (tau >= 0);
        (EPI_TO1 >= 0.0061);
        (EPI_TO1 <= 0.007);

flow:
              d/dt[EPI_TO1] = 0.0;
              d/dt[tau] = 1.0;
              d/dt[u] =  (stim - jfi4) - (jso4 + jsi4);
              d/dt[w]  = (-w/EPI_TWP);
              d/dt[v]  = (-v/EPI_TVP);
              d/dt[s]  = (((1/(1+exp( -2 * EPI_KS * (u - EPI_US) ))) - s)/EPI_TS2) ;
jump:
                ( u > 2.0) ==> @4 (and (tau' = tau) (u' = u) (v'= v) (w' = w) (s' = s) (EPI_TO1' =  EPI_TO1));
}

init:	@1 (and (tau = 0) (u = 0.0) (v = 1.0) (w = 1.0) (s = 0.0) (EPI_TO1 >= 0.0061) (EPI_TO1 <= 0.007));

goal:   @4 (and (tau > 0) (tau <= 2) (u >= 0.3) (u <= 2) (v >= 0) (v <= 2) (w >= 0) (w <= 2) (s >= 0) (s <= 2) (EPI_TO1 >= 0.0061) (EPI_TO1 <= 0.007) );

Logic Encoding

(set-logic QF_NRA_ODE)
(declare-fun w () Real)
(declare-fun v () Real)
(declare-fun u () Real)
(declare-fun tau () Real)
(declare-fun s () Real)
(declare-fun EPI_TO1 () Real)
(declare-fun w_0_0 () Real)
(declare-fun w_0_t () Real)
(declare-fun w_1_0 () Real)
(declare-fun w_1_t () Real)
(declare-fun w_2_0 () Real)
(declare-fun w_2_t () Real)
(declare-fun w_3_0 () Real)
(declare-fun w_3_t () Real)
(declare-fun v_0_0 () Real)
(declare-fun v_0_t () Real)
(declare-fun v_1_0 () Real)
(declare-fun v_1_t () Real)
(declare-fun v_2_0 () Real)
(declare-fun v_2_t () Real)
(declare-fun v_3_0 () Real)
(declare-fun v_3_t () Real)
(declare-fun u_0_0 () Real)
(declare-fun u_0_t () Real)
(declare-fun u_1_0 () Real)
(declare-fun u_1_t () Real)
(declare-fun u_2_0 () Real)
(declare-fun u_2_t () Real)
(declare-fun u_3_0 () Real)
(declare-fun u_3_t () Real)
(declare-fun tau_0_0 () Real)
(declare-fun tau_0_t () Real)
(declare-fun tau_1_0 () Real)
(declare-fun tau_1_t () Real)
(declare-fun tau_2_0 () Real)
(declare-fun tau_2_t () Real)
(declare-fun tau_3_0 () Real)
(declare-fun tau_3_t () Real)
(declare-fun s_0_0 () Real)
(declare-fun s_0_t () Real)
(declare-fun s_1_0 () Real)
(declare-fun s_1_t () Real)
(declare-fun s_2_0 () Real)
(declare-fun s_2_t () Real)
(declare-fun s_3_0 () Real)
(declare-fun s_3_t () Real)
(declare-fun EPI_TO1_0_0 () Real)
(declare-fun EPI_TO1_0_t () Real)
(declare-fun EPI_TO1_1_0 () Real)
(declare-fun EPI_TO1_1_t () Real)
(declare-fun EPI_TO1_2_0 () Real)
(declare-fun EPI_TO1_2_t () Real)
(declare-fun EPI_TO1_3_0 () Real)
(declare-fun EPI_TO1_3_t () Real)
(declare-fun time_0 () Real)
(declare-fun time_1 () Real)
(declare-fun time_2 () Real)
(declare-fun time_3 () Real)
(declare-fun mode_0 () Real)
(declare-fun mode_1 () Real)
(declare-fun mode_2 () Real)
(declare-fun mode_3 () Real)
(define-ode flow_1 ((= d/dt[EPI_TO1] 0.000000) (= d/dt[tau] 1.000000) (= d/dt[u] (- (- 1.000000 0.000000) (+ (/ u EPI_TO1) 0.000000))) (= d/dt[w] (/ (- (- 1.000000 (/ u 0.070000)) w) (+ 60.000000 (* (- 15.000000 60.000000) (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 65.000000) (- u 0.030000))))))))) (= d/dt[v] (/ (- 1.000000 v) 60.000000)) (= d/dt[s] (/ (- (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 2.099400) (- u 0.908700))))) s) 2.734200))))
(define-ode flow_2 ((= d/dt[EPI_TO1] 0.000000) (= d/dt[tau] 1.000000) (= d/dt[u] (- (- 1.000000 0.000000) (+ (/ u 6.000000) 0.000000))) (= d/dt[w] (/ (- 0.940000 w) (+ 60.000000 (* (- 15.000000 60.000000) (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 65.000000) (- u 0.030000))))))))) (= d/dt[v] (/ (- 0.000000 v) 1150.000000)) (= d/dt[s] (/ (- (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 2.099400) (- u 0.908700))))) s) 2.734200))))
(define-ode flow_3 ((= d/dt[EPI_TO1] 0.000000) (= d/dt[tau] 1.000000) (= d/dt[u] (- (- 1.000000 0.000000) (+ (/ 1.000000 (+ 30.018100 (* (- 0.995700 30.018100) (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 2.045800) (- u 0.650000)))))))) (- 0.000000 (/ (* w s) 1.887500))))) (= d/dt[w] (/ (- 0.000000 w) 200.000000)) (= d/dt[v] (/ (- 0.000000 v) 1150.000000)) (= d/dt[s] (/ (- (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 2.099400) (- u 0.908700))))) s) 16.000000))))
(define-ode flow_4 ((= d/dt[EPI_TO1] 0.000000) (= d/dt[tau] 1.000000) (= d/dt[u] (- (- 1.000000 (- 0.000000 (/ (* (* v (- u 0.300000)) (- 1.550000 u)) 0.110000))) (+ (/ 1.000000 (+ 30.018100 (* (- 0.995700 30.018100) (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 2.045800) (- u 0.650000)))))))) (- 0.000000 (/ (* w s) 1.887500))))) (= d/dt[w] (/ (- 0.000000 w) 200.000000)) (= d/dt[v] (/ (- 0.000000 v) 1.450600)) (= d/dt[s] (/ (- (/ 1.000000 (+ 1.000000 (exp (* (* -2.000000 2.099400) (- u 0.908700))))) s) 16.000000))))
(assert (<= 0.000000 w_0_0))
(assert (<= w_0_0 2.000000))
(assert (<= 0.000000 w_0_t))
(assert (<= w_0_t 2.000000))
(assert (<= 0.000000 w_1_0))
(assert (<= w_1_0 2.000000))
(assert (<= 0.000000 w_1_t))
(assert (<= w_1_t 2.000000))
(assert (<= 0.000000 w_2_0))
(assert (<= w_2_0 2.000000))
(assert (<= 0.000000 w_2_t))
(assert (<= w_2_t 2.000000))
(assert (<= 0.000000 w_3_0))
(assert (<= w_3_0 2.000000))
(assert (<= 0.000000 w_3_t))
(assert (<= w_3_t 2.000000))
(assert (<= 0.000000 v_0_0))
(assert (<= v_0_0 2.000000))
(assert (<= 0.000000 v_0_t))
(assert (<= v_0_t 2.000000))
(assert (<= 0.000000 v_1_0))
(assert (<= v_1_0 2.000000))
(assert (<= 0.000000 v_1_t))
(assert (<= v_1_t 2.000000))
(assert (<= 0.000000 v_2_0))
(assert (<= v_2_0 2.000000))
(assert (<= 0.000000 v_2_t))
(assert (<= v_2_t 2.000000))
(assert (<= 0.000000 v_3_0))
(assert (<= v_3_0 2.000000))
(assert (<= 0.000000 v_3_t))
(assert (<= v_3_t 2.000000))
(assert (<= 0.000000 u_0_0))
(assert (<= u_0_0 2.000000))
(assert (<= 0.000000 u_0_t))
(assert (<= u_0_t 2.000000))
(assert (<= 0.000000 u_1_0))
(assert (<= u_1_0 2.000000))
(assert (<= 0.000000 u_1_t))
(assert (<= u_1_t 2.000000))
(assert (<= 0.000000 u_2_0))
(assert (<= u_2_0 2.000000))
(assert (<= 0.000000 u_2_t))
(assert (<= u_2_t 2.000000))
(assert (<= 0.000000 u_3_0))
(assert (<= u_3_0 2.000000))
(assert (<= 0.000000 u_3_t))
(assert (<= u_3_t 2.000000))
(assert (<= 0.000000 tau_0_0))
(assert (<= tau_0_0 1.000000))
(assert (<= 0.000000 tau_0_t))
(assert (<= tau_0_t 1.000000))
(assert (<= 0.000000 tau_1_0))
(assert (<= tau_1_0 1.000000))
(assert (<= 0.000000 tau_1_t))
(assert (<= tau_1_t 1.000000))
(assert (<= 0.000000 tau_2_0))
(assert (<= tau_2_0 1.000000))
(assert (<= 0.000000 tau_2_t))
(assert (<= tau_2_t 1.000000))
(assert (<= 0.000000 tau_3_0))
(assert (<= tau_3_0 1.000000))
(assert (<= 0.000000 tau_3_t))
(assert (<= tau_3_t 1.000000))
(assert (<= 0.000000 s_0_0))
(assert (<= s_0_0 2.000000))
(assert (<= 0.000000 s_0_t))
(assert (<= s_0_t 2.000000))
(assert (<= 0.000000 s_1_0))
(assert (<= s_1_0 2.000000))
(assert (<= 0.000000 s_1_t))
(assert (<= s_1_t 2.000000))
(assert (<= 0.000000 s_2_0))
(assert (<= s_2_0 2.000000))
(assert (<= 0.000000 s_2_t))
(assert (<= s_2_t 2.000000))
(assert (<= 0.000000 s_3_0))
(assert (<= s_3_0 2.000000))
(assert (<= 0.000000 s_3_t))
(assert (<= s_3_t 2.000000))
(assert (<= 0.006100 EPI_TO1_0_0))
(assert (<= EPI_TO1_0_0 0.007000))
(assert (<= 0.006100 EPI_TO1_0_t))
(assert (<= EPI_TO1_0_t 0.007000))
(assert (<= 0.006100 EPI_TO1_1_0))
(assert (<= EPI_TO1_1_0 0.007000))
(assert (<= 0.006100 EPI_TO1_1_t))
(assert (<= EPI_TO1_1_t 0.007000))
(assert (<= 0.006100 EPI_TO1_2_0))
(assert (<= EPI_TO1_2_0 0.007000))
(assert (<= 0.006100 EPI_TO1_2_t))
(assert (<= EPI_TO1_2_t 0.007000))
(assert (<= 0.006100 EPI_TO1_3_0))
(assert (<= EPI_TO1_3_0 0.007000))
(assert (<= 0.006100 EPI_TO1_3_t))
(assert (<= EPI_TO1_3_t 0.007000))
(assert (<= 0.000000 time_0))
(assert (<= time_0 1.000000))
(assert (<= 0.000000 time_1))
(assert (<= time_1 1.000000))
(assert (<= 0.000000 time_2))
(assert (<= time_2 1.000000))
(assert (<= 0.000000 time_3))
(assert (<= time_3 1.000000))
(assert (<= 1.000000 mode_0))
(assert (<= mode_0 4.000000))
(assert (<= 1.000000 mode_1))
(assert (<= mode_1 4.000000))
(assert (<= 1.000000 mode_2))
(assert (<= mode_2 4.000000))
(assert (<= 1.000000 mode_3))
(assert (<= mode_3 4.000000))
(assert (and (and (<= EPI_TO1_0_0 0.007000) (>= EPI_TO1_0_0 0.006100) (= s_0_0 0.000000) (= w_0_0 1.000000) (= v_0_0 1.000000) (= u_0_0 0.000000) (= tau_0_0 0.000000)) (= mode_0 1.000000) (= [w_0_t v_0_t u_0_t tau_0_t s_0_t EPI_TO1_0_t] (integral 0. time_0 [w_0_0 v_0_0 u_0_0 tau_0_0 s_0_0 EPI_TO1_0_0] flow_1)) (= mode_0 1.000000) (forall_t 1.000000 [0.000000 time_0] (>= u_0_t 0.000000)) (>= u_0_t 0.000000) (>= u_0_0 0.000000) (forall_t 1.000000 [0.000000 time_0] (<= u_0_t 0.006000)) (<= u_0_t 0.006000) (<= u_0_0 0.006000) (forall_t 1.000000 [0.000000 time_0] (>= v_0_t 0.000000)) (>= v_0_t 0.000000) (>= v_0_0 0.000000) (forall_t 1.000000 [0.000000 time_0] (>= w_0_t 0.000000)) (>= w_0_t 0.000000) (>= w_0_0 0.000000) (forall_t 1.000000 [0.000000 time_0] (>= s_0_t 0.000000)) (>= s_0_t 0.000000) (>= s_0_0 0.000000) (forall_t 1.000000 [0.000000 time_0] (>= tau_0_t 0.000000)) (>= tau_0_t 0.000000) (>= tau_0_0 0.000000) (forall_t 1.000000 [0.000000 time_0] (>= EPI_TO1_0_t 0.006100)) (>= EPI_TO1_0_t 0.006100) (>= EPI_TO1_0_0 0.006100) (forall_t 1.000000 [0.000000 time_0] (<= EPI_TO1_0_t 0.007000)) (<= EPI_TO1_0_t 0.007000) (<= EPI_TO1_0_0 0.007000) (= mode_1 2.000000) (>= u_0_t 0.006000) (= EPI_TO1_1_0 EPI_TO1_0_t) (= s_1_0 s_0_t) (= w_1_0 w_0_t) (= v_1_0 v_0_t) (= u_1_0 u_0_t) (= tau_1_0 tau_0_t) (= [w_1_t v_1_t u_1_t tau_1_t s_1_t EPI_TO1_1_t] (integral 0. time_1 [w_1_0 v_1_0 u_1_0 tau_1_0 s_1_0 EPI_TO1_1_0] flow_2)) (= mode_1 2.000000) (forall_t 2.000000 [0.000000 time_1] (>= u_1_t 0.006000)) (>= u_1_t 0.006000) (>= u_1_0 0.006000) (forall_t 2.000000 [0.000000 time_1] (<= u_1_t 0.013000)) (<= u_1_t 0.013000) (<= u_1_0 0.013000) (forall_t 2.000000 [0.000000 time_1] (>= v_1_t 0.000000)) (>= v_1_t 0.000000) (>= v_1_0 0.000000) (forall_t 2.000000 [0.000000 time_1] (>= w_1_t 0.000000)) (>= w_1_t 0.000000) (>= w_1_0 0.000000) (forall_t 2.000000 [0.000000 time_1] (>= s_1_t 0.000000)) (>= s_1_t 0.000000) (>= s_1_0 0.000000) (forall_t 2.000000 [0.000000 time_1] (>= tau_1_t 0.000000)) (>= tau_1_t 0.000000) (>= tau_1_0 0.000000) (forall_t 2.000000 [0.000000 time_1] (>= EPI_TO1_1_t 0.006100)) (>= EPI_TO1_1_t 0.006100) (>= EPI_TO1_1_0 0.006100) (forall_t 2.000000 [0.000000 time_1] (<= EPI_TO1_1_t 0.007000)) (<= EPI_TO1_1_t 0.007000) (<= EPI_TO1_1_0 0.007000) (= mode_2 3.000000) (>= u_1_t 0.013000) (= EPI_TO1_2_0 EPI_TO1_1_t) (= s_2_0 s_1_t) (= w_2_0 w_1_t) (= v_2_0 v_1_t) (= u_2_0 u_1_t) (= tau_2_0 tau_1_t) (= [w_2_t v_2_t u_2_t tau_2_t s_2_t EPI_TO1_2_t] (integral 0. time_2 [w_2_0 v_2_0 u_2_0 tau_2_0 s_2_0 EPI_TO1_2_0] flow_3)) (= mode_2 3.000000) (forall_t 3.000000 [0.000000 time_2] (>= u_2_t 0.013000)) (>= u_2_t 0.013000) (>= u_2_0 0.013000) (forall_t 3.000000 [0.000000 time_2] (<= u_2_t 0.300000)) (<= u_2_t 0.300000) (<= u_2_0 0.300000) (forall_t 3.000000 [0.000000 time_2] (>= v_2_t 0.000000)) (>= v_2_t 0.000000) (>= v_2_0 0.000000) (forall_t 3.000000 [0.000000 time_2] (>= w_2_t 0.000000)) (>= w_2_t 0.000000) (>= w_2_0 0.000000) (forall_t 3.000000 [0.000000 time_2] (>= s_2_t 0.000000)) (>= s_2_t 0.000000) (>= s_2_0 0.000000) (forall_t 3.000000 [0.000000 time_2] (>= tau_2_t 0.000000)) (>= tau_2_t 0.000000) (>= tau_2_0 0.000000) (forall_t 3.000000 [0.000000 time_2] (>= EPI_TO1_2_t 0.006100)) (>= EPI_TO1_2_t 0.006100) (>= EPI_TO1_2_0 0.006100) (forall_t 3.000000 [0.000000 time_2] (<= EPI_TO1_2_t 0.007000)) (<= EPI_TO1_2_t 0.007000) (<= EPI_TO1_2_0 0.007000) (= mode_3 4.000000) (>= u_2_t 0.300000) (= EPI_TO1_3_0 EPI_TO1_2_t) (= s_3_0 s_2_t) (= w_3_0 w_2_t) (= v_3_0 v_2_t) (= u_3_0 u_2_t) (= tau_3_0 tau_2_t) (= [w_3_t v_3_t u_3_t tau_3_t s_3_t EPI_TO1_3_t] (integral 0. time_3 [w_3_0 v_3_0 u_3_0 tau_3_0 s_3_0 EPI_TO1_3_0] flow_4)) (= mode_3 4.000000) (forall_t 4.000000 [0.000000 time_3] (>= u_3_t 0.300000)) (>= u_3_t 0.300000) (>= u_3_0 0.300000) (forall_t 4.000000 [0.000000 time_3] (>= v_3_t 0.000000)) (>= v_3_t 0.000000) (>= v_3_0 0.000000) (forall_t 4.000000 [0.000000 time_3] (>= w_3_t 0.000000)) (>= w_3_t 0.000000) (>= w_3_0 0.000000) (forall_t 4.000000 [0.000000 time_3] (>= s_3_t 0.000000)) (>= s_3_t 0.000000) (>= s_3_0 0.000000) (forall_t 4.000000 [0.000000 time_3] (>= tau_3_t 0.000000)) (>= tau_3_t 0.000000) (>= tau_3_0 0.000000) (forall_t 4.000000 [0.000000 time_3] (>= EPI_TO1_3_t 0.006100)) (>= EPI_TO1_3_t 0.006100) (>= EPI_TO1_3_0 0.006100) (forall_t 4.000000 [0.000000 time_3] (<= EPI_TO1_3_t 0.007000)) (<= EPI_TO1_3_t 0.007000) (<= EPI_TO1_3_0 0.007000) (= mode_3 4.000000) (<= EPI_TO1_3_t 0.007000) (>= EPI_TO1_3_t 0.006100) (<= s_3_t 2.000000) (>= s_3_t 0.000000) (<= w_3_t 2.000000) (>= w_3_t 0.000000) (<= v_3_t 2.000000) (>= v_3_t 0.000000) (<= u_3_t 2.000000) (>= u_3_t 0.300000) (<= tau_3_t 2.000000) (> tau_3_t 0.000000)))
(check-sat)
(exit)

Result


Reference

  1. R. Grosu, G. Batt, F. H. Fenton, J. Glimm, C. L. Guernic, S. A. Smolka, and E. Bartocci. From cardiac cells to genetic regulatory networks. In CAV, pages 396–411, 2011. [pdf]