dreal / dreal2

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

ode_solver::extract_invariant: errortrue #10

Closed rachelwang closed 10 years ago

rachelwang commented 10 years ago

reported

ode_solver::extract_invariant: errortrue

when running numodel.drh:

#define Ix      (7.5*10^(-3))
#define Iy      (7.5*10^(-3))
#define Iz      (1.3*10^(-2))
#define Jr      (6.5*10^(-5))
#define b       (3.13*10^(-5))
#define dia (7.5*10^(-7))
#define l       0.23
#define m       0.65
#define g       9.81

#define g1      0
#define g2      0
#define g3      0
#define g4      ((l/Ix) * u22)
#define g5      ((l/Iy * u32))
#define g6      (u42 * (1/Iz))
#define g7      0
#define g8      0
#define g9      0
#define g10     (((cos(phi)*sin(theta)*cos(psi)) + sin(phi)*sin(psi))*(u12/m))
#define g11     (((cos(phi)*sin(theta)*sin(psi)) - (sin(phi)*cos(psi)))*(u12/m))
#define g12     (((u12)/m)*cos(phi)*cos(theta))

#define Omega           (dia*omegasqr5)
#define omegasqr5       (-omegasqr1 + omegasqr2 - omegasqr3 + omegasqr4)
#define omegasqr1       (U1/(4*b)) + (U3/(2*b*l)) - (U4/(4*dia))
#define omegasqr2       (U1/(4*b)) - (U2/(2*b*l)) + (U4/(4*dia))
#define omegasqr3       (U1/(4*b)) - (U3/(2*b*l)) - (U4/(4*dia))
#define omegasqr4       (U1/(4*b)) + (U2/(2*b*l)) + (U4/(4*dia))

#define u12     ((b)*(omegasqr1 + omegasqr2 + omegasqr3 + omegasqr4))
#define u22     ((b)*(-omegasqr2 + omegasqr4))
#define u32     ((b)*(omegasqr1 - omegasqr3))
#define u42     ((dia)*(-omegasqr1 + omegasqr2 -omegasqr3 + omegasqr4))

#define U1      (0.000000000000000040040329806638157622061132068177*psi - 0.000000000000000004006260662349088113459483121302*d_psi + 0.000000000000000040199263120208627223437034754057*d_theta + 0.00000000000016481994537721932724351482870661*theta + 0.00000000000098891967226331596346108897223964*x + 0.0000000000079113573781065277076887117779171*d_x + 4.11553517599868712295574368909*z + 2.5199605312384134592207374225836*d_z + 3.1622776601683793319988935444327*int_z)

#define U2      (189.73665961010275991993361266596*y - 31.630275731249675175149604910985*d_phi - 31.622776601683793319988935444327*phi + 1517.8932768808220793594689013277*d_y)

#define U3      (0.00000000000000070138917281910823366567033228324*d_psi + 0.00000000000000043749598496085489029482841870694*psi - 31.630275731249682280576962511986*d_theta - 31.622776601683793319988935444327*theta - 189.73665961010275991993361266596*x - 1517.8932768808220793594689013277*d_x - 0.0000000000000070356585091052359927346895193447*z - 0.0000000000000034839309111753163949802837487703*d_z - 0.000000000000011331008570360934389675285377061*int_z)

#define U4      (0.00000000000000040464873271944341320474427745137*d_theta - 1.0*psi - 1.0129165771177819355131077827537*d_psi + 0.00000000000023878030692159577841250980175465*theta + 0.0000000000014326818415295746704750588105279*x + 0.000000000011461454732236597363800470484223*d_x - 0.00000000000000031636295750377493337137733115377*z + 0.00000000000000020031329352465790704239314222127*d_z - 0.00000000000000010038228518403374163714875500275*int_z)

[-600,600]  phi;
[-600,600]  theta;
[-600,600]  psi;
[-3000,3000]    d_phi;
[-3000,3000]    d_theta;
[-3000,3000]    d_psi;
[-10, 10]   x;
[-10, 10]   y;
[-10, 10]   z;
[-20, 20]   d_x;
[-20, 20]   d_y;
[-20, 20]       d_z;
[-20, 20]   int_z;
[0, 5]  tau;
[0, 5]  time;

{mode 1;
invt:           true;

flow:       d/dt[phi]       = d_phi;
                d/dt[theta]     = d_theta;
                d/dt[psi]   = d_psi;
                d/dt[d_phi] = (((Iy - Iz)/Ix)*(d_theta)*(d_psi)) + (Jr/Ix * d_theta * Omega)+ g4;
                d/dt[d_theta]   = (((Iz - Ix)/Iy )*(d_phi)*(d_psi)) - ((Jr/Iy)*d_phi*Omega) + g5;
                d/dt[d_psi] = (((Ix - Iy)/Iz)*(d_phi)*(d_theta)) + g6;
                d/dt[x]     = d_x;
                d/dt[y]     = d_y;
                d/dt[z]     = d_z;
                d/dt[d_x]   = g10;
                d/dt[d_y]   = g11;
                d/dt[d_z]   = g - g12;
                d/dt[int_z] = z;
                d/dt[tau] = 1;
jump:
(x>5) ==> @1 (and
                  (phi' = phi)
                  (theta' = theta)
                  (psi' = psi)
                  (d_phi' = d_phi)
                  (d_theta' = d_theta)
                  (d_psi' = d_psi)
                  (x' = x)
                  (y' = y)
                  (z' = z)
                  (d_x' = d_x)
                  (d_y' = d_y)
                  (d_z' = d_z)
                  (int_z' = int_z)
                  (tau' = tau)
                  );
}

init:
        @1 (and (phi= 391.072) (theta= 391.072) (psi= 391.072) (d_phi=0) (d_theta=0) (d_psi=0) (x= 6.51787) (y= 6.51787) (z= 8.25894) (d_x=0) (d_y=0) (d_z=0) (int_z = 0) (tau=0));

goal:
        @1 (tau=5);
soonhokong commented 10 years ago

That is just really not an error. It's a warning. I'm working on changing the message.

rachelwang commented 10 years ago

I see. :)