Error reported by dReach: v is not found in flow_map.

[rachelwang]

After updating the bmc, I encounter the following error when running the gear_shift model attached.

SMT: numodel_4_0.smt2, PATH : [1,2,1,2,3]
v is not found in flow_map.
SMT: numodel_4_1.smt2, PATH : [1,2,3,2,3]
v is not found in flow_map.
SMT: numodel_4_2.smt2, PATH : [1,2,3,4,3]
v is not found in flow_map.

the numodel.drh:

#define mu1 0.8 // \in (0.5, 1.5)
#define mu2 1.8 // \in (1.5, 2.5)
#define mu3 2.8 // \in (2.5, 3.5)
#define mu4 3.8 // \in (3.5, 4.5)
#define theta1 0.4 // \in (0.3, 0.7)
#define theta2 0.5 // \in (0.3, 0.7)
#define theta3 0.52 // \in (0.3, 0.7)
#define theta4 0.43 // \in (0.3, 0.7)
#define x1init 0 // initial location
#define x2init 3 // initial velocity
#define thre1 10 // threshold 1 for shifting
#define thre2 15 // threshold 2 for shifting
#define thre3 20 // threshold 3 for shifting
#define thre4 25 // threshold 4 for shifting
#define pi 3.1416

[0, 1] v; // throttle
[0, 5] gear; // necessary?
[0, 1000] x1;
[0, 100] x2;
[0, 3] time;

{ mode 1; //gear 1

  invt:
        (gear <= 1.5);
    (gear > 0);
  flow:
        d/dt[x1] = x2;
    d/dt[x2] = v * (1 / (theta1 * sqrt(2 * pi))) * exp(0 - ((x2 - mu1) ^ 2) / (2 * theta1 ^ 2));
    d/dt[gear] = 0.0;
  jump:
        (x2 >= thre2) ==> @2 (and (gear' = gear + 1) (x1' = x1) (x2' = x2));
}
{ mode 2; //gear 2

  invt:
        (gear > 1);
    (gear <= 2.5);
  flow:
        d/dt[x1] = x2;
    d/dt[x2] = v * (1 / (theta2 * sqrt(2 * pi))) * exp(0 - ((x2 - mu2) ^ 2) / (2 * theta2 ^ 2));
    d/dt[gear] = 0.0;
  jump:
        (x2 >= thre3) ==> @3 (and (gear' = gear + 1) (x1' = x1) (x2' = x2));
    (x2 <= thre1) ==> @1 (and (gear' = gear - 1) (x1' = x1) (x2' = x2));
}
{ mode 3; //gear 3

  invt:
        (gear <= 3.5); 
    (gear > 2);
  flow:
        d/dt[x1] = x2;
    d/dt[x2] = v * (1 / (theta3 * sqrt(2 * pi))) * exp(0 - ((x2 - mu3) ^ 2) / (2 * theta3 ^ 2));
    d/dt[gear] = 0.0;
  jump:
        (x2 >= thre4) ==> @4 (and (gear' = gear + 1) (x1' = x1) (x2' = x2));
    (x2 <= thre2) ==> @2 (and (gear' = gear - 1) (x1' = x1) (x2' = x2));
}
{ mode 4; //gear 4

  invt:
        (gear <= 4.5);
    (gear > 3);
  flow:
        d/dt[x1] = x2;
    d/dt[x2] = v * (1 / (theta4 * sqrt(2 * pi))) * exp(0 - ((x2 - mu4) ^ 2) / (2 * theta4 ^ 2));
    d/dt[gear] = 0.0;
  jump:
        (x2 <= thre3) ==> @3 (and (gear' = gear - 1) (x1' = x1) (x2' = x2));
}
init:
@1  (and (x1 = x1init) (x2 = x2init) (gear = 1));

goal:
@3  (and (gear <= 5) (x2 <= 80));

[soonhokong]

It means that the ODE for the variable v is not provided in the model.

[rachelwang]

I see. So, essentially, if I want to use a variable within the definition of an ODE, and do not want to add extra assertions for it. I'd better use #define to give it a fixed value, or (for my tool) define it as a random variable.

Thanks.

[rachelwang]

So, after your modification, each call to dReach will return 3 paths and 3 sat/unsat results?

SMT: numodel_4_0.smt2, PATH : [1,2,1,2,3]
unsat
SMT: numodel_4_1.smt2, PATH : [1,2,3,2,3]
unsat
SMT: numodel_4_2.smt2, PATH : [1,2,3,4,3]
unsat
unsat
dReal Options:
SMT: numodel_4_0.smt2, PATH : [1,2,1,2,3]
unsat
SMT: numodel_4_1.smt2, PATH : [1,2,3,2,3]
unsat
SMT: numodel_4_2.smt2, PATH : [1,2,3,4,3]
unsat
unsat
dReal Options:
SMT: numodel_4_0.smt2, PATH : [1,2,1,2,3]
unsat
SMT: numodel_4_1.smt2, PATH : [1,2,3,2,3]
unsat
SMT: numodel_4_2.smt2, PATH : [1,2,3,4,3]
unsat
unsat
BFTI 0.9 1000 1 1 0.01: Reject Null hypothesis, successes = 0, samples = 3
Elapsed cpu time: 0.007947
Elapsed wall time: 0

[rachelwang]

3 is for the gear model, I mean "multiple" in general...

[soonhokong]

I still need to see the model, but it seems that is the case. In general, dReach enumerates possible paths until it sees a SAT path or there is no path to enumerate.

[soonhokong]

So, after your modification, each call to dReach will return 3 paths and 3 sat/unsat results?

Is there any problem with it? Otherwise, please close the issue.

[rachelwang]

I see. Then, I need to modify codes for statsmt_sq as well, as previously we only have one .output file per each call.