search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

std::logic_error: C0DoubletonSet fatal error from CAPD4 #300

Closed soonho-tri closed 8 years ago

soonho-tri commented 8 years ago 
#define p1  0.00
#define p2  0.025
#define p3 0.000013
#define VI  12
#define nn 5/54
#define GB 4.5
#define IB 15
#define B  0.5
#define k  0.05

#define u  1+2*sin(tau)
#define Pt B*exp(-k*tau)
#define diff max(max(abs(G2-G), abs(X2-X)), abs(I2-I))

[0, 20] G;
[0.0, 1] X;
[-1, 1] I;
[0, 20] G2;
[0.0, 1] X2;
[-1, 1] I2;
[0,1] boundary;
[0, 220] tau;
[0, 220] time;

{ mode 1;

  invt:
        (and (tau <= 20) (G >= -2) (G <= 10));
  flow:
        d/dt[G]         = -p1 * G - X*(G+GB) + Pt;
        d/dt[X]         = -p2 * X + p3 * I;
        d/dt[I]         = -nn * (I+IB) + 1000*u / VI/60;
        d/dt[G2]        = -p1 * G2 - X2*(G2+GB) + Pt;
        d/dt[X2]        = -p2 * X2 + p3 * I2;
        d/dt[I2]        = -nn * (I2 + IB) + 1000*u / VI/60;
        d/dt[tau]       = 1;
        d/dt[boundary]  = 0;
  jump:
        (tau >= 20)   ==> @2 (and (X' = X) (G' = G) (I' = I) (tau'=tau));
        (diff = 1.280040e+00 ) ==> @1 (and (boundary' = 1) (X' = X) (G' = G) (I' = I) (X2' = X2) (G2' = G2) (I2' = I2) (tau'=tau));
}

{ mode 2;

  invt:
        (and (G <= 10) (G >= -2) (G>= -1) (G <= 1));    
  flow:
        d/dt[G]         = -p1 * G - X*(G+GB) + Pt;
        d/dt[X]         = -p2 * X + p3 * I;
        d/dt[I]         = -nn * (I+IB) + 1000*u / VI/60;
        d/dt[G2]        = -p1 * G2 - X2*(G2+GB) + Pt;
        d/dt[X2]        = -p2 * X2 + p3 * I2;
        d/dt[I2]        = -nn * (I2 + IB) + 1000*u / VI/60;
        d/dt[tau]       = 1;
        d/dt[boundary]  = 0;
  jump:
        (diff = 1.280040e+00 ) ==> @2 (and (boundary' = 1) (X' = X) (G' = G) (I' = I) (X2' = X2) (G2' = G2) (I2' = I2) (tau'=tau));
}

init:
@1  (and (G >= 0) (G <= 10) (X >= 7.000000e-02) (X <= 1.000000e-01) (I >= -1.000000e-01) (I <= 1.000000e-01) (tau <= 0) (tau >= 0) (G2 >= 4.389346e+00) (G2 <= 4.389346e+00) (X2 >= 7.544747e-02) (X2 <= 7.544747e-02) (I2 >= 8.780944e-02) (I2 <= 8.780944e-02) (boundary = 0) );

goal:
@2 (and (tau >= 0) (boundary = 1) );

Output:

libc++abi.dylib: terminating with uncaught exception of type std::logic_error: C0DoubletonSet fatal error! Intersection of two enclosures of the same object is empty. Report this error to CAPD developers!
bound={[-3.67067e+166,3.67067e+166],[-3.25386e+166,3.25386e+166],[-3.77531e+08,3.77531e+08],[-3.77531e+08,3.77531e+08],[-813573,813573],[-815809,815809],[-18.5566,180.102]}
result.m_x={[-3.67047e+166,3.67047e+166],[-3.25369e+166,3.25369e+166],[-3.77381e+08,3.77381e+08],[-3.77381e+08,3.77381e+08],[-813549,813549],[-815785,815785],[80.7696,80.7756]}
result.m_C={
{[-2.59832e+08,2.78274e+09],[0,0],[-3.32368e+157,3.32368e+157],[0,0],[-1.13341e+161,1.13341e+161],[0,0],[-8.71332e+155,8.71332e+155]},
{[0,0],[-1.84091e+08,1.97744e+09],[0,0],[-2.93771e+157,2.93771e+157],[0,0],[-1.00178e+161,1.00178e+161],[-7.70159e+155,7.70159e+155]},
{[0,0],[0,0],[3.5502,3.5502],[0,0],[6.10221e-06,6.10221e-06],[0,0],[-2.31012,2.31012]},
{[0,0],[0,0],[0,0],[3.5502,3.5502],[0,0],[6.10221e-06,6.10221e-06],[-2.31012,2.31012]},
{[0,0],[0,0],[-0.000414448,-0.000414448],[0,0],[1.40789,1.40789],[0,0],[-1.17899e-05,1.17899e-05]},
{[0,0],[0,0],[0,0],[-0.000414448,-0.000414448],[0,0],[1.40789,1.40789],[-1.17899e-05,1.17899e-05]},
{[0,0],[0,0],[0,0],[0,0],[0,0],[0,0],[1,0.:]}
}
result.m_B={
{[-2.26502e+07,2.42579e+08],[0,0],[-9.01288e+155,9.01288e+155],[0,0],[-8.2108e+160,8.2108e+160],[0,0],[-8.71332e+155,8.71332e+155]},
{[0,0],[-2.19453e+07,2.35729e+08],[0,0],[-7.96627e+155,7.96627e+155],[0,0],[-7.25727e+160,7.25727e+160],[nan,nan]},
{[0,0],[0,0],[1.0758,1.0758],[0,0],[9.81017e-07,9.81017e-07],[0,0],[-2.31012,2.31012]},
{[0,0],[0,0],[0,0],[1.0758,1.0758],[0,0],[1.32904e-121,9.81017e-07],[nan,nan]},
{[0,0],[0,0],[-1.16771e-05,-1.16771e-05],[0,0],[1.01992,1.01992],[0,0],[-1.17899e-05,1.17899e-05]},
{[0,0],[0,0],[0,0],[-1.16771e-05,-1.16771e-05],[0,0],[-9.80012e-12,1.01992],[nan,nan]},
{[0,0],[0,0],[0,0],[0,0],[0,0],[0,0],[9.08365e-108,1]}
}
result.m_x + result.m_C * set.m_r0 + result.m_B*set.m_r={[nan,nan],[nan,nan],[nan,nan],[nan,nan],[nan,nan],[nan,nan],[nan,nan]}