Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Any way to overcome high order enclosure error? #354

Open
SunandanAdhikary opened this issue Aug 23, 2019 · 0 comments
Open

Any way to overcome high order enclosure error? #354

SunandanAdhikary opened this issue Aug 23, 2019 · 0 comments

Comments

@SunandanAdhikary
Copy link

SunandanAdhikary commented Aug 23, 2019

High Order Enclosure Error: minimal time step reached. Cannot integrate.
the set: {[0,0],[0,0],[1,1],[2,2]}
current time: [0,1.01496e-06]
time step: [1.01496e-06,1.01496e-06]

Getting this error while trying to solve my smt script. (can't attach the file type so pasting it here)

(set-logic QF_NRA_ODE)
(declare-fun x () Real [-100, 100])
(declare-fun v () Real [0, 10000])
(declare-fun u () Real [-100, 100])
(declare-fun lt () Real [0.000000, 0.1])
(declare-fun gt () Real [0.000000, 20])
(declare-fun state_x_0 () Real [-100, 100] )
(declare-fun next_u_0 () Real [-100, 100] )
(declare-fun x_0_0 () Real [-100, 100])
(declare-fun x_0_t () Real [-100, 100])
(declare-fun v_0_0 () Real [0, 10000])
(declare-fun v_0_t () Real [0, 10000])
(declare-fun u_0_0 () Real [-100, 100])
(declare-fun u_0_t () Real [-100, 100])
(declare-fun lt_0_0 () Real [0.000000, 0.1])
(declare-fun lt_0_t () Real [0.000000, 0.1])
(declare-fun gt_0_0 () Real [0.000000, 20])
(declare-fun gt_0_t () Real [0.000000, 20])
(declare-fun time_0 () Real [0.001, 0.001])
(declare-fun mode_0 () Real [1.000000, 1.000000])
(declare-fun Noise__-1 () Real [0, 0])
(declare-fun state_x_1 () Real [-100, 100] )
(declare-fun next_u_1 () Real [-100, 100] )
(declare-fun x_1_0 () Real [-100, 100])
(declare-fun x_1_t () Real [-100, 100])
(declare-fun v_1_0 () Real [0, 10000])
(declare-fun v_1_t () Real [0, 10000])
(declare-fun u_1_0 () Real [-100, 100])
(declare-fun u_1_t () Real [-100, 100])
(declare-fun lt_1_0 () Real [0.000000, 0.1])
(declare-fun lt_1_t () Real [0.000000, 0.1])
(declare-fun gt_1_0 () Real [0.000000, 20])
(declare-fun gt_1_t () Real [0.000000, 20])
(declare-fun time_1 () Real [0.1, 0.1])
(declare-fun mode_1 () Real [1.000000, 1.000000])
(declare-fun state_x_2 () Real [-100, 100] )
(declare-fun next_u_2 () Real [-100, 100] )
(declare-fun x_2_0 () Real [-100, 100])
(declare-fun x_2_t () Real [-100, 100])
(declare-fun v_2_0 () Real [0, 10000])
(declare-fun v_2_t () Real [0, 10000])
(declare-fun u_2_0 () Real [-100, 100])
(declare-fun u_2_t () Real [-100, 100])
(declare-fun lt_2_0 () Real [0.000000, 0.1])
(declare-fun lt_2_t () Real [0.000000, 0.1])
(declare-fun gt_2_0 () Real [0.000000, 20])
(declare-fun gt_2_t () Real [0.000000, 20])
(declare-fun time_2 () Real [0.1, 0.1])
(declare-fun mode_2 () Real [1.000000, 1.000000])
(declare-fun state_x_3 () Real [-100, 100] )
(declare-fun next_u_3 () Real [-100, 100] )
(declare-fun x_3_0 () Real [-100, 100])
(declare-fun x_3_t () Real [-100, 100])
(declare-fun v_3_0 () Real [0, 10000])
(declare-fun v_3_t () Real [0, 10000])
(declare-fun u_3_0 () Real [-100, 100])
(declare-fun u_3_t () Real [-100, 100])
(declare-fun lt_3_0 () Real [0.000000, 0.1])
(declare-fun lt_3_t () Real [0.000000, 0.1])
(declare-fun gt_3_0 () Real [0.000000, 20])
(declare-fun gt_3_t () Real [0.000000, 20])
(declare-fun time_3 () Real [0.1, 0.1])
(declare-fun mode_3 () Real [1.000000, 1.000000])
(declare-fun state_x_4 () Real [-100, 100] )
(declare-fun next_u_4 () Real [-100, 100] )
(declare-fun x_4_0 () Real [-100, 100])
(declare-fun x_4_t () Real [-100, 100])
(declare-fun v_4_0 () Real [0, 10000])
(declare-fun v_4_t () Real [0, 10000])
(declare-fun u_4_0 () Real [-100, 100])
(declare-fun u_4_t () Real [-100, 100])
(declare-fun lt_4_0 () Real [0.000000, 0.1])
(declare-fun lt_4_t () Real [0.000000, 0.1])
(declare-fun gt_4_0 () Real [0.000000, 20])
(declare-fun gt_4_t () Real [0.000000, 20])
(declare-fun time_4 () Real [0.1, 0.1])
(declare-fun mode_4 () Real [1.000000, 1.000000])
(declare-fun state_x_5 () Real [-100, 100] )
(declare-fun next_u_5 () Real [-100, 100] )
(declare-fun x_5_0 () Real [-100, 100])
(declare-fun x_5_t () Real [-100, 100])
(declare-fun v_5_0 () Real [0, 10000])
(declare-fun v_5_t () Real [0, 10000])
(declare-fun u_5_0 () Real [-100, 100])
(declare-fun u_5_t () Real [-100, 100])
(declare-fun lt_5_0 () Real [0.000000, 0.1])
(declare-fun lt_5_t () Real [0.000000, 0.1])
(declare-fun gt_5_0 () Real [0.000000, 20])
(declare-fun gt_5_t () Real [0.000000, 20])
(declare-fun time_5 () Real [0.1, 0.1])
(declare-fun mode_5 () Real [1.000000, 1.000000])
(declare-fun state_x_6 () Real [-100, 100] )
(declare-fun next_u_6 () Real [-100, 100] )
(declare-fun x_6_0 () Real [-100, 100])
(declare-fun x_6_t () Real [-100, 100])
(declare-fun v_6_0 () Real [0, 10000])
(declare-fun v_6_t () Real [0, 10000])
(declare-fun u_6_0 () Real [-100, 100])
(declare-fun u_6_t () Real [-100, 100])
(declare-fun lt_6_0 () Real [0.000000, 0.1])
(declare-fun lt_6_t () Real [0.000000, 0.1])
(declare-fun gt_6_0 () Real [0.000000, 20])
(declare-fun gt_6_t () Real [0.000000, 20])
(declare-fun time_6 () Real [0.1, 0.1])
(declare-fun mode_6 () Real [1.000000, 1.000000])
(declare-fun state_x_7 () Real [-100, 100] )
(declare-fun next_u_7 () Real [-100, 100] )
(declare-fun x_7_0 () Real [-100, 100])
(declare-fun x_7_t () Real [-100, 100])
(declare-fun v_7_0 () Real [0, 10000])
(declare-fun v_7_t () Real [0, 10000])
(declare-fun u_7_0 () Real [-100, 100])
(declare-fun u_7_t () Real [-100, 100])
(declare-fun lt_7_0 () Real [0.000000, 0.1])
(declare-fun lt_7_t () Real [0.000000, 0.1])
(declare-fun gt_7_0 () Real [0.000000, 20])
(declare-fun gt_7_t () Real [0.000000, 20])
(declare-fun time_7 () Real [0.1, 0.1])
(declare-fun mode_7 () Real [1.000000, 1.000000])
(declare-fun state_x_8 () Real [-100, 100] )
(declare-fun next_u_8 () Real [-100, 100] )
(declare-fun x_8_0 () Real [-100, 100])
(declare-fun x_8_t () Real [-100, 100])
(declare-fun v_8_0 () Real [0, 10000])
(declare-fun v_8_t () Real [0, 10000])
(declare-fun u_8_0 () Real [-100, 100])
(declare-fun u_8_t () Real [-100, 100])
(declare-fun lt_8_0 () Real [0.000000, 0.1])
(declare-fun lt_8_t () Real [0.000000, 0.1])
(declare-fun gt_8_0 () Real [0.000000, 20])
(declare-fun gt_8_t () Real [0.000000, 20])
(declare-fun time_8 () Real [0.1, 0.1])
(declare-fun mode_8 () Real [1.000000, 1.000000])
(declare-fun state_x_9 () Real [-100, 100] )
(declare-fun next_u_9 () Real [-100, 100] )
(declare-fun x_9_0 () Real [-100, 100])
(declare-fun x_9_t () Real [-100, 100])
(declare-fun v_9_0 () Real [0, 10000])
(declare-fun v_9_t () Real [0, 10000])
(declare-fun u_9_0 () Real [-100, 100])
(declare-fun u_9_t () Real [-100, 100])
(declare-fun lt_9_0 () Real [0.000000, 0.1])
(declare-fun lt_9_t () Real [0.000000, 0.1])
(declare-fun gt_9_0 () Real [0.000000, 20])
(declare-fun gt_9_t () Real [0.000000, 20])
(declare-fun time_9 () Real [0.1, 0.1])
(declare-fun mode_9 () Real [1.000000, 1.000000])
(declare-fun state_x_10 () Real [-100, 100] )
(declare-fun next_u_10 () Real [-100, 100] )
(declare-fun x_10_0 () Real [-100, 100])
(declare-fun x_10_t () Real [-100, 100])
(declare-fun v_10_0 () Real [0, 10000])
(declare-fun v_10_t () Real [0, 10000])
(declare-fun u_10_0 () Real [-100, 100])
(declare-fun u_10_t () Real [-100, 100])
(declare-fun lt_10_0 () Real [0.000000, 0.1])
(declare-fun lt_10_t () Real [0.000000, 0.1])
(declare-fun gt_10_0 () Real [0.000000, 20])
(declare-fun gt_10_t () Real [0.000000, 20])
(declare-fun time_10 () Real [0.000000, 0.1])
(declare-fun mode_10 () Real [1.000000, 1.000000])
(define-ode flow_1 ((= d/dt[gt] 1) (= d/dt[lt] 1) (= d/dt[x] (+(- x) u)) (= d/dt[v] (-((- x)(- x u))( u(- u x)))) (= d/dt[u] 0)))
(assert (and (= lt_0_0 0) (= gt_0_0 0) (= v_0_0 2 )(= u_0_0 1 )(= x_0_0 1 )(= mode_0 1)
(= lt_0_t (+ lt_0_0 (* 1 0.001))) (= gt_0_t (+ gt_0_0 (* 1 0.001))) (= u_0_t (+ u_0_0 (* 0 0.001)))
(= [gt_0_t lt_0_t x_0_t v_0_t u_0_t ] (integral 0. time_0 [gt_0_0 lt_0_0 x_0_0 v_0_0 u_0_0 ] flow_1))
(= mode_1 1) (= lt_0_t 0.001) (= gt_1_0 gt_0_t) (= lt_1_0 0)
(= x_1_0 x_0_t)(= v_1_0 v_0_t)
(= state_x_0 x_0_t )
(= next_u_1 (- -0 state_x_0 ) )

(= next_u_1 u_1_0 )
(= lt_1_t (+ lt_1_0 (* 1 time_1 ))) (= gt_1_t (+ gt_1_0 (* 1 time_1 ))) (= u_1_t (+ u_1_0 (* 0 time_1 )))
(= [gt_1_t lt_1_t x_1_t v_1_t u_1_t ] (integral 0. time_1 [gt_1_0 lt_1_0 x_1_0 v_1_0 u_1_0 ] flow_1))
(<= lt_1_t 0.1) (<= lt_1_0 0.1) (= mode_2 1)
(= mode_2 1) (<= lt_1_t 0.1) (= gt_2_0 gt_1_t) (= lt_2_0 0)
(= x_2_0 x_1_t)(= v_2_0 v_1_t)
(= state_x_1 x_1_t )
(= next_u_2 (- -0 state_x_1 ) )

(= next_u_2 u_2_0 )
(= lt_2_t (+ lt_2_0 (* 1 time_2 ))) (= gt_2_t (+ gt_2_0 (* 1 time_2 ))) (= u_2_t (+ u_2_0 (* 0 time_2 )))
(= [gt_2_t lt_2_t x_2_t v_2_t u_2_t ] (integral 0. time_2 [gt_2_0 lt_2_0 x_2_0 v_2_0 u_2_0 ] flow_1))
(<= lt_2_t 0.1) (<= lt_2_0 0.1) (= mode_3 1)
(= mode_3 1) (<= lt_2_t 0.1) (= gt_3_0 gt_2_t) (= lt_3_0 0)
(= x_3_0 x_2_t)(= v_3_0 v_2_t)
(= state_x_2 x_2_t )
(= next_u_3 (- -0 state_x_2 ) )

(= next_u_3 u_3_0 )
(= lt_3_t (+ lt_3_0 (* 1 time_3 ))) (= gt_3_t (+ gt_3_0 (* 1 time_3 ))) (= u_3_t (+ u_3_0 (* 0 time_3 )))
(= [gt_3_t lt_3_t x_3_t v_3_t u_3_t ] (integral 0. time_3 [gt_3_0 lt_3_0 x_3_0 v_3_0 u_3_0 ] flow_1))
(<= lt_3_t 0.1) (<= lt_3_0 0.1) (= mode_4 1)
(= mode_4 1) (<= lt_3_t 0.1) (= gt_4_0 gt_3_t) (= lt_4_0 0)
(= x_4_0 x_3_t)(= v_4_0 v_3_t)
(= state_x_3 x_3_t )
(= next_u_4 (- -0 state_x_3 ) )

(= next_u_4 u_4_0 )
(= lt_4_t (+ lt_4_0 (* 1 time_4 ))) (= gt_4_t (+ gt_4_0 (* 1 time_4 ))) (= u_4_t (+ u_4_0 (* 0 time_4 )))
(= [gt_4_t lt_4_t x_4_t v_4_t u_4_t ] (integral 0. time_4 [gt_4_0 lt_4_0 x_4_0 v_4_0 u_4_0 ] flow_1))
(<= lt_4_t 0.1) (<= lt_4_0 0.1) (= mode_5 1)
(= mode_5 1) (<= lt_4_t 0.1) (= gt_5_0 gt_4_t) (= lt_5_0 0)
(= x_5_0 x_4_t)(= v_5_0 v_4_t)
(= state_x_4 x_4_t )
(= next_u_5 (- -0 state_x_4 ) )

(= next_u_5 u_5_0 )
(= lt_5_t (+ lt_5_0 (* 1 time_5 ))) (= gt_5_t (+ gt_5_0 (* 1 time_5 ))) (= u_5_t (+ u_5_0 (* 0 time_5 )))
(= [gt_5_t lt_5_t x_5_t v_5_t u_5_t ] (integral 0. time_5 [gt_5_0 lt_5_0 x_5_0 v_5_0 u_5_0 ] flow_1))
(<= lt_5_t 0.1) (<= lt_5_0 0.1) (= mode_6 1)
(= mode_6 1) (<= lt_5_t 0.1) (= gt_6_0 gt_5_t) (= lt_6_0 0)
(= x_6_0 x_5_t)(= v_6_0 v_5_t)
(= state_x_5 x_5_t )
(= next_u_6 (- -0 state_x_5 ) )

(= next_u_6 u_6_0 )
(= lt_6_t (+ lt_6_0 (* 1 time_6 ))) (= gt_6_t (+ gt_6_0 (* 1 time_6 ))) (= u_6_t (+ u_6_0 (* 0 time_6 )))
(= [gt_6_t lt_6_t x_6_t v_6_t u_6_t ] (integral 0. time_6 [gt_6_0 lt_6_0 x_6_0 v_6_0 u_6_0 ] flow_1))
(<= lt_6_t 0.1) (<= lt_6_0 0.1) (= mode_7 1)
(= mode_7 1) (<= lt_6_t 0.1) (= gt_7_0 gt_6_t) (= lt_7_0 0)
(= x_7_0 x_6_t)(= v_7_0 v_6_t)
(= state_x_6 x_6_t )
(= next_u_7 (- -0 state_x_6 ) )

(= next_u_7 u_7_0 )
(= lt_7_t (+ lt_7_0 (* 1 time_7 ))) (= gt_7_t (+ gt_7_0 (* 1 time_7 ))) (= u_7_t (+ u_7_0 (* 0 time_7 )))
(= [gt_7_t lt_7_t x_7_t v_7_t u_7_t ] (integral 0. time_7 [gt_7_0 lt_7_0 x_7_0 v_7_0 u_7_0 ] flow_1))
(<= lt_7_t 0.1) (<= lt_7_0 0.1) (= mode_8 1)
(= mode_8 1) (<= lt_7_t 0.1) (= gt_8_0 gt_7_t) (= lt_8_0 0)
(= x_8_0 x_7_t)(= v_8_0 v_7_t)
(= state_x_7 x_7_t )
(= next_u_8 (- -0 state_x_7 ) )

(= next_u_8 u_8_0 )
(= lt_8_t (+ lt_8_0 (* 1 time_8 ))) (= gt_8_t (+ gt_8_0 (* 1 time_8 ))) (= u_8_t (+ u_8_0 (* 0 time_8 )))
(= [gt_8_t lt_8_t x_8_t v_8_t u_8_t ] (integral 0. time_8 [gt_8_0 lt_8_0 x_8_0 v_8_0 u_8_0 ] flow_1))
(<= lt_8_t 0.1) (<= lt_8_0 0.1) (= mode_9 1)
(= mode_9 1) (<= lt_8_t 0.1) (= gt_9_0 gt_8_t) (= lt_9_0 0)
(= x_9_0 x_8_t)(= v_9_0 v_8_t)
(= state_x_8 x_8_t )
(= next_u_9 (- -0 state_x_8 ) )

(= next_u_9 u_9_0 )
(= lt_9_t (+ lt_9_0 (* 1 time_9 ))) (= gt_9_t (+ gt_9_0 (* 1 time_9 ))) (= u_9_t (+ u_9_0 (* 0 time_9 )))
(= [gt_9_t lt_9_t x_9_t v_9_t u_9_t ] (integral 0. time_9 [gt_9_0 lt_9_0 x_9_0 v_9_0 u_9_0 ] flow_1))
(<= lt_9_t 0.1) (<= lt_9_0 0.1) (= mode_10 1)
(= mode_10 1) (<= lt_9_t 0.1) (= gt_10_0 gt_9_t) (= lt_10_0 0)
(= x_10_0 x_9_t)(= v_10_0 v_9_t)
(= state_x_9 x_9_t )
(= next_u_10 (- -0 state_x_9 ) )

(= next_u_10 u_10_0 )
(= lt_10_t (+ lt_10_0 (* 1 time_10 ))) (= gt_10_t (+ gt_10_0 (* 1 time_10 ))) (= u_10_t (+ u_10_0 (* 0 0.1 )))
(= [gt_10_t lt_10_t x_10_t v_10_t u_10_t ] (integral 0. time_10 [gt_10_0 lt_10_0 x_10_0 v_10_0 u_10_0 ] flow_1))
(forall_t 1 [0 time_10] (<= lt_10_t 0.1))
(<= lt_10_t 0.1) (<= lt_10_0 0.1) (= mode_10 1)
(> v_10_t 0.735758882 )(> gt_10_t 1 ) ))
(check-sat)
(exit)

Tried reducing decimal points in precisions. Doesn't help much. Will dReal4 come handy to handle this? Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant