hybrid reachability { state var x1, x2, x3, x4, x5 setting { fixed steps 0.01 time 1 remainder estimation 1e-5 identity precondition gnuplot octagon x1,x2 fixed orders 15 cutoff 1e-15 precision 512 output switching_5 max jumps 5 print on } modes { l1 { poly ode 1 { x1' = -0.8047*x1 + 8.7420*x2 - 2.4591*x3 - 8.2714*x4 - 1.8640*x5 + [-0.0845,0.0845] x2' = -8.6329*x1 - 0.5860*x2 - 2.1006*x3 + 3.6035*x4 - 1.8423*x5 x3' = 2.4511*x1 + 2.2394*x2 - 0.7538*x3 - 3.6934*x4 + 2.4585*x5 x4' = 8.3858*x1 - 3.1739*x2 + 3.7822*x3 - 0.6249*x4 + 1.8829*x5 x5' = 1.8302*x1 + 1.9869*x2 - 2.4539*x3 - 1.7726*x4 - 0.7911*x5 + [-0.7342,0.7342] } inv { x1 >= 3 } } l2 { poly ode 1 { x1' = -0.8316*x1 + 8.7658*x2 - 2.4744*x3 - 8.2608*x4 - 1.9033*x5 + [-0.0845,0.0845] x2' = -0.8316*x1 - 0.5860*x2 - 2.1006*x3 + 3.6035*x4 - 1.8423*x5 x3' = 2.4511*x1 + 2.2394*x2 - 0.7538*x3 - 3.6934*x4 + 2.4585*x5 x4' = 8.3858*x1 - 3.1739*x2 + 3.7822*x3 - 0.6249*x4 + 1.8829*x5 x5' = 1.5964*x1 + 2.1936*x2 - 2.5872*x3 - 1.6812*x4 - 1.1324*x5 + [-0.7342,0.7342] } inv { x1 >= 2 } } l3 { poly ode 1 { x1' = -0.9275*x1 + 8.8628*x2 - 2.5428*x3 - 8.2329*x4 - 2.0324*x5 + [-0.0845,0.0845] x2' = -0.8316*x1 - 0.5860*x2 - 2.1006*x3 + 3.6035*x4 - 1.8423*x5 x3' = 2.4511*x1 + 2.2394*x2 - 0.7538*x3 - 3.6934*x4 + 2.4585*x5 x4' = 8.3858*x1 - 3.1739*x2 + 3.7822*x3 - 0.6249*x4 + 1.8829*x5 x5' = 0.7635*x1 + 3.0357*x2 - 3.1814*x3 - 1.4388*x4 - 2.2538*x5 + [-0.7342,0.7342] } inv { x1 >= 1 } } l4 { poly ode 1 { x1' = -1.0145*x1 + 8.9701*x2 - 2.6207*x3 - 8.2199*x4 - 2.1469*x5 + [-0.0845,0.0845] x2' = -0.8316*x1 - 0.5860*x2 - 2.1006*x3 + 3.6035*x4 - 1.8423*x5 x3' = 2.4511*x1 + 2.2394*x2 - 0.7538*x3 - 3.6934*x4 + 2.4585*x5 x4' = 8.3858*x1 - 3.1739*x2 + 3.7822*x3 - 0.6249*x4 + 1.8829*x5 x5' = 0.0076*x1 + 3.9682*x2 - 3.8578*x3 - 1.3253*x4 - 3.2477*x5 + [-0.7342,0.7342] } inv { x1 >= 0 } } l5 { poly ode 1 { x1' = -1.4021*x1 + 10.1647*x2 - 3.3937*x3 - 8.5139*x4 - 2.9602*x5 + [-0.0845,0.0845] x2' = -0.8316*x1 - 0.5860*x2 - 2.1006*x3 + 3.6035*x4 - 1.8423*x5 x3' = 2.4511*x1 + 2.2394*x2 - 0.7538*x3 - 3.6934*x4 + 2.4585*x5 x4' = 8.3858*x1 - 3.1739*x2 + 3.7822*x3 - 0.6249*x4 + 1.8829*x5 x5' = -3.3585*x1 + 14.3426*x2 - 10.5703*x3 - 3.8785*x4 - 10.3111*x5 + [-0.7342,0.7342] } inv { x1 <= 1 } } } jumps { l1 -> l2 guard { x1 = 3 } reset { } parallelotope aggregation {} l2 -> l3 guard { x1 = 2 } reset { } parallelotope aggregation {} l3 -> l4 guard { x1 = 1 } reset { } parallelotope aggregation {} l4 -> l5 guard { x1 = 0 } reset { } parallelotope aggregation {} } init { l1 { x1 in [3.1,3.1] x2 in [4,4] x3 in [0,0] x4 in [0,0] x5 in [0,0] } } } unsafe set { l5 { x1 <= -1.2 } }