-- NOTE: Use SiSAT option "--dont-stop" since we aim at staying within
-- the safe set. Thus, the probability decreases during solving.
-- In order to avoid that the solver stops if probability 1 is computed
-- (which is actually the case for this benchmark up to BMC unwinding depth 3)
-- you need to call ./sisat --i temp-regulation.hys --dont-stop
-- Case study: Temperature Regulation-Control.
-- Source: Abate, A., Prandini, M., Lygeros, J., and Sastry, S.,
-- Probabilistic reachability and safety for controlled discrete time
-- stochastic hybrid systems. Automatica 44, 11 (Nov. 2008), 2724-2734.
-- DOI=http://dx.doi.org/10.1016/j.automatica.2008.03.027
-- Specifications as in the original paper:
-- - 2 rooms
-- - temperature in degree Celcius
-- - one discrete time unit: delta = 10 minutes
DECL
-- Parameters for initial state.
-- Initial temperatures.
define INIT_TEMP_1 = 18;
define INIT_TEMP_2 = 18;
-- Initial mode: 0: off, 1: on_1, 2: on_2.
define INIT_MODE = 0;
-- Discrete states.
-- on_i means room i is heated.
-- off means no room is heated.
boole on_1, on_2, off;
-- Continuous states.
-- Average temperature x_i of room i.
float [-20, 50] x_1, x_2;
-- Parameter values.
-- Ambient temperature (assumed to be constant).
define x_a = 6;
-- Average heat loss rate of room i to the ambient.
define b_1 = 0.0167;
define b_2 = 0.0167;
-- Average heat loss rate of room i to room j.
define a_12 = 0.022;
define a_21 = 0.022;
-- Rate of heat supplied by the heater in room i.
define c_1 = 0.8;
define c_2 = 0.9333;
-- Variance for disturbances affecting temperature.
define v_square = 0.06;
-- Discrete time horizon: [0, N].
define N = 60;
-- Desired temperature interval for both rooms.
define MIN_TEMPERATURE = 17.5;
define MAX_TEMPERATURE = 22.0;
-- Takes value 1 iff room i is heated.
int [0,1] h_1, h_2;
-- Disturbances affecting temperature evolution.
float [-1, 1] n_1, n_2;
-- Encode values for better readability.
define SW_1 = 1;
define SW_2 = 2;
define SW_OFF = 3;
define OFF = 0;
define CORRECT = 1;
define UNCHANGED = 2;
define FAULTY = 3;
-- Set corresponding probabilities.
define PROB_CORRECT = 0.8;
define PROB_UNCHANGED = 0.1;
define PROB_FAULTY = 0.1;
boole safe_set_left;
INIT
-- Initial mode.
-- Mode off.
(INIT_MODE = 0) -> (!on_1 and !on_2 and off);
-- Mode on_1.
(INIT_MODE = 1) -> (on_1 and !on_2 and !off);
-- Mode on_2.
(INIT_MODE = 2) -> (!on_1 and on_2 and !off);
-- Temperature must be fixed.
x_1 = INIT_TEMP_1;
x_2 = INIT_TEMP_2;
-- Safe set left?
safe_set_left <-> ( x_1 < MIN_TEMPERATURE or
x_1 > MAX_TEMPERATURE or
x_2 < MIN_TEMPERATURE or
x_2 > MAX_TEMPERATURE );
DISTR
-- Transition control input can be chosen non-deterministically.
-- We use existential quantification to maximize probability of
-- reaching the target states.
E. control_input {SW_1, SW_2, SW_OFF}:
-- Encoding probabilistic behavior by randomized quantification:
-- 1) Command of remaining in current mode: Definitely stay in mode.
-- In this case, we disable random experiment by setting value OFF.
-- 2) Command of commuting to another mode:
-- - Transition is actually taken with probability 0.8
-- - Situation remains unchanged with probability 0.1 (models a delay)
-- - Transition to the third, non-recommended mode occurs with
-- probability 0.1 (models a faulty behavior)
R. trans p = [ OFF -> 1,
CORRECT -> PROB_CORRECT,
UNCHANGED -> PROB_UNCHANGED,
FAULTY -> PROB_FAULTY
]:
TRANS
-- Exactly in one discrete state.
on_1' + on_2' + off' = 1;
-- Describe the transition relation.
-- 1) system is in on_1:
-- a) command to stay in on_1:
-- Disable random experiment and stay in mode on_1.
(on_1 and control_input = SW_1) -> (trans = OFF and on_1');
-- b) command to leave on_1:
-- Enable random experiment:
(on_1 and control_input != SW_1) -> (trans != OFF);
-- Correct, then enter right mode.
(on_1 and control_input != SW_1 and trans = CORRECT)
-> ( (control_input = SW_2 -> on_2') and
(control_input = SW_OFF -> off')
);
-- Unchanged, then stay in on_1.
(on_1 and control_input != SW_1 and trans = UNCHANGED)
-> (on_1');
-- Faulty, then enter third mode.
(on_1 and control_input != SW_1 and trans = FAULTY)
-> ( (control_input = SW_2 -> off') and
(control_input = SW_OFF -> on_2')
);
-- 2) system is in on_2:
-- a) command to stay in on_2:
-- Disable random experiment and stay in mode on_2.
(on_2 and control_input = SW_2) -> (trans = OFF and on_2');
-- b) command to leave on_2:
-- Enable random experiment:
(on_2 and control_input != SW_2) -> (trans != OFF);
-- Correct, then enter right mode.
(on_2 and control_input != SW_2 and trans = CORRECT)
-> ( (control_input = SW_1 -> on_1') and
(control_input = SW_OFF -> off')
);
-- Unchanged, then stay in on_2.
(on_2 and control_input != SW_2 and trans = UNCHANGED)
-> (on_2');
-- Faulty, then enter third mode.
(on_2 and control_input != SW_2 and trans = FAULTY)
-> ( (control_input = SW_1 -> off') and
(control_input = SW_OFF -> on_1')
);
-- 3) system is in off:
-- a) command to stay in off:
-- Disable random experiment and stay in mode off.
(off and control_input = SW_OFF) -> (trans = OFF and off');
-- b) command to leave off:
-- Enable random experiment:
(off and control_input != SW_OFF) -> (trans != OFF);
-- Correct, then enter right mode.
(off and control_input != SW_OFF and trans = CORRECT)
-> ( (control_input = SW_1 -> on_1') and
(control_input = SW_2 -> on_2')
);
-- Unchanged, then stay in on_2.
(off and control_input != SW_OFF and trans = UNCHANGED)
-> (off');
-- Faulty, then enter third mode.
(off and control_input != SW_OFF and trans = FAULTY)
-> ( (control_input = SW_1 -> on_2') and
(control_input = SW_2 -> on_1')
);
-- Assign the right values to h_i.
on_1 -> (h_1 = 1);
!on_1 -> (h_1 = 0);
on_2 -> (h_2 = 1);
!on_2 -> (h_2 = 0);
-- Neglect disturbance first.
n_1 = 0;
n_2 = 0;
-- Evolution of the average temperatures.
-- x_i(k+1) = x_i(k) + SUM_{j != i} a_ij * (x_j(k) - x_i(k))
-- + b_i * (x_a - x_i(k))
-- + c_i * h_i(k)
-- + n_i(k)
x_1' = x_1 + a_12*(x_2 - x_1)
+ b_1*(x_a - x_1)
+ c_1*h_1
+ n_1;
x_2' = x_2 + a_21*(x_1 - x_2)
+ b_2*(x_a - x_2)
+ c_2*h_2
+ n_2;
-- Safe set is left in next state if it was already left
-- or one temperature leaves its desired interval.
safe_set_left' <-> ( safe_set_left or
( x_1 < MIN_TEMPERATURE or
x_1 > MAX_TEMPERATURE or
x_2 < MIN_TEMPERATURE or
x_2 > MAX_TEMPERATURE ) );
TARGET
-- We want to compute the maximum probability of staying within
-- the safe set.
!safe_set_left;