Incorrect solution by dReach/dReal

[shmarovfedor]

I tried the following problem in dReach with k = 1

#define a 20
#define b 20

[0.7854] alpha;
[9.8] g;
[0, 100] Sy;
[0, 1000] Sx;
[0, 15] t;
[0, 15] time;
[0, 100] v0;

{ mode 1;

  flow:
        d/dt[Sx] = v0 * cos(alpha);
        d/dt[Sy] = v0 * sin(alpha) - g * t;
        d/dt[t] = 1.0;
        d/dt[v0] = 0.0;
  jump:
        (and (t >= 0.0001) (Sy = 0)) ==> @1 (and (Sx' = Sx) (Sy' = 0) (t' = 0) (v0' = 0.9 * v0));
}

init:
@1    (and (Sx = 0) (Sy = 0) (t = 0) (v0 <= b) (v0 >= a));

goal:
@1    (and (Sx >= 100.0));

dReach/dReal says that the problem is SAT:

         Sx_1_t : [100, 100.0005308618921];
          t_1_t : [3.475316833962188, 3.475424424903862];
         v0_1_t : [0, 0.000762939453125];
         Sx_1_0 : [40.81630880754172, 40.81695618194594];
         Sy_1_0 : [0, 0];
          t_1_0 : [0, 0];
         v0_1_0 : [24.08271789550781, 24.08340454101563];
         time_1 : [3.475316833962188, 3.475424424903862];
          t_0_0 : [0, 0];
         Sy_0_0 : [0, 0];
         v0_0_t : [26.75857543945313, 26.75933837890625];
         Sx_0_0 : [0, 0];
          t_0_t : [2.88615542799785, 2.886155427997853];
         Sy_0_t : [0, 0];
         Sx_0_t : [40.81632653033684, 40.81632653033694];
         mode_1 : [1, 1];
         time_0 : [2.88615542799785, 2.886155427997853];
         Sy_1_t : [0, 0.0008690540290179318];
         v0_0_0 : [20, 20];
         mode_0 : [1, 1]

which is, in fact, incorrect because v0_0_0 : [20, 20] should remain the same (d/dt[v0] = 0.0) and can't be v0_0_t : [26.75857543945313, 26.75933837890625];

[danbryce]

This is a duplicate of an issue I reported. Capd does not like constant zero flows.

Dan

[shmarovfedor]

Thank you for the reply, Dan.

What is the correct way of specifying constants (such as v0 in this example) then? By the constants I also mean variables which remain the same within the mode and change their values while making a discrete transition.

[soonhokong]

Like Dan said, it looks like a duplicate of #19. Anyway, I'm working on it now.

[danbryce]

Thanks Fedor for making that wheel squeak!

[soonhokong]

Fixed.