Defining constant intervals in the flow

[shmarovfedor]

Is it possible to enable constant intervals in the flow without declaring them in the flow map? In other words, instead of

#define a 0.7
#define b 0.8

[0, 3.1415] alpha;
[9.8] g;
[0, 100] Sy;
[0, 1000] Sx;
[0, 15] t;
[0, 15] time;
[20.0] v0;

{ mode 1;

  flow:
        d/dt[Sx] = v0 * cos(alpha);
        d/dt[Sy] = v0 * sin(alpha) - g * t;
        d/dt[t] = 1.0;
        d/dt[alpha] = 0;
  jump:
        (and (t >= 0.0001) (Sy = 0)) ==> @1 (and (Sx' = Sx) (Sy' = 0) (t' = 0));
}

init:
@1    (and (Sx = 0) (Sy = 0) (t = 0) (alpha <= b) (alpha >= a));

goal:
@1    (and (Sx >= 40.81));

to be able to write something like this

[0.7, 0.8] alpha;
[9.8] g;
[0, 100] Sy;
[0, 1000] Sx;
[0, 15] t;
[0, 15] time;
[20.0] v0;

{ mode 1;

  flow:
        d/dt[Sx] = v0 * cos(alpha);
        d/dt[Sy] = v0 * sin(alpha) - g * t;
        d/dt[t] = 1.0;
  jump:
        (and (t >= 0.0001) (Sy = 0)) ==> @1 (and (Sx' = Sx) (Sy' = 0) (t' = 0));
}

init:
@1    (and (Sx = 0) (Sy = 0) (t = 0));

goal:
@1    (and (Sx >= 40.81));

Currently, it gives an error that variable is not defined in the flow map. As far as I remember, it was possible to use constant intervals without declaring them in the flow map in one of the past releases (sometime around March)

I think it is not difficult to do as all the computations are already performed using interval library. At the same time we can benefit a lot reducing the complexity (as we reduce the number of ODEs in the flow) which can result into a better performance.

[soonhokong]

It's certainly an implementable feature. It can reduce the burden of users. I'll put it on my todo list.

At the same time we can benefit a lot reducing the complexity (as we reduce the number of ODEs in the flow) which can result into a better performance.

While I still agree that this can reduce the amount of work on the user-side, I think it doesn't reduce the complexity on the solver side. The extra complexity added by d/dt[alpha] = 0.0 was already dropped in the current implementation. We handle d/dt[alpha] = 0.0 specially in that it is used as an ODE parameter in CAPD rather than an ODE variable.

For example, see http://mnich.ii.uj.edu.pl/capd/doc/examples_integrate.html, where a and b are treated as parameters while x, y, and z are interpreted as ODE variables with corresponding ODEs:

d/dt[x] = -(y+z)
d/dt[y] = x+b*y
d/dt[z] = b+z*(x-a)

In the end, we still need to let CAPD know that alpha is an ODE parameter. I think this can be done at best by dReach, not by dReal. Unless this can be avoided by somehow, I think the complexity remains as it is on the solver side.

[pzuliani]

Very clear explanation - thanks Soonho! Indeed it'd be a nice feature to have.

[shmarovfedor]

Thanks for the reply. It surely won't change anything if the constant is defined locally (within the flow).

But sometimes it is necessary do define such a parameter globally (for the whole system). For example, now if I want to define such a global constant I need to do the following:

...
[0, 3.1415] alpha;
...

{ mode 1;

  flow:
        ...
        d/dt[alpha] = 0;
  jump:
        ... ==> @1 (and ...(alpha' = alpha));
}
...

It means that for each jumps there will be created a new variable alpha' which will be bound with the old variable alpha using = relation. So I was thinking that we can use just one variable for this purpose and put it as a parameter in all the flows so we won't need to define it for each flow and then bind newly introduced variables for each jump. Possibly in this way the complexity will be reduced as the number of variables will be reduced.

I think it will benefit my algorithm as its performance mostly depends on dReach. Also I think it can benefit for the parameter estimation using the dReal.

[soonhokong]

@shmarovfedor, I see your point. I'll give you an update when I implement the feature.

[shmarovfedor]

Thanks