dReach-2.15.01 performance

[shmarovfedor]

dReach-2.14.08 returns sat for the model below within 10 seconds with -k 1.

dReach-2.15.01 with -k 1 and -l 1 does not terminate (stopped it after 20 minutes).

[-5.980000e+00, 6.080000e+00]alphay;
[0, 100]time;
[0, 100]tau;
[0, 100]x;
[0, 10]y;
[0, 100]z;
{
mode 1;
invt:
(y <= 1);
flow:
d/dt[x]=1.0 * ((((0.0197/(1+exp((10.0 -z)*1.0)))-(0.0175/(1+exp((z-10.0)*2)))) - (0.00005 * (1 - (z / 12.0))) - 0.01) * x + 0.03);
d/dt[y]=1.0 * ((0.00005 * (1 - (z / 12.0))) * x + ((alphay * (1 - (1.0 * (z / 12.0)))) - 0.0168) * y);
d/dt[z]=1.0 * (-z * 0.08 + 0.02);
d/dt[tau]=1.0 * 1.0;
d/dt[alphay]=0.0;
jump:
((x+y)=4.0)==>@2(and(tau'=tau)(x'=x)(y'=y)(z'=z));
}
{
mode 2;
flow:
d/dt[x]=1.0 * ((((0.0197/(1+exp((10.0 -z)*1.0)))-(0.0175/(1+exp((z-10.0)*2)))) - (0.00005 * (1 - (z / 12.0))) - 0.01) * x + 0.03);
d/dt[y]=1.0 * ((0.00005 * (1 - (z / 12.0))) * x + ((alphay * (1 - (1.0 * (z / 12.0)))) - 0.0168) * y);
d/dt[z]=1.0 * ((12.0 - z) * 0.08 + 0.02);
d/dt[tau]=1.0 * 1.0;
d/dt[alphay]=0.0;
jump:
((x+y)=10.0)==>@1(and(tau'=tau)(x'=x)(y'=y)(z'=z));
}
init:
@1(and (and (x = 19) (y = 0.1) (z = 12.5) (tau = 0))(alphay=0.049355));
goal:
@2(and(tau = 100.0));

[soonhokong]

@shmarovfedor, could you check whether this is caused by two different versions of dReal?

[shmarovfedor]

@soonhokong, Sorry, I meant dReal-2.14.08 and dReal-2.15.01. I was using the binaries from the release page. In the most recent version most of the time it was doing this kind of operations without much progress:

...
ode_solver::inner_loop_backward:[70.8359, 70.8359]      {[0, 14.8058],[0, 100],[0, 0.217378],[3.98279, 13.3036]}
ode_solver::inner_loop_backward:[70.8359, 70.8359]      {[0, 14.8058],[0, 100],[0, 0.217378],[3.98279, 13.3036]}
ode_solver::inner_loop_backward:[70.8359, 70.8359]      {[0, 14.8058],[0, 100],[0, 0.217378],[3.98279, 13.3036]}
ode_solver::inner_loop_backward:[70.8359, 70.8359]      {[0, 14.8058],[0, 100],[0, 0.217378],[3.9828, 13.3036]}
ode_solver::inner_loop_backward:[70.8359, 70.836]       {[0, 14.8058],[0, 100],[0, 0.217378],[3.9828, 13.3036]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217378],[3.9828, 13.3036]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217378],[3.9828, 13.3036]}
ode_solver::inner_loop_backward prevTime = [70.836, 70.836] m_T = [70.1417, 85.6417]
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217378],[3.98281, 13.3037]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217378],[3.98281, 13.3037]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217378],[3.98281, 13.3037]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217379],[3.98282, 13.3037]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217379],[3.98282, 13.3037]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217379],[3.98282, 13.3037]}
ode_solver::inner_loop_backward:[70.836, 70.836]        {[0, 14.8057],[0, 100],[0, 0.217379],[3.98283, 13.3037]}
ode_solver::inner_loop_backward:[70.836, 70.8361]       {[0, 14.8057],[0, 100],[0, 0.217379],[3.98283, 13.3037]}
ode_solver::inner_loop_backward:[70.8361, 70.8361]      {[0, 14.8056],[0, 100],[0, 0.217379],[3.98283, 13.3037]}
ode_solver::inner_loop_backward:[70.8361, 70.8361]      {[0, 14.8056],[0, 100],[0, 0.217379],[3.98283, 13.3037]}
ode_solver::inner_loop_backward:[70.8361, 70.8361]      {[0, 14.8056],[0, 100],[0, 0.217379],[3.98284, 13.3038]}
ode_solver::inner_loop_backward:[70.8361, 70.8361]      {[0, 14.8056],[0, 100],[0, 0.217379],[3.98284, 13.3038]}
ode_solver::inner_loop_backward:[70.8361, 70.8361]      {[0, 14.8056],[0, 100],[0, 0.217379],[3.98284, 13.3038]}
...

[soonhokong]

@shmarovfedor, thanks for the clarification. I guess it's a side-effect of switching from CAPD3 to CAPD4. I'll take a closer look at this one.