Commit 4528bd02 authored by erwan's avatar erwan

Some cleaning in the examples directory.

parent cc6125c5
OASISFormat: 0.4
Name: Lutin
Version: 2.51
Version: 2.52
Authors: Erwan Jahier, Pascal Raymond, Bertrand Jeannnet (polka), Yvan Roux
Maintainers: erwan.jahier@univ-grenoble-alpes.fr
License: CeCILL
......
......@@ -9,8 +9,9 @@ test:
cd call-luciole && make test ;
cd from_ocaml && make test;
cd external_code && make test;
cd luciole && make test ;
cd call-luciole && make test ;
cd crazy-rabbit && make test;
cd StimulusLib/ && make test;
echo "All lutin tests ran correctly."
# XXX Broken !
......
EXE=
ifeq ($(HOSTTYPE),win32)
EXE=.exe
endif
ifndef LUTIN
LUTIN=lutin
endif
EXPDIR=`$(LUTIN) --ocaml-version`
$(EXPDIR):
[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
test.rif :
lurette -l 100 -o test.rif0 \
-sut "lutin -seed 1 temporal.lut -main main" \
-env "lutin -seed 1 temporal.lut -main env"
cat test.rif0 | sed -e "s/^M//" | grep -v " Version" > test.rif
test:test.rif $(EXPDIR)
rm -f test.res && diff -B -u -i -w $(EXPDIR)/test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
utest:test.rif
cp test.rif $(EXPDIR)/test.rif.exp ; true
clean:
rm -rf $(OBJDIR) rm -rf *.res *.log *~ *.rif0 *.rif *.gp *.plot
Mimick in Lutin the Stimulus (Argosim) standard lib.
......@@ -67,6 +67,7 @@ node test_OnceBefore(event : bool) returns( condition : bool) =
OnceBefore(condition,event)
node env() returns (event:bool) = loop [50] event fby true
node main(event:bool) returns (res:int) =
......
Illustrate and test the use of Lutin via gnuplot-rif.
This directory contains examples that are not tracked by the test
scripts, which means that some (most) programs might not (even) be
syntactically correct (anymore).
#
# Testing the use of the --oracle-* option
#
EXE=
ifeq ($(HOSTTYPE),cross-win32)
EXE=.exe
endif
LUTIN=../../../bin/lutin$(EXE) -seed 1 -boot --load-mem
test : test1 test2 clear
not_a_sauna.ec: heater_control.lus
lus2lic -n not_a_sauna -ec $< -o $@
test1 : not_a_sauna.ec
rm -f test1.rif
echo -e "0.0 0.0 0.0 0.0\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\n" | \
$(LUTIN) env.lut -main main --oracle-ec $< -rif test1.rif || true
cat test1.rif | sed -e "s/^M//" | grep -v "This is lutin" > test1.rif
rm -f test1.res && diff -B -u -i -w test1.rif.exp test1.rif > test1.res
test2 : not_a_sauna.ec
rm -f test2.rif
echo -e "0.0 0.0 0.0 0.0\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\n" | \
$(LUTIN) env.lut -main main --oracle-ec $< | sed -e "s/^M//" | grep -v "This is lutin" > test2.rif
rm -f test2.res && diff -B -u -i -w test2.rif.exp test2.rif > test2.res
clear:
[ ! -s test1.res ] && [ ! -s test2.res ] && make clean
utest1:
cp test1.rif test1.rif.exp ; true
utest2:
cp test2.rif test2.rif.exp ; true
utest:utest1 utest2
clean:
rm -rf $(OBJDIR) rm -rf *.res *.log *~ *.rif0 *.rif *.gp *.plot *.ec *.cov
let between(x, min, max : real) : bool =
((min < x) and (x < max))
node main(Heat_on : bool) returns (
T : real;
T1 : real;
T2 : real;
T3 : real) =
assert between(T1, T-1.5, T + 1.5) in
assert between(T2, T-1.5, T + 1.5) in
assert between(T3, T-1.5, T + 1.5) in
{
(6.0 < T) and (T < 9.0)
}
fby
loop { if Heat_on then
between(T, pre T, pre T + 0.5)
else
between(T, pre T - 0.5, pre T)
}
--
-- 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, C1, C2, C3:bool);
let
-- Some stupid coverage criteria...
C1 = T > T1;
C2 = T > T2;
C3 = T > T3;
ok =
(C1 => (T < TMAX + 1.0)) and
(C2 => (T < TMAX + 1.0)) and
(C3 => (T < TMAX + 1.0)) ;
tel
node not_a_fridge(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
let str="2.51"
let sha="8e78a39"
let str="2.52"
let sha="cc6125c"
Markdown is supported
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