continuous reachability { state var x1,x2,x3,x4,x5,x6,x7 setting { fixed steps 0.05 time 20 remainder estimation 1e-1 identity precondition matlab interval x5,x7 fixed orders 4 cutoff 1e-7 precision 100 output laubLoomis_small print on } poly ode 1 { 200 } # the symbolic remainder senario which can only be used with "poly ode 1" and "nonpoly ode" { x1' = 1.4 * x3 - 0.9 * x1 x2' = 2.5 * x5 - 1.5 * x2 x3' = 0.6 * x7 - 0.8 * x3 * x2 x4' = 2 - 1.3 * x4 * x3 x5' = 0.7 * x1 - x4 * x5 x6' = 0.3 * x1 - 3.1 * x6 x7' = 1.8 * x6 - 1.5 * x7 * x2 } init { x1 in [1.1,1.3] x2 in [0.95,1.15] x3 in [1.4,1.6] x4 in [2.3,2.5] x5 in [0.9,1.1] x6 in [0,0.2] x7 in [0.35,0.55] } }