Invariant bug

[shmarovfedor]

Both following problems should be UNSAT. In the first case I obtain the correct result

(set-logic QF_NRA_ODE)
(declare-fun x () Real)
(declare-fun tau () Real)
(declare-fun x_0_0 () Real)
(declare-fun x_0_t () Real)
(declare-fun x_1_0 () Real)
(declare-fun x_1_t () Real)
(declare-fun tau_0_0 () Real)
(declare-fun tau_0_t () Real)
(declare-fun tau_1_0 () Real)
(declare-fun tau_1_t () Real)
(declare-fun time_0 () Real)
(declare-fun time_1 () Real)
(declare-fun mode_0 () Real)
(declare-fun mode_1 () Real)
(define-ode flow_1 ((= d/dt[x] (* -1 x)) (= d/dt[tau] 10)))
(define-ode flow_2 ((= d/dt[x] (* -1 (- x 30))) (= d/dt[tau] 10)))
(assert (<= 0 x_0_0))
(assert (<= x_0_0 130))
(assert (<= 0 x_0_t))
(assert (<= x_0_t 130))
(assert (<= 0 x_1_0))
(assert (<= x_1_0 130))
(assert (<= 0 x_1_t))
(assert (<= x_1_t 130))
(assert (<= 0 tau_0_0))
(assert (<= tau_0_0 100))
(assert (<= 0 tau_0_t))
(assert (<= tau_0_t 100))
(assert (<= 0 tau_1_0))
(assert (<= tau_1_0 100))
(assert (<= 0 tau_1_t))
(assert (<= tau_1_t 100))
(assert (<= 0 time_0 [0.000000]))
(assert (<= time_0 100 [0.000000]))
(assert (<= 0 time_1 [0.000000]))
(assert (<= time_1 100 [0.000000]))
(assert (<= 1 mode_0))
(assert (<= mode_0 2))
(assert (<= 1 mode_1))
(assert (<= mode_1 2))
(assert (and
        (= tau_0_0 0)
        (<= x_0_0 30)
        (>= x_0_0 20)
        (= [x_0_t tau_0_t] (integral 0. time_0 [x_0_0 tau_0_0] flow_1))
        (forall_t 1 [0 time_0] (>= x_0_t 18))
        (>= x_0_0 18)
        (<= x_0_t 18)
        (= tau_1_0 tau_0_t)
        (= x_1_0 x_0_t)
        (= [x_1_t tau_1_t] (integral 0. time_1 [x_1_0 tau_1_0] flow_2))
        (forall_t 2 [0 time_1] (<= x_1_t 22))
        (forall_t 2 [0 time_1] (<= x_1_t 18))
        (<= x_1_0 22)
        (>= x_1_t 22)
        ))
(check-sat)
(exit)                                                                         

The result is

unsat

The following problem is SAT (which is incorrect) but I just swapped 2 invariants in conjunction:

(set-logic QF_NRA_ODE)
(declare-fun x () Real)
(declare-fun tau () Real)
(declare-fun x_0_0 () Real)
(declare-fun x_0_t () Real)
(declare-fun x_1_0 () Real)
(declare-fun x_1_t () Real)
(declare-fun tau_0_0 () Real)
(declare-fun tau_0_t () Real)
(declare-fun tau_1_0 () Real)
(declare-fun tau_1_t () Real)
(declare-fun time_0 () Real)
(declare-fun time_1 () Real)
(declare-fun mode_0 () Real)
(declare-fun mode_1 () Real)
(define-ode flow_1 ((= d/dt[x] (* -1 x)) (= d/dt[tau] 10)))
(define-ode flow_2 ((= d/dt[x] (* -1 (- x 30))) (= d/dt[tau] 10)))
(assert (<= 0 x_0_0))
(assert (<= x_0_0 130))
(assert (<= 0 x_0_t))
(assert (<= x_0_t 130))
(assert (<= 0 x_1_0))
(assert (<= x_1_0 130))
(assert (<= 0 x_1_t))
(assert (<= x_1_t 130))
(assert (<= 0 tau_0_0))
(assert (<= tau_0_0 100))
(assert (<= 0 tau_0_t))
(assert (<= tau_0_t 100))
(assert (<= 0 tau_1_0))
(assert (<= tau_1_0 100))
(assert (<= 0 tau_1_t))
(assert (<= tau_1_t 100))
(assert (<= 0 time_0 [0.000000]))
(assert (<= time_0 100 [0.000000]))
(assert (<= 0 time_1 [0.000000]))
(assert (<= time_1 100 [0.000000]))
(assert (<= 1 mode_0))
(assert (<= mode_0 2))
(assert (<= 1 mode_1))
(assert (<= mode_1 2))
(assert (and
        (= tau_0_0 0)
        (<= x_0_0 30)
        (>= x_0_0 20)
        (= [x_0_t tau_0_t] (integral 0. time_0 [x_0_0 tau_0_0] flow_1))
        (forall_t 1 [0 time_0] (>= x_0_t 18))
        (>= x_0_0 18)
        (<= x_0_t 18)
        (= tau_1_0 tau_0_t)
        (= x_1_0 x_0_t)
        (= [x_1_t tau_1_t] (integral 0. time_1 [x_1_0 tau_1_0] flow_2))
        (forall_t 2 [0 time_1] (<= x_1_t 18))
        (forall_t 2 [0 time_1] (<= x_1_t 22))
        (<= x_1_0 22)
        (>= x_1_t 22)
        ))
(check-sat)
(exit)      

The result:

sat

Is it also possible to modify the tool to support more complex invariants (conjunctions and disjunctions of simple terms)?

[soonhokong]

Thanks, Fedor. I fixed the bug in b231f9622d76b42719ae955b59a585d2f4c32ba0

[pzuliani]

Thank you for fixing it so quickly!

Paolo

[soonhokong]

Is it also possible to modify the tool to support more complex invariants (conjunctions and disjunctions of simple terms)?

Yes, it's certainly possible. Currently, it's handled by extract_invariant function in ode_solver.cpp, which only supports simple inequalities. In general, we can even call the ICP solver recursively and check almost arbitrary (ODE-free) mode invariants.

[shmarovfedor]

That's great. Thank you

[scungao]

Supporting more complex formulas requires recursive call to the solver itself. This leads to general algorithms for solving exists-forall formulas which can be widely useful. It's a significant step and will take some time. @shmarovfedor would you be interested in working with us on that?

[pzuliani]

Fedor and I were just discussing this morning how to use exists-forall formulas for parameter estimation and synthesis. We should start working on this now!

Paolo

From: Sicun Gao [mailto:notifications@github.com] Sent: 20 June 2014 17:53 To: dreal/dreal Cc: Paolo Zuliani Subject: Re: [dreal] Invariant bug (#49)

Supporting more complex formulas requires recursive call to the solver itself. This leads to general algorithms for solving exists-forall formulas which can be widely useful. It's a significant step and will take some time. @shmarovfedorhttps://github.com/shmarovfedor would you be interested in working with us on that?

— Reply to this email directly or view it on GitHubhttps://github.com/dreal/dreal/issues/49#issuecomment-46701109.

[scungao]

@pzuliani Great! I'll sketch some notes after CMSB :)

[danbryce]

Has there been any movement on this issue regarding generalized invariants? I think I'll need it for some new encodings that I want to develop.

[scungao]

I plan to work on the in December (have algorithms, need to implement). What do your invariants look like? (linear, polynomial, ...?)

On Oct 28, 2014, at 19:15, Daniel Bryce notifications@github.com wrote:

Has there been any movement on this issue regarding generalized invariants? I think I'll need it for some new encodings that I want to develop.

— Reply to this email directly or view it on GitHub.

[danbryce]

Arbitrary Boolean function with propositional and nonlinear literals. However, there are no integrals or quantifiers. See my latest draft in the silver-surfer repo.

On Oct 28, 2014, at 1:30 PM, Sicun Gao notifications@github.com wrote:

I plan to work on the in December (have algorithms, need to implement). What do your invariants look like? (linear, polynomial, ...?)

On Oct 28, 2014, at 19:15, Daniel Bryce notifications@github.com wrote:

Has there been any movement on this issue regarding generalized invariants? I think I'll need it for some new encodings that I want to develop.

— Reply to this email directly or view it on GitHub. — Reply to this email directly or view it on GitHub.

[pzuliani]

That's the sort of stuff we would also like to have :)

[soonhokong]

It's my last week at MSR. I'll work on non-ODE part until the mid November. After that, I plan to revisit the ODE part.

[danbryce]

Here are a few examples of invariant conditions I’m looking at (from http://www.aaai.org/Papers/JAIR/Vol27/JAIR-2708.pdf, page 289):

(and (< (demand) (supply)) (day)) (> (demand) (supply)) (day) (not (day)) (not (and (day) (>= (daytime) (dusk)))) (not (and (not (day)) (>= (daytime) 0))) (> (soc) (safelevel))

As you can see, they are not super complicated, but mix standard Boolean operators and propositional and numeric literals. I believe that the propositional literals can be checked once because they won’t change over an interval, just at the boundaries. In these examples, the only change needed for dReal is to allow simple inequalities on other variables (and not just constants).

The numeric literals can be more complicated than I show here. The syntax for these conditions follows the syntax for (page 116 of https://www.jair.org/media/1129/live-1129-2132-jair.pdf):

::=:disjunctive−preconditions (or ∗) ::=:disjunctive−preconditions (not ) ::=:disjunctive−preconditions (imply ) ::=:existential−preconditions (exists (∗) ) ::=:universal−preconditions (forall (∗) ) ::=:fluents ::= ( ) ::= ::= (not ) ::= ( t∗) ::= ::= ::= ::= ( ) ::= (- ) ::= ::= ( ∗) ::= ::= + ::= − ::= ∗ ::= / ::= > ::= < ::= = ::= >= ::= <= On Oct 28, 2014, at 3:48 PM, Soonho Kong notifications@github.com wrote: > It's my last week at MSR. I'll work on non-ODE part until the mid November. After that, I plan to revisit the ODE part. > > — > Reply to this email directly or view it on GitHub.

[scungao]

For this we'll need dReal to call itself. Let's talk about it in the next meeting.