dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

Flows with m_T = [0, 0] generate [0,0] interval on flows #79

Open danbryce opened 9 years ago

danbryce commented 9 years ago

The drh file, pasted below, illustrates how CAPD computes the wrong interval for x_0_t because the time interval of the flow is [0, 0]. CAPD does the right thing (sets x_0_t = x_0_0) if the interval for m_T = [0, 10]. It will recognize that m_T is [0, 0] after integration and pruning, but if it starts with m_T = [0, 0], then it compute x_0_t = [0, 0]. To illustrate correct behavior, set the bounds on time to be [0, 10].

[0, 1000] x; [0, 0] time; [0, 1000] c;

{ mode 1;

invt: (x >= 0); flow: d/dt[x] = c; d/dt[c] = 0; jump: (c = 0) ==> @2 true; } { mode 2; invt: (x >= 0); flow: d/dt[x] = c; d/dt[c] = 1; jump: true ==> @2 true; }

init: @1 (and (x = 100) (c = 0) );

goal: @2 (and (x = 100));