Undefined symbol in dReach

[shmarovfedor]

I have the following drh model:

#define alphax  0.0197
#define alphay  0.0242
#define betax   0.0175
#define betay   0.0168
#define k1  10.0
#define k2  1.0
#define k3  10.0
#define k4  2
#define m1  0.00005
#define z0  12.0
#define gamma   0.08
//#define   r1  10.0
//#define   r0  4.0
#define d0  1.0
#define c1  0.01
#define c2  0.03
#define c3  0.02

#define Gx  ((alphax/(1+exp((k1-z)*k2)))-(betax/(1+exp((z-k3)*k4))))
#define Gy  ((alphay * (1 - (d0 * (z / z0)))) - betay)
#define Mxy (m1 * (1 - (z / z0)))

#define scale   1.0
#define T   365.0

[0, 365.0]  time;
[0, T]      tau;

[0.0, 35.0] x;
[0.0, 1.0]  y;
[0.0, 20.0] z;

[0.0, 7.99] r0;
[8.0, 15.0] r1;

{mode 1;

invt:
        (x >= 0.0);
    (x <= 35);
        (y >= 0.0);
    (y <= 1);
        (z >= 0.0);
    (z <= 20);
        (r0 >= 0.0);
    (r0 <= 7.99);
        (r1 >= 8.0);
    (r1 <= 15.0);
        (tau >= 0.0);
    (tau <= T);
flow:
    d/dt[r0] = 0;
    d/dt[r1] = 0;
        d/dt[x] = scale * ((Gx - Mxy - c1) * x + c2);
        d/dt[y] = scale * (Mxy * x + Gy * y);
        d/dt[z] = scale * (-z * gamma + c3);
        d/dt[tau] = scale * 1.0;
jump:
        ((x+y)=r0) ==> @2 (and (tau' = tau) (x' = x) (y'= y) (z' = z));
}

{mode 2;

invt:
    (x >= 0.0);
    (x <= 35);
        (y >= 0.0);
    (y <= 1);
        (z >= 0.0);
    (z <= 20);
        (r0 >= 0.0);
    (r0 <= 7.99);
        (r1 >= 8.0);
    (r1 <= 15.0);
        (tau >= 0.0);
    (tau <= T);
flow:
    d/dt[r0] = 0;
    d/dt[r1] = 0;
        d/dt[x] = scale * ((Gx - Mxy - c1) * x + c2);
        d/dt[y] = scale * (Mxy * x + Gy * y);
        d/dt[z] = scale * ((z0 - z) * gamma + c3);
        d/dt[tau] = scale * 1.0;
jump:
        ((x+y)=r1) ==> @1 (and (tau' = tau) (x' = x) (y'= y) (z' = z));
}

init:

@1  (and (x = 19) (y = 0.1) (z = 12.5) (r0 >= 0.0) (r0 <= 7.99) (r1 >= 8.0) (r0 <= 15.0) (tau = 0));

goal:

@2  (and (x >= 0.0) (x <= 30.0) (y >= 0.0) (y <= 1.0) (z >= 0.0) (z <= 20.0)  (r0 >= 0.0) (r0 <= 7.99) (r1 >= 8.0) (r0 <= 15.0) (tau = T));

and dReach outputs the following error message:

dReal Options:
For k = 0, there is no feasible path to check.
SMT: run08_1_0.smt2, PATH : [1,2]
terminate called after throwing an instance of 'std::runtime_error'
  what():  undefined symbol '5.000000000000001e' in the expression!
For k = 1, dReach tried 1 feasible paths, all of them are unsat.

[soonhokong]

It's because CAPD3/CAPD4 do not support numbers in scientific notation (i.e. 3.1415e-10). We had the problem and a solution. I think somehow I changed the print_infix function which is used to generate an input to CAPD. I'll fix it soon.

[soonhokong]

In https://github.com/dreal/dreal/commit/d217fe9d494d63609b19dc3c3095e05578af6a0e, I forget to add std::fixed which enfoces fixed-point notation instead of scientific notation.

[soonhokong]

I just sent an email to the author of CAPD reporting the problem (CC-ed: @shmarovfedor, @scungao, and @pzuliani). When he fixes the problem, I will update dReal as well. For now, we will use std::fixed to avoid the problem.

[soonhokong]

I got responses from one of the authors of CAPD. It seems that we need to keep the current approach (always printing numbers in fixed-point notation).