-- NOTE: Use SiSAT option "--dont-stop" since we aim at computing decreasing -- upper bounds on time-bounded reachability probability. -- In order to avoid that the solver stops if probability 1 is computed -- you need to call ./sisat --i thermostat.hys --dont-stop -- Model of thermostat from Lijun Zhang, Zhikun She, Stefan Ratschan, Holger -- Hermanns, and Ernst Moritz Hahn, "Safety Verification for Probabilistic -- Hybrid Systems", CAV 2010. DECL define TIMEBOUND = 4; define MINTEMP = -100; define MAXTEMP = 100; define MAXTIME = 1000; define MAXTIMESTEP = 1000; -- Constants for values of quantified variables. -- Value OFF means "disabling" quantifier. define OFF = 0; define FLOW = 1; define JUMP = 2; define NORMAL = 1; define ERROR = 2; define T1 = 1; define T2 = 2; -- System modes. boole heat, cool, check, error; -- Mode invariants (encoded). boole inv_heat, inv_cool, inv_check; -- System variables. float [MINTEMP,MAXTEMP] temp; float [0,MAXTIME] global_time; float [0,MAXTIME] local_timer; float [0,MAXTIMESTEP] timestep; -- Transitions. boole t1, t2, t3, t4, t5; -- Transition guards (encoded). boole g1, g2, g3, g4, g5; -- Variable indicating flow or jump. boole flow; -- Indicates whether system was initialized. boole initialized; INIT -- Initial state. heat and !cool and !check and !error; temp >= 9; temp <= 10; global_time = 0; local_timer = 0; -- Invariant of heat must hold. inv_heat; -- Initially not initialized. !initialized; -- Note: flow variable is initialized in TRANS predicate via quantified -- variable initial_action. DISTR -- To select flow or jump initially. E. initial_action {OFF, FLOW, JUMP}: -- To select transition t1 or t2 if in mode heat. E. trans_from_heat {OFF, T1, T2}: -- Probabilistic transition for transition t4. R. prob_trans p = [ OFF -> 1, NORMAL -> 0.95, ERROR -> 0.05 ]: TRANS -- Initialized after first transition. initialized'; -- Enable existential quantifier before 1st transition -- and set "flow" variable accordingly. !initialized -> ( (initial_action != OFF) and (initial_action = FLOW -> flow) and (initial_action = JUMP -> !flow) ); -- If system initialized then disable existential quantifier. initialized -> ( (initial_action = OFF) ); -- Encoding of guards. g1 <-> (temp >= 9); g2 <-> (local_timer >= 2); g3 <-> (temp <= 6); g4 <-> (local_timer >= 0.5); g5 <-> (true); -- Encoding of invariants. inv_heat <-> (temp <= 10 and local_timer <= 3); inv_cool <-> (temp >= 5); inv_check <-> (local_timer <= 1); -- Enable and disbale quantified variables. -- If in mode heat and no flow then enable trans_from_heat, -- and set transition variables accordingly. (heat and !flow) -> ( (trans_from_heat != OFF) and (trans_from_heat = T1 -> t1) and (trans_from_heat = T2 -> t2) ); -- If not in heat or flo then disable trans_from_heat. (!heat or flow) -> (trans_from_heat = OFF); -- If transition t4 is taken then enable probabilistic choice, -- else disable it. t4 -> (prob_trans != OFF); !t4 -> (prob_trans = OFF); -- Alternation of flows and jumps. flow <-> !flow'; -- Exactly in one mode after transition. heat' + cool' + check' + error' = 1; -- If now flow then exactly one transition will be taken. !flow -> (t1 + t2 + t3 + t4 + t5 = 1); -- If flow then no transition will be taken. flow -> (!t1 and !t2 and !t3 and !t4 and !t5); -- If in some mode and no flow then corresponding guards and transitions -- must hold. (heat and !flow) -> ( (g1 and t1) or (g2 and t2) ); (cool and !flow) -> ( (g3 and t3) ); (check and !flow) -> ( (g4 and t4) ); (error and !flow) -> ( (g5 and t5) ); -- Time. global_time' = global_time + timestep; -- If jump or in mode error then time step = 0. (!flow or error) -> (timestep = 0); -- Transition relation. -- Mode heat. -- Flow: (heat and flow) -> ( heat' and inv_heat' and (temp' = temp + 2*timestep) and (local_timer' = local_timer + timestep) ); -- Jump: (heat and !flow and g1 and t1) -> ( cool' and inv_cool' and (temp ' = temp) and (local_timer' = local_timer) ); (heat and !flow and g2 and t2) -> ( check' and inv_check' and (temp ' = temp) and (local_timer' = 0) ); -- Mode cool. -- Flow: (cool and flow) -> ( cool' and inv_cool' and -- Solution of dtemp/dt = -temp (temp' = exp(-timestep) * temp) and (local_timer' = local_timer + timestep) ); -- Jump: (cool and !flow and g3 and t3) -> ( heat' and inv_heat' and (temp ' = temp) and (local_timer' = 0) ); -- Mode check. -- Flow: (check and flow) -> ( check' and inv_check' and -- Solution of dtemp/dt = -0.5temp (temp' = exp(-0.5*timestep) * temp) and (local_timer' = local_timer + timestep) ); -- Jump: (check and !flow and g4 and t4 and prob_trans = NORMAL) -> ( heat' and inv_heat' and (temp ' = temp) and (local_timer' = 0) ); (check and !flow and g4 and t4 and prob_trans = ERROR) -> ( error' and (temp ' = temp) and (local_timer' = local_timer) ); -- Mode error. -- Stop behavior. (error) -> ( error' and (temp ' = temp) and (local_timer' = local_timer) ); TARGET global_time <= TIMEBOUND;