# Time-stamp: <modified the 30/03/2022 (at 15:03) by Erwan Jahier>
#+LANGUAGE: fr
#+LATEX_HEADER: \input{include/header}
#+OPTIONS: H:3 toc:t \n:nil @:t ::t |:t ^:t -:t f:t *:t TeX:t LaTeX:nil skip:nil tags:not-in-toc
#+SETUPFILE: include/theme-readtheorg.setup
#+TITLE: Test du programme phare
#+AUTHOR: GHERRAZ Salah BERNABE Aurelien
* TODO [3/4] Le Système sous test (ou SUT, pour System Under Test)
Le SUT est constitué d'un programme C nommé file:phare.c (qui est
obtenu par la commande =make noweb= ou =Ctrl-c Ctrl-v t= depuis
=emacs=). Ce programme importe les librairies nécessaires
#+BEGIN_SRC c :tangle phare.c
#include <stdlib.h>
#include <stdio.h>
#include <unistd.h>
#+END_SRC
et défini
- des fonctions pour lire du RIF sur l'entrée standard (stdin)
- quelques constantes utiles
- la fonction =phares_step()=
- la fonction =main()=
#+BEGIN_SRC c :tangle phare.c :noweb no-export
<<read-rif>>
<<def-constantes>>
<<phares-step>>
<<main>>
#+END_SRC
Notez (depuis le source =.org=) le =:noweb no-export= en entête du
bloc source qui permet expanser les définitions des chuncks dans le
fichier C, mais pas dans l'export html.
** DONE La lecture du rif
est effectuée à l'aide de =scanf= :
#+NAME: read-rif
#+BEGIN_SRC c :noweb tangle
int _get_int(char* n){
char b[512];
int r;
int s = 1;
do {
if(scanf("%s", b)==EOF) exit(0);
if (*b == 'q') exit(0);
s = sscanf(b, "%d", &r);
} while(s != 1);
return r;
}
#define REALFORMAT ((sizeof(double)==8)?"%lf":"%f")
double _get_double(char* n){
char b[512];
double r;
int s = 1;
do {
if(scanf("%s", b)==EOF) exit(0);
if (*b == 'q') exit(0);
s = sscanf(b, REALFORMAT, &r);
} while(s != 1);
return r;
}
#+END_SRC
** DONE Quelques constantes utiles
pour rendre le programme plus lisible :
#+name: def-constantes
#+BEGIN_SRC c
typedef int SwitchMode;
#define ON 0
#define OFF 1
#define AUTO 2
typedef int boolean;
#define false 0
#define true 1
double period = 0.5;
boolean pre_InAuto;
boolean pre_is_on;
#+END_SRC
** DONE Le programme principal
est une simple boucle infinie qui lit et écrit des données au format
RIF, pour que =lurette= puisse interagir avec.
#+name: main
#+BEGIN_SRC c
/////////////////////////////////////////////////////////////////
/* Main procedure that wraps the step() function using RIF conventions */
int main(){
int _s = 0; // time counter
SwitchMode switch_pos;
double intensity;
boolean is_on;
printf("#inputs \"switch_pos\":int \"intensity\":real\n");
printf("#outputs \"is_on\":bool\n");
fflush(stdout);
/* Main loop */
while(1){
printf("#step %d \n", _s+1); fflush(stdout);
++_s;
switch_pos = _get_int("switch_pos");
intensity = _get_double("intensity");
phares_step(switch_pos,intensity,&is_on);
printf("%d\n",is_on);
fflush(stdout);
}
return 1;
}
#+END_SRC
** TODO La fonction step (*qu'il vous faut finir*)
et qui constitue le coeur du SUT :
#+name: phares-step
#+BEGIN_SRC c
double timer = 0.0;
void phares_step(SwitchMode switch_pos, double intensity, boolean *is_on){
// XXX finish me
// calcule is_on en fonction de intensity et switch_pos
switch (switch_pos) {
case ON:
*is_on = true;
break;
case OFF:
*is_on = false;
break;
case AUTO:
if(is_on){
if(intensity > 70){
timer += period;
if(timer >= 3){
timer = 0;
*is_on = false;
}
}
}else{
if(intensity < 60){
timer += period;
if(timer >= 2){
timer = 0;
*is_on = true;
}
}
// timer 2s
}
break;
}
} // End of phares_step
#+END_SRC
* TODO [1/6] Les oracles du test
Les oracles permettent de décider si les tests se sont bien déroulés.
Pour cela, nous allons utiliser une formalisation des exigences
fonctionnelles en logique temporelle via des programmes Lustre (ceux
effectuées lors du TP 8) :
** DONE L'exigence =REQ_001=
dit : "if the switch is ON then the headlights must turn immediately
on". Ce que nous pouvons formaliser en Lustre ainsi :
#+BEGIN_SRC lustre :tangle phare_prop.lus :export none
include "util.lus"
include "num_real.lus"
#+END_SRC
#+BEGIN_SRC lustre :tangle phare_prop.lus
function req1(switch_pos: SwitchMode; intensity: num; is_on:bool) returns (res, cov:bool);
let
res = (switch_pos=ON) => is_on;
cov = switch_pos=ON;
tel
#+END_SRC
Remarquer la définition de la variable =cov=, qui n'intervient pas
dans le calcul du résultat, et qui sert juste ici à définir un critère
de couverture pour cet oracle.
** TODO L'exigence =REQ_002=
XXX recopier vos oracles du TP 8 en les adaptant pour rajouter des
critères de couverture pertinents (c'est-à-dire, en définissant des
valeurs pertinentes pour les sorties =cov=, comme je l'ai fait pour le
=req1=).
#+BEGIN_SRC lustre :tangle phare_prop.lus
function req2(switch_pos: SwitchMode; intensity: real; is_on:bool)
returns (res,cov:bool);
let
res = (switch_pos=OFF) => not(is_on);
cov = switch_pos = OFF;
tel
#+END_SRC
** TODO L'exigence =REQ_003.1=
#+BEGIN_SRC lustre :tangle phare_prop.lus
node req31(switch_pos: SwitchMode; intensity: real;is_on:bool)
returns (res,cov1,cov2:bool);
var
p1,p2:bool;
auto:bool;
let
auto = (switch_pos = AUTO);
cov1 = (front_montant(auto) and (intensity <= seuil_haut));
p1 = cov1 => is_on;
cov2 = false -> if not(pre(cov2)) then cov1 else pre(cov2) and auto and (intensity <= seuil_haut);
p2 = cov2 => is_on;
res = p1 and p2;
tel
#+END_SRC
** TODO L'exigence =REQ_003.2=
#+BEGIN_SRC lustre :tangle phare_prop.lus
node req32(switch_pos: SwitchMode; intensity: real;is_on:bool)
returns (res, cov1, cov2 :bool);
var
c1,c2,p1,p2: bool;
auto: bool;
let
auto = (switch_pos = AUTO);
cov1 = (front_montant(auto) and (intensity > seuil_haut));
p1 = cov1 => not(is_on);
cov2 = false -> if not(pre(cov2)) then cov1 else pre(cov2) and auto and (intensity >= seuil_bas);
p2 = cov2 => not(is_on);
res = p1 and p2;
tel
#+END_SRC
** TODO L'exigence =REQ_003.3=
#+BEGIN_SRC lustre :tangle phare_prop.lus
node req33(switch_pos: SwitchMode; intensity: real; is_on: bool)
returns (res,cov:bool);
var
c: bool;
auto: bool;
let
auto = (switch_pos = AUTO);
c = (not pre(is_on)) and auto and (intensity <= 0.6);
cov = vrai_depuis_n_secondes(c , _2_sec);
res = cov => is_on;
tel
#+END_SRC
** TODO L'exigence =REQ_003.4=
#+BEGIN_SRC lustre :tangle phare_prop.lus
node req34(switch_pos: SwitchMode; intensity: real;is_on:bool)
returns (res,cov:bool);
var
c: bool;
auto: bool;
let
auto = (switch_pos = AUTO);
c = pre(is_on) and auto and (intensity > 0.7);
cov = vrai_depuis_n_secondes(c , _3_sec);
res = cov => not(is_on);
tel
#+END_SRC
Et voici le noeud principal, qui va être utilisé par =lurette= pour
décider si les tests se passent bien, et pour calculer le taux de
couverture :
#+BEGIN_SRC lustre :tangle phare_prop.lus
node all(switch_pos: SwitchMode; intensity: real; is_on:bool)
returns (res,cov_Req1,cov_Req2,cov_Req31_1,cov_Req31_2,cov_Req32_1,
cov_Req32_2,cov_Req33,cov_Req34:bool);
var
Req1,Req2,Req31,Req32,Req33,Req34:bool;
let
Req1,cov_Req1 = req1(switch_pos, intensity, is_on);
Req2,cov_Req2 = req2(switch_pos, intensity, is_on);
Req31,cov_Req31_1,cov_Req31_2 = req31(switch_pos, intensity, is_on);
Req32,cov_Req32_1,cov_Req32_2 = req32(switch_pos, intensity, is_on);
Req33,cov_Req33 = req33(switch_pos, intensity, is_on);
Req34,cov_Req34 = req34(switch_pos, intensity, is_on);
res = Req1 and Req2 and Req31 and Req32 and Req33 and Req34;
tel
#+END_SRC
#+BEGIN_SRC lustre :tangle num_real.lus :exports none
type SwitchMode = int;
const
ON=0;
OFF=1;
AUTO=2;
type num=real;
const seuil_bas = 60.0;
const seuil_haut = 70.0;
const zero = 0.0;
const period = 0.5; -- en s
const _2_sec = 2.0; -- en s
const _3_sec = 3.0; -- en s
#+END_SRC
#+BEGIN_SRC lustre :tangle util.lus :exports none
node front_montant(x : bool) returns (res : bool);
let
res = x -> (x and not pre(x));
tel
node max(x,y:num) returns (res:num);
let
res = if x>y then x else y;
tel
node vrai_depuis_n_secondes(signal: bool; n: num) returns (res: bool);
var
tempo : num;
let
tempo = n -> if not signal then n else max (zero, pre tempo - period);
res = (tempo = zero);
tel
#+END_SRC
* DONE La génération des entrées
Dans un premier temps, la génération des entrées peut se faire à
l'aide d'un programme lutin qui se contente de tirer au hasard.
#+BEGIN_SRC lutin :tangle phare_env.lut
node au_hasard(is_on:bool)
returns(switch_pos: int [0;2];intensity: real [0.0;100.0]) =
loop true
#+END_SRC
* Lancer les tests avec =lurette=
Après avoir compilé votre programme file:phare.c avec =gcc=
#+BEGIN_SRC sh
gcc phare.c -o phare
#+END_SRC
ou via le file:Makefike (que je n'ai pas mis dans le .org cette fois
ci) :
#+BEGIN_SRC sh
make phare
#+END_SRC
Nous pouvons lancer les tests avec =lurette=, pendant 500 steps, et en
enregistrant les valeurs générées dans file:phare.rif ainsi :
#+BEGIN_SRC sh
lurette -l 500 -o phare.rif \
-sut "./phare" \
-env "lutin phare_env.lut -n au_hasard" \
-oracle "lv6 -rif phare_prop.lus -n all"
#+END_SRC
Ou bien via le file:Makefike ainsi :
#+BEGIN_SRC sh
make all.test
#+END_SRC
Notez qu'il peut être pratique, lors de la phase de mise au point, de ne
pas lancer tous les oracles en même temps.
#+BEGIN_SRC sh
make req1.test
#+END_SRC
lance les tests en utilisant que le noeud =req1= comme seul oracle. Cela
rend les messages d'erreurs (un peu) plus faciles à interpréter.
* Visualisation du rif
Comme les autres fois, on peut visualiser les =.rif= générés avec
=sim2chro= ou =gnuplot-rif=
#+BEGIN_SRC sh
sim2chrogtk -in phare.rif -ecran > /dev/null
gnuplot-rif phare.rif
#+END_SRC
ou bien via le file:Makefile :
#+BEGIN_SRC sh
make s
make g
#+END_SRC
Dans =gnuplot-rif=, les variables correspondant à la couverture
font un peu de bruit dans l'affichage. On peut les cacher grâce
à un fichier file:.gnuplot-rif qui contient :
#+BEGIN_SRC text :tangle .gnuplot-rif
hide cov_*
#+END_SRC
Notez que vous pouvez *aussi* analyser les données produites lors de
vos simulations en regardant le contenu de file:phare.rif dans un
éditeur de texte (=emacs= ou autre).
* TODO Améliorer la couverture
Une fois que tous les tests passent, on peut remarquer que =lurette=
nous dit que le taux de couverture n'est pas de 100%. C'est parce que
le noeud Lutin =au_hasard= n'est pas assez malin.
Nous allons donc écrire un noeud Lutin =plus_malin= qui va faire en
sorte que les 100% de couverture soit atteint.
#+BEGIN_SRC lutin :tangle phare_env.lut
node plus_malin(is_on:bool)
returns(switch_pos: int [0;2];intensity: real [0.0;100.0]) =
loop true // XXX a vous d'etre malin
#+END_SRC
nb : il vous faudra éditer le file:Makefile pour que =lurette= utilise le
noeud =plus_malin=.
* TODO gitlab-ci
Et voici un job =gitlab-ci= qui va permettre de lancer les tests à
chaque =git push= :
#+BEGIN_SRC yaml :tangle phare.yml
test:
rm lurette.cov ; # XXX laisser cette ligne au début de vos tests !
#+END_SRC
* TODO CR
XXX
- Faites court (l'équivalent d'une page A4 max)
- Indiquer le temps que vous y avez passé, ce que vous avez trouvé dur
ou facile (3 lignes max)
- Faites une petite synthèse de ce que vous avez fait et appris durant
le TP