Open soonhokong opened 9 years ago
@pondering, could you take a look at this problem when you have some time?
Let's say that we define a ode system as follows during the translation of a hybrid system (e.g. cardiac example):
(define-ode flow_1 ((= d/dt[tau] 1.000000) (= d/dt[u] (- (- 1.000000 0.000000) (+ (/ u 0.005500) 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))))
Can we change bmc routine so that integral constraints respect the ordering of the variables (in this example, tau, u, w, v, and s)?
tau
u
w
v
s
For example, in https://github.com/dreal/dreal/blob/master/src/tests/nra_ode/cardiac_bad_3_0.smt2, we have
(= [w_0_t v_0_t u_0_t tau_0_t s_0_t] (integral 0. time_0 [w_0_0 v_0_0 u_0_0 tau_0_0 s_0_0] flow_1))
and it uses the variable ordering w, v, u, tau, and s, which does not respect the one in define-ode.
define-ode
Sure. Just assign it to me.
@pondering, somehow github doesn't allow me to assign this to you.. let me figure out later.
@pondering, finally I figured out how to assign it to you ;-)
@pondering, could you take a look at this problem when you have some time?
Let's say that we define a ode system as follows during the translation of a hybrid system (e.g. cardiac example):
Can we change bmc routine so that integral constraints respect the ordering of the variables (in this example,
tau
,u
,w
,v
, ands
)?For example, in https://github.com/dreal/dreal/blob/master/src/tests/nra_ode/cardiac_bad_3_0.smt2, we have
and it uses the variable ordering
w
,v
,u
,tau
, ands
, which does not respect the one indefine-ode
.