1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
--
-- A fault-tolerant heater controller with 3 sensors.
--
-- To guess the temperature (T),
--
-- (1) It compares the value of the 3 sensors 2 by 2 to determine
-- which ones seem are broken -- we consider then broken if they
-- differ too much.
--
-- (2) then, it performs a vote:
-- o If the tree sensors are broken, it does not heat;
-- o If the temperature is bigger than TMAX, it does not heat;
-- o If the temperature is smaller than TMIN, it heats;
-- o Otherwise, it keeps its previous state.
const FAILURE = -999.0; -- a fake temperature given when all sensors are broken
const TMIN = 6.0;
const TMAX = 9.0;
const DELTA = 0.5;
-- const DELTA : real;
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool);
-- T is supposed to be the real temperature and is not
-- used in the controller; we add it here in oder to test the
-- controller to be able to write a sensible oracle.
var
V12, V13, V23 : bool;
Tguess : real;
let
V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid?
V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid?
V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid?
Tguess =
if noneoftree(V12, V13, V23) then FAILURE else
if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else
if alloftree(V12, V13, V23) then Median(T1, T2, T3) else
-- 2 among V1, V2, V3 are false
if V12 then Average(T1, T2) else
if V13 then Average(T1, T3) else
-- V23 is necessarily true, hence T1 is wrong
Average(T2, T3) ;
Heat_on = true ->
if Tguess = FAILURE then false else
if Tguess < TMIN then true else
if Tguess > TMAX then false else
pre Heat_on;
tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
let
ok = true -> pre T < TMAX + 1.0 ;
tel
node not_a_sauna2(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
let
ok = true -> pre T < TMAX - 6.0 ;
tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
-- returns the absolute value of 2 reals
function abs (v : real) returns (a : real) ;
let
a = if v >= 0.0 then v else -v ;
tel
-- returns the average values of 2 reals
function Average(a, b: real) returns (z : real);
let
z = (a+b)/2.0 ;
tel
-- returns the median values of 3 reals
function Median(a, b, c : real) returns (z : real);
let
z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ;
tel
-- returns the maximum values of 2 reals
function max2 (one, two : real) returns (m : real) ;
let
m = if one > two then one else two ;
tel
-- returns the minimum values of 2 reals
function min2 (one, two : real) returns (m : real) ;
let
m = if one < two then one else two ;
tel
function noneoftree (f1, f2, f3 : bool) returns (r : bool)
let
r = not f1 and not f2 and not f3 ;
tel
function alloftree (f1, f2, f3 : bool) returns (r : bool)
let
r = f1 and f2 and f3 ;
tel
function oneoftree (f1, f2, f3 : bool) returns (r : bool)
let
r = f1 and not f2 and not f3 or
f2 and not f1 and not f3 or
f3 and not f1 and not f2 ;
tel
|
