-- 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;