Constant zero flow ignored

[soonhokong]

The DRH file below illustrates a problem with dReal ignoring a flow constraint.

I run:

dReach -k 0 one-var.drh --proof

It finds the satisfying assignment (should be unsat):

SAT with the following box:
         time_0 : [0 , 0.0006103515625];
          d_0_t : [1 , 1.00054931640625];
         mode_0 : 1;
          d_0_0 : 0
0: 0.000000=d_0_0       : 0; [delta = 0.001000000000000001]
1: mode_0=1.000000      : 0; [delta = 0.001000000000000001]
2: 0.000000<=d_0_t      : 0.00054931640625; [delta = 0.001000000000000001]
3: 0.000000<=d_0_0      : 0; [delta = 0.001000000000000001]
4: 1.000000<=d_0_t      : 0.00054931640625; [delta = 0.001000000000000001]
5: time_0<=10.000000    : 0.0006103515625; [delta = 0.001000000000000001]
6: 0.000000<=time_0     : 0.0006103515625; [delta = 0.001000000000000001]

one-var.drh is below:

[0, 10] d;
[0, 10] time;

{ mode 1;

  invt:
       (d >= 0);
  flow:
        d/dt[d] = 0;
  jump:
        true ==> @1 true;
}

init:
@1  (and (d = 0));

goal:
@1  (and (d >= 1));

For this model, dReal construct a CAPD problem "par:d_0_0;" which is too simple so that CAPD doesn't perform any pruning. It seems that we need to add extra algebraic constraints (v_0 = v_t) for the case d/dt[v] = 0 so that things can be handled in ICP level, not in ODE level.

[soonhokong]

@danbryce said:

"I thought this might be related to the last bug report of mine. When I was tracing that code it looked like you were removing constraints of the form d/dt[v] = 0, so that CAPD would never see it. Maybe I don't understand how it works, but it should be able to prune using that constraint.

Your suggestion of adding the v_0 = v_t constraint would fix my problem in this bug report."

[soonhokong]

We handle the case "d/dt[v] = 0" specially. We consider v as a "parameter" not as a ODE variable. I hoped that this marking gives CAPD more information and get better performance as a result.

It seems that in an extreme case, like the one that you provided, we end up with 0 ODE variables and a few ODE parameters. I haven't really tested this scenario before and it seems that CAPD behaves not normally.

[danbryce]

I think I'm still getting problems with this issue. If all ODEs are zero, then I'm getting unsat when I should get sat. Try this problem:

[0, 10] d;
[0, 2] v;
[-1, 1] a;
[-1, 1] b;
[0, 10] time;

{ mode 1;

  flow:
        d/dt[d] = 0;
        d/dt[v] = 0;
        d/dt[a] = 0;
        d/dt[b] = 0;
  jump:
        true ==> @2 true;
}

{ mode 2;

  flow:
        d/dt[d] = v;
        d/dt[v] = a;
        d/dt[a] = 0;
        d/dt[b] = 0;
  jump:
        (or (b  = 1) (b = -1)) ==> @2 (and  (a' = (a + b)));
        (and  ( v = 0)) ==> @1 (and (a' = 0));
}

init:
@1  (and (d = 0) ( v = 0) ( a = 0) );

goal:
@2  (and (a = 0)  );

[soonhokong]

Fixed by 4761f4dd33429f1358260b582789b4cbf055a793