cannot generate .smt2 file again, "'" is not the reason

[rachelwang]

Here is the drh file:

[10, 30] x; 
[0, 3] time;
[0, 1000] tau;

{ mode 1; 

  invt:
        (x >= 16.5133);
    (tau >= 0.0);
  flow:
        d/dt[x] = (0 - 0.0756651 * x) * (2.71828 ^ (0 - 0.0756651 * tau));
    d/dt[tau] = 1.0;
  jump:
        (x <= 16.5133) ==> @2 (and (x' = x) (tau' = tau));
}
{ mode 2;

  invt:
        (x <= (16.5133 + 2.12833));
    (tau >= 0.0);
  flow:
        d/dt[x] = (0 - 0.0756651 * x) * (2.71828 ^(0 - 0.0756651 * tau)) + (4.62833 * 0.0756651) * (2.71828 ^ (0 - 0.0756651 * tau));
  jump:
        (x >= (16.5133 + 2.12833)) ==> @1 (and (x' = x) (tau' = tau));
}
init:
@1  (and (x = 18) (tau = 0));

goal:
@1  (x <= (16.5133 + 2.12833));

Thanks!

[soonhokong]

In mode2, you need to have

d/dt[tau] = 1.0;

which is indicated by the error message:

tau is not found in flow_map.

[rachelwang]

Sorry, it seems that I deleted that line by accident. It is not the reason unfortunately. Here is the complete file, which I still cannot get the .smt2 file.

[10, 30] x; 
[0, 3] time;
[0, 1000] tau;

{ mode 1; 

  invt:
        (x >= 19.5152);
    (tau >= 0.0);
  flow:
        d/dt[x] = (0 - 0.22576 * x) * (2.71828 ^ (0 - 0.22576 * tau));
    d/dt[tau] = 1.0;
  jump:
        (x <= 19.5152) ==> @2 (and (x' = x) (tau' = tau));
}
{ mode 2;

  invt:
        (x <= (19.5152 + 2.8788));
    (tau >= 0.0);
  flow:
        d/dt[x] = (0 - 0.22576 * x) * (2.71828 ^(0 - 0.22576 * tau)) + (5.3788 * 0.22576) * (2.71828 ^ (0 - 0.22576 * tau));
    d/dt[tau] = 1.0;
  jump:
        (x >= (19.5152 + 2.8788)) ==> @1 (and (x' = x) (tau' = tau));
}
init:
@1  (and (x = 18) (tau = 0));

goal:
@1  (x <= (19.5152 + 2.8788));

[soonhokong]

what was the value of k that you tried?

[rachelwang]

both 3 and 7

[soonhokong]

You should use an even number for k. Odd numbers don't work. For example, if you start from mid 1, and have three mode changes, you will end up at mode 2. dReach detects that there is no feasible path and, as a result, doesn't generates any .smt2 file.

[rachelwang]

It is different from my understanding. I was expecting that dreal would generate .smt2, and return unsat then. Anyway, thanks.

[soonhokong]

Improved the output messages by 1971239eb2165d3b6e717e5900bf121d3a243632.

• If there are more than one feasible path, dReach outputs

dReal Options:
SMT: temp_3_0.smt2, PATH : [1,1,1,1]
unsat
SMT: temp_3_1.smt2, PATH : [1,1,2,1]
unsat
SMT: temp_3_2.smt2, PATH : [1,2,1,1]
unsat
SMT: temp_3_3.smt2, PATH : [1,2,2,1]
unsat
Tried 4 feasible paths, all of them are unsat.

• If there is no feasible paths to check for a given k, dReach outputs:

There is no feasible path to check when k = 1.