dreal / dreal2

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

dReach returns a syntax error #72

Closed shmarovfedor closed 9 years ago

shmarovfedor commented 9 years ago

dReach gives a syntax error in line 9 for the following problem:

[1, 100]F;
[1, 100]M;
[0, 100]K;
[0, 100]time;
[0, 100]tau;
{
mode 1;
flow:
d/dt[F]=F*(-0.013/(1+K)-(1/7777.8)*((772.3+10.0*30.4)/(F+M)+10.0));
d/dt[M]=(-M/1400)*((772.3+10.0*30.4)/(F+M)+10.0);
d/dt[K]=(0.9*0.013*F)/(1+K)-0.05;
d/dt[tau]=1;
jump:
}
init:
@1(and(tau=0)(F=25)(M=43.6)(K=0.02));
goal:
@1(and(tau=25)(M<=0.6*43.6));

However, when I put whitespaces between + and 10.0 it works alright. For example, for the following model it works fine:

[1, 100]F;
[1, 100]M;
[0, 100]K;
[0, 100]time;
[0, 100]tau;
{
mode 1;
flow:
d/dt[F]=F*(-0.013/(1+K)-(1/7777.8)*((772.3+ 10.0*30.4)/(F+M)+ 10.0));
d/dt[M]=(-M/1400)*((772.3+ 10.0*30.4)/(F+M)+ 10.0);
d/dt[K]=(0.9*0.013*F)/(1+K)-0.05;
d/dt[tau]=1;
jump:
}
init:
@1(and(tau=0)(F=25)(M=43.6)(K=0.02));
goal:
@1(and(tau=25)(M<=0.6*43.6));
soonhokong commented 9 years ago

@pondering, is it related with the recent change in dReach?

wweic commented 9 years ago

@soonhokong I don't think so. Will take a look at it. Should be parsing.