Skip to content
This repository has been archived by the owner on May 11, 2021. It is now read-only.

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

Open
danbryce opened this issue Feb 6, 2015 · 0 comments
Open

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

danbryce opened this issue Feb 6, 2015 · 0 comments

Comments

@danbryce
Copy link
Member

danbryce commented Feb 6, 2015

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));

danbryce pushed a commit to danbryce/dreal that referenced this issue Jul 9, 2015
example:

(declare-fun v () Real [0.5])

related issue: dreal#79
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant