This repository was archived by the owner on May 11, 2021. It is now read-only.
This repository was archived by the owner on May 11, 2021. It is now read-only.
dReach-2.15.01 performance #83
Description
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));
Metadata
Metadata
Assignees
Labels
No labels