hybrid reachability { state var cycle_time1, global_time, Temp, low, H_plc, nextSfcLoc, H, high par {globalTimeHorizon=10.0 delta=0.5 } setting { fixed steps 0.01 time 10 remainder estimation 1e-5 identity precondition gnuplot octagon global_time, Temp fixed orders 5 cutoff 1e-12 precision 53 output thermostat_hypro_with_aggregation_separateControllerAndPlant_with_timer max jumps 10000000 print on } modes { l1 { poly ode 1 { Temp' = -0.1*Temp + 3 global_time' = 1 cycle_time1' = 1 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 >= 0.0 cycle_time1 <= delta global_time <= globalTimeHorizon global_time >= 0.0 H_plc = 1.0 } } l2 { poly ode 1 { Temp' = -0.1*Temp global_time' = 1 cycle_time1' = 1 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 >= 0.0 H_plc = 0.0 cycle_time1 <= delta global_time <= globalTimeHorizon global_time >= 0.0 } } clock__switch_on__cycle { poly ode 1 { global_time' = 1 cycle_time1' = 1 Temp' = 0 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 = 0.0 global_time <= globalTimeHorizon global_time >= 0.0 } } clock__switch_on_in__comm { poly ode 1 { global_time' = 1 cycle_time1' = 1 Temp' = 0 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 = 0.0 global_time <= globalTimeHorizon global_time >= 0.0 } } clock__switch_on_in__cycle { poly ode 1 { global_time' = 1 cycle_time1' = 1 Temp' = 0 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 = 0.0 global_time <= globalTimeHorizon global_time >= 0.0 } } clock__switch_off__cycle { poly ode 1 { global_time' = 1 cycle_time1' = 1 Temp' = 0 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 = 0.0 global_time <= globalTimeHorizon global_time >= 0.0 } } clock__switch_off_in__comm { poly ode 1 { global_time' = 1 cycle_time1' = 1 Temp' = 0 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 = 0.0 global_time <= globalTimeHorizon global_time >= 0.0 } } clock__switch_off_in__cycle { poly ode 1 { global_time' = 1 cycle_time1' = 1 Temp' = 0 high' = 0 H_plc' = 0 nextSfcLoc' = 0 low' = 0 H' = 0 } inv { cycle_time1 = 0.0 global_time <= globalTimeHorizon global_time >= 0.0 } } } jumps { clock__switch_on_in__cycle -> l1 guard { cycle_time1 = 0.0} reset { nextSfcLoc' := 5 } parallelotope aggregation { } clock__switch_on_in__cycle -> l2 guard { cycle_time1 = 0.0} reset { nextSfcLoc' := 5 } parallelotope aggregation { } clock__switch_off_in__cycle -> l1 guard { cycle_time1 = 0.0} reset { nextSfcLoc' := 1 } parallelotope aggregation { } clock__switch_off_in__cycle -> l2 guard { cycle_time1 = 0.0} reset { nextSfcLoc' := 1 } parallelotope aggregation { } l1 -> clock__switch_on_in__comm guard { nextSfcLoc = 5.0 cycle_time1 = delta } reset { cycle_time1' := 0 H_plc' := H } parallelotope aggregation { } l2 -> clock__switch_on_in__comm guard { nextSfcLoc = 5.0 cycle_time1 = delta } reset { cycle_time1' := 0 H_plc' := H } parallelotope aggregation { } l1 -> clock__switch_off_in__comm guard { nextSfcLoc = 1.0 cycle_time1 = delta } reset { cycle_time1' := 0 H_plc' := H } parallelotope aggregation { } l2 -> clock__switch_off_in__comm guard { nextSfcLoc = 1.0 cycle_time1 = delta } reset { cycle_time1' := 0 H_plc' := H } parallelotope aggregation { } clock__switch_off_in__comm -> clock__switch_off__cycle guard { Temp >= 23.0 cycle_time1 = 0.0} reset { low' := 1.0 high' := 1.0 H' := H_plc } parallelotope aggregation { } clock__switch_off_in__comm -> clock__switch_off__cycle guard { Temp >= 18.0 Temp <= 23.0 cycle_time1 = 0.0} reset { low' := 1.0 high' := 0.0 H' := H_plc } parallelotope aggregation { } clock__switch_off_in__comm -> clock__switch_off__cycle guard { Temp <= 18.0 cycle_time1 = 0.0} reset { low' := 0.0 high' := 0.0 H' := H_plc } parallelotope aggregation { } clock__switch_off__cycle -> clock__switch_off_in__cycle guard { low = 1.0 cycle_time1 = 0.0} reset { } parallelotope aggregation { } clock__switch_off__cycle -> clock__switch_on_in__cycle guard { low = 0.0 cycle_time1 = 0.0} reset { H' := 1 } parallelotope aggregation { } clock__switch_on_in__comm -> clock__switch_on__cycle guard { Temp >= 23.0 cycle_time1 = 0.0} reset { low' := 1.0 high' := 1.0 H' := H_plc } parallelotope aggregation { } clock__switch_on_in__comm -> clock__switch_on__cycle guard { Temp >= 18.0 Temp <= 23.0 cycle_time1 = 0.0} reset { low' := 1.0 high' := 0.0 H' := H_plc } parallelotope aggregation { } clock__switch_on_in__comm -> clock__switch_on__cycle guard { Temp <= 18.0 cycle_time1 = 0.0} reset { low' := 0.0 high' := 0.0 H' := H_plc } parallelotope aggregation { } clock__switch_on__cycle -> clock__switch_off_in__cycle guard { high = 1.0 cycle_time1 = 0.0} reset { H' := 0 } parallelotope aggregation { } clock__switch_on__cycle -> clock__switch_on_in__cycle guard { high = 0.0 cycle_time1 = 0.0} reset { } parallelotope aggregation { } } init { clock__switch_on_in__comm { H_plc in [1.0,1.0] cycle_time1 in [0.0,0.0] nextSfcLoc in [1.0,1.0] global_time in [0.0,0.0] H in [1.0,1.0] Temp in [20.0,20.0] low in [1.0,1.0] high in [0.0,0.0] } } }