// -------------------------------------------------------- // Thermostat example // -------------------------------------------------------- // -------------------------------------------------------- // Analysis Parameters // -------------------------------------------------------- PARTITION_CHECK_TIME_RELEVANCE_DURING = false; //REACH_USE_CONVEX_HULL = true; CHEAP_CONTAIN_RETURN_OTHERS = false; // REACH_STOP_USE_CONVEX_HULL_ITER = 10; // REACH_USE_BBOX_ITER = 10; //REFINE_DERIVATIVE_METHOD = 3; //SEARCH_METHOD = 6; time_bound := 1; // -------------------------------------------------------- // System Definition // -------------------------------------------------------- automaton thermostat synclabs : tau; state_var : t,x,T; loc init: while True wait {T'==0 & x'==0 & t'==0} when True sync tau goto heat; loc cool: while T>=5 & x<=time_bound wait {T'==-T & x'==1 & t'==1} when T<=6 sync tau do {t' == 0 & x'==x & T'==T} goto heat; loc heat: while T<=10 & t<=3 & x<=time_bound wait {T'==2 & x'==1 & t'==1} when T>=9 sync tau do {t'==t & x'==x & T'==T} goto cool; when t>=2 sync tau do {t'==0 & x'==x & T'==T} goto check; loc check: while t<=1 & x<=time_bound wait {T'==-0.5*T & x'==1 & t'==1} when t>=0.5 & x<=time_bound sync tau palt { 95 : do {t'==0 & x'==x & T'==T} goto heat, 5 : do {t'==0 & x'==0 & T'==0} goto error }; loc error: while x<=time_bound wait {T'==0 & x'==0 & t'==0} initially init & t==0 & x==0 & 9<=T & T<=10; end -- thermostat thermostat.add_label(tick); thermostat.set_refine_constraints((x,2),tick); //thermostat.set_refine_constraints((x,10),tick); // -------------------------------------------------------- // Definition of forbidden states // -------------------------------------------------------- forbidden=thermostat.{error & True}; thermostat.reach_graph("thermostat.graph", forbidden);