Bug on dReach path generation

[kquine]

For multiple jump conditions between two modes, dReach does not generate necessary smt2 files. Below is a simple example. Although there are two different jumps for 1 ==> 1, it generates only one.

[0, 10] x; [0, 10] y; [-1, 1] d; [0, 1] tau; [0, 1] time;

{mode 1; invt: (tau <= 1); flow: d/dt[x] = d; d/dt[y] = -d; d/dt[d] = 0; d/dt[tau] = 1; jump: (and (tau = 1) (x >= y)) ==> @1 (and (x' = x) (y' = y) (d' = 1) (tau' = tau)); (and (tau = 1) (x < y)) ==> @1 (and (x' = x) (y' = y) (d' = -1) (tau' = tau)); } init: @1 (and (x = 4) (y = 5) (d = 1) (tau = 0)); goal: @1 true;

[soonhokong]

@pondering, could you please take a look at this one?

[wweic]

I'm working on it. Seems like it's preprocessing error.

[wweic]

@soonhokong To fix it, we have to abandon the Jumpmap field and roll back to plain list representation of jumps. I'll do that.

[soonhokong]

I agree.

On Thursday, January 22, 2015, Wei Chen notifications@github.com wrote:

@soonhokong https://github.com/soonhokong To fix it, we have to abandon the Jumpmap field and roll back to plain list representation of jumps. I'll do that.

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/68#issuecomment-71145532.

Soonho Kong soonhok@cs.cmu.edu

[wweic]

@soonhokong I found heuristic/heuristic.ml still uses jumpmap. While it's added by @danbryce, I'll try to go ahead and see if it will cause any problem.

[wweic]

@kquine @soonhokong Please try this patch without enabling heuristic.

[soonhokong]

@kquine confirmed that it worked with his examples. Let me close this for now. Please reopen it if you find a problem.