Untitled

# 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