search

dreal / dreal2

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

Universal quantification over the variables in the goal #43

Closed shmarovfedor closed 10 years ago

shmarovfedor commented 10 years ago

As a part of the algorithm I developed, I want to check whether the system stays (for all time points) within some region in the k-th step. Therefore, I need universal quantification over the variables used in the goal.

I think it is possible to specify such a problem in dReal and I am wondering whether it can be implemented in dReach.

soonhokong commented 10 years ago

In .drh file, you can specify mode invariant in invt: section. We check the mode invariant during the integration, not just the value of _0 and _t variables but also its values in a trace. We reject a trace if it violates the mode invariant. If you want to specify a universal invariant for a variable, you can do it by specifying mode invariants in all modes.

For now, we only support a limited forms of mode invariant -- it should be a list of simple inequalities:

...
invt:
    (x >= 0);
    (x <= 10);
...