dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

Syntax error with .drh file #2

Closed rachelwang closed 10 years ago

rachelwang commented 10 years ago

I have wrote a drh. However, dReach keeps telling me that there is a syntax error at line 16, even after I simplified the file into the following one.

#define t1 20 // temperature threshold 1
#define t2 22 // tmp thres 2
#define T0 20 // init tmp of room
#define v 5 // velocity of heating
#define d 0.1 // coefficient for the linear decrease

[10, 30] x; // room tmp

{ mode 1;

  invt:
        (x >= 20);
  flow:
        d/dt[x] = 0 - d * x;
  jump:
        (x < 20) ==> @2 (x’ = x);
}
{ mode 2;

  invt:
        (x <= 22);
  flow:
        d/dt[x] = v - d * x;
  jump:
        (x > 22) ==> @1 (x' = x);
}
init:
@1    (x = T0);

goal:
@1    (x <= 22);
soonhokong commented 10 years ago

@rachelwang, the preprocessor replaces

flow:
        d/dt[x] = 0 - d * x;

with

   flow:
         0.1/dt[x] = 5 - 0.1 * x;

because of the macro #define d 0.1.

When you debug, you need to read <xxx.preprocessed.smt2>.