Commit 29a083d8 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Merge /home/chmaiza/lurette into HEAD

parents 7991faeb c6aa944f
LTOP=../../../../$(HOSTTYPE)/bin/lurettetop
LURETTETOP=$(LTOP) --precision 2 --sut heater_control.lus \
--main-sut-node heater_control --oracle heater_control.lus \
--main-oracle-node not_a_sauna --sut-compiler verimag \
--oracle-compiler verimag --test-length 100 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step
LURETTETOP_0=$(LTOP) --precision 2 --sut heater_control.lus \
--main-sut-node heater_control --sut-compiler verimag \
--test-length 100 --thick-draw 1 --draw-inside 0 --draw-edges 0 \
--draw-vertices 0 --draw-all-vertices --step-mode Inside --local-var \
--no-sim2chro --seed 3 --do-not-show-step
#
test:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) -go --output test.rif0 degradable-sensors.lut && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
utest:
cp test.rif test.rif.exp
clean:
rm -rf *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp
test_dontgo:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) --output test.rif0 degradable-sensors.luc && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
env:
$(LURETTETOP_0) -go --output test.rif0 heater_control_env.lut
sensors:
$(LURETTETOP_0) -go --output test.rif0 sensors.lut
sensors-oracle:
$(LURETTETOP) -go --output test.rif0 sensors.lut
degradable:
$(LURETTETOP_0) -go --output test.rif0 degradable-sensors.lut
degradable-oracle:
$(LURETTETOP) -go --output test.rif0 degradable-sensors.lut
-- Simulate sensors that wears out
let between(x, min, max : real): bool = (min < x) and (x < max)
node main(Heat_on : bool) returns (T, T1, T2, T3 : real) =
let delta = 0.2 in
exist eps1, eps2, eps3 : real in
assert between(eps1, -0.1, 0.1) in
assert between(eps2, -0.1, 0.1) in
assert between(eps3, -0.1, 0.1) in
loop {
-- init
T = 7.0 and T1 = T and T2 = T and T3 = T
fby
loop ~50:8 {
T = pre T + (if Heat_on then delta else -delta) and
T1 = T + eps1 and T2 = T + eps2 and T3 = T + eps3
}
fby -- one sensor is broken
loop ~30 {
T = pre T + (if Heat_on then delta else -delta) and
T1 = T + eps1 and T2 = T + eps2 and T3 = pre T3
}
fby -- two sensors are broken
loop ~20 {
T = pre T + (if Heat_on then delta else -delta) and
T1 = T + eps1 and T2 = pre T2 and T3 = pre T3
}
-- all the three sensors are broken
-- start again from the beginning
}
--
-- 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
node abs (v : real) returns (a : real) ;
let
a = if v >= 0.0 then v else -v ;
tel
-- returns the average values of 2 reals
node Average(a, b: real) returns (z : real);
let
z = (a+b)/2.0 ;
tel
-- returns the median values of 3 reals
node 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
node max2 (one, two : real) returns (m : real) ;
let
m = if one > two then one else two ;
tel
-- returns the minimum values of 2 reals
node min2 (one, two : real) returns (m : real) ;
let
m = if one < two then one else two ;
tel
node noneoftree (f1, f2, f3 : bool) returns (r : bool)
let
r = not f1 and not f2 and not f3 ;
tel
node alloftree (f1, f2, f3 : bool) returns (r : bool)
let
r = f1 and f2 and f3 ;
tel
node 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
-- Will be automatically generated in the future :P
node main(Heat_on : bool) returns (T, T1, T2, T3 : real) =
loop {
(0.0 < T) and (T < 1.0) and
(0.0 < T1) and (T1 < 1.0) and
(0.0 < T2) and (T2 < 1.0) and
(0.0 < T3) and (T3 < 1.0)
}
-- Simulate perfect sensors that never get worn
let between(x, min, max : real): bool = (min < x) and (x < max)
node main(Heat_on : bool) returns (T, T1, T2, T3 : real) =
let delta = 0.2 in
exist eps1, eps2, eps3 : real in
assert between(eps1, -0.1, 0.1) in
assert between(eps2, -0.1, 0.1) in
assert between(eps3, -0.1, 0.1) in
( T = 7.0 and
T1 = T + eps1 and
T2 = T + eps2 and
T3 = T + eps3 )
fby
loop {
(T = pre T + (if Heat_on then delta else -delta)) and
T1 = T + eps1 and
T2 = T + eps2 and
T3 = T + eps3
}
LURETTETOP=../../../../$(HOSTTYPE)/bin/lurettetop
ifeq ($(HOSTTYPE),win32)
RM=del /q
LURETTETOP=u:/lurette/win32/bin/lurettetop.bat
else
RM=rm -f
endif
# heater_ctrl_int.lus temp_int.lut
test1:
$(RM) test1.rif0 && \
$(LURETTETOP) \
-l 30 -td 10 --sut heater_ctrl_int.lus -msn heater_ctrl_int --seed 1 \
--draw-inside 10 --draw-edges 10 --draw-all-vertices --draw-vertices 10 \
--do-not-show-step -ns2c -go -o test1.rif0 --draw-inside 10 --draw-edges 10 \
-go temp_int.lut &&\
grep -v "lurette chronogram" test1.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" \
> test1.rif &&\
$(RM) test1.res && diff -u -i test1.rif.exp test1.rif > test1.res
[ ! -s test1.res ] && make clean
# heater_ctrl_float.lus temp_float.lut
test2:
$(RM) test2.rif0 && \
$(LURETTETOP) \
-l 30 -td 10 --sut heater_ctrl_float.lus -msn heater_ctrl_float --seed 1 \
--draw-inside 10 --draw-edges 10 --draw-all-vertices --draw-vertices 10 \
--do-not-show-step -ns2c -go -o test2.rif0 --draw-inside 10 --draw-edges 10 \
--precision 4 -go temp_float.lut &&\
grep -v "lurette chronogram" test2.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//"\
> test2.rif &&\
$(RM) test2.res && diff -u -i test2.rif.exp test2.rif \
> test2.res
[ ! -s test2.res ] && make clean
# heater_ctrl.lus window.lut
test3 :
$(RM) test3.rif0 && \
$(LURETTETOP) -l 250 -go -seed 1 \
--do-not-show-step -ns2c -sut heater_ctrl.lus -msn heater_ctrl -o test3.rif0 window.lut &&\
grep -v "lurette chronogram" test3.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test3.rif && \
$(RM) test3.res && diff -u -i test3.rif.exp test3.rif > test3.res
[ ! -s test3.res ] && make clean
test : test1 test2 test3
utest1:
cp test1.rif test1.rif.exp
utest2:
cp test2.rif test2.rif.exp
utest3:
cp test3.rif test3.rif.exp
utest: utest1 utest2 utest3
clean:
$(RM) -rf *.ec *.log *~ Data *.pp_luc *.rif0 *.rif
node heater_ctrl(t:real) returns (T: real; On:bool);
let
T = 10. ;
On = true ->
if t < 15.
then true
else if t > 20.
then false
else pre On;
tel
node heater_ctrl_float(U:real) returns (Heat_on:bool);
let
Heat_on = false ->
if U < 15.
then true
else if U > 20.
then false
else pre Heat_on;
tel
node heater_ctrl_int(U:int) returns (Heat_on:bool);
let
Heat_on = true ->
if U < 15
then true
else if U > 20
then false
else pre Heat_on;
tel
-- Temperatures are floats
let between(x, min, max : real): bool = (min < x) and (x < max)
node main(Heat_on : bool) returns (U : real) =
exist Dudt : real in
U = 17.0 and Dudt = 0.0
fby
loop {
U = pre U + pre Dudt and
if Heat_on then between(Dudt, 0.0, 2.0) else between(Dudt, -5.0, 0.0)
}
-- Temperatures are integers
let between(x, min, max : int): bool = (min < x) and (x < max)
node main(Heat_on : bool) returns (U : int) =
exist Dudt : int; Toto : bool in
U = 17 and Dudt = 0
fby
loop {
U = pre U + pre Dudt and Toto = Heat_on and
if Heat_on then between(Dudt, 0, 2) else between(Dudt, -5, 0)
}
--
-- This program simulates the temperature in a room that contains a
-- heater and a window which is opened from times to times.
let between(x, min, max : real): bool = (min < x) and (x < max)
let betweenI(x, min, max : int): bool = (min <= x) and (x <= max)
-- Input variables are a Boolean On, which is true if the
-- heater is on and false otherwise; and a rational T, which indicates
-- the temperature outside the room (behind the window).
-- The only output variable is a rational t, which simulates the
-- temperature inside the room.
node main(T : real; On : bool) returns (t: real) =
-- Local variables are the float delta, which is used to compute
-- the new temperature, and the integer cpt, which is used to count
-- the number of steps the window remains open (before rebooting).
exist delta : real; cpt : int in
t = 17.0 and cpt = 0 and delta = 0.0
fby
loop {
-- If the heater is on (resp off), only 2 choices are possible among the
-- 3 choices : indeed, the choice labelled by not On (resp On) is
-- unsatisfiable. The first possible choice has weight 100, and the other
-- one has weight 1.
--
-- o The first choice will therefore be choosed with a probability of
-- 100/101. The elected formula is therefore t = pre t + delta and
-- 0.0 < delta < 0.5 (resp -0.5 < delta < 0.0). It states that the local
-- variable delta will be uniformally drawn between 0 and 0.5 (resp
-- -0.5 and 0.0), and that delta is then used to increase (resp decrease)
-- the temperature. This is intended to model that, when the heater is
-- on (resp off), the temperature increases (resp decreases) slightly
-- with a little bit of non-determinism.
--
-- o The second choice will be drawn with a probability of 1/101. The
-- elected formula is 10 <= cpt <= 15 and t = (3 * pre t + T) / 4. It
-- states that the local integer variable cpt is drawn uniformally
-- between 10 and 15, and defines how long the new temperature is
-- computed. This is intended to model that, whenever the window is open,
-- the temperature become closer to the temperature outside.
-- Once that cpt becomes null (after between 10 and 15 steps) i.e. once
-- that the window is closed, the temperature restarts to increase or
-- decrease depending on the heater situation i.e. depending on On value.
{
|100: On
and between(delta, 0.0, 0.5) and t = pre t + delta and cpt = 0
|100: not On
and between(delta, -0.5, 0.0) and t = pre t + delta and cpt = 0
|1: betweenI(cpt, 10, 15) and t = pre t and delta = pre delta
fby
--loop {
-- pre cpt > 0 and cpt = pre cpt -1 and delta = 0.0 and
-- t = ( 3.0 * (pre t) + T ) / 4.0
--}
loop [pre cpt, pre cpt] {
delta = 0.0 and cpt = pre cpt and
t = ( 3.0 * (pre t) + T ) / 4.0
}
}
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment