Corrige de l'examen de dec. 2006.

Exercice 1.

(* en Lucid Synchrone. Ce programme est rejete par le calcul d'horloges *)
let node unbounded x = (o, h) where
  rec o = x && (x when h)
  and h = true fby not h

(* Il y a une erreur dans la note de bas de page. La relation
quasi-synchrone est un peu plus complexe que l'alternance; entre
deux occurrence de l'un, il y a 0, 1 ou 2 occurrence du second *)

(* compter le nb. d'occurrences de [a]; en re-initialisant sur [r] *)
let node counter a r = ok where
  rec
    reset
       cpt = (if a then 1 else 0) + (0 fby cpt)
    every r

(* une solution un peu generale *)
let node alternate a b = ok where
  rec ca = counter a b
  and cb = counter b a
  and ok = (ca <= 1) && (cb <= 1)

Exercice 2.

L'exercice reprend quelques idees de l'article de Colaco et al. [EMSOFT'05]
mais sans aucun soucis d'efficacite. En particulier, on genere du Lustre
"plat" c'est-a-dire ou toutes les branches d'une structure de controle
sont calculees a chaque cycle.

node until(x: bool)
returns (ok: bool) let ok = false -> if pre x then true else pre ok;
tel;

node unless(x: bool) returns (ok: bool)
  let
    ok = x -> if x then true else pre ok;
  tel;

node init(x: bool) returns (ok: bool)
  let
    ok = true -> pre(if x then false else ok)
  tel;

Question 2:

Ces deux programmes ne sont pas equivalents. Le second calcule
la suite -1 -1 0 1 1 ...

node question2(x: bool) returns (cpt: int)
  var cond: bool;
  let
    cpt = if cond then 42 -> pre cpt + 1 else -1 -> pre cpt;
    cond = false -> (pre (false -> not (pre cond)));
  tel;

-- un codage en Lustre.
node followed_by(cond: bool; x: int; y: int) returns (o: int)
  let
    o = if init(cond) then x else y;
  tel;

node question2_equivalent(x: bool) returns (cpt: int)
  var cond: bool;
  let
    cpt = if cond then followed_by(cond,  42, pre cpt + 1)
          else -1 -> pre cpt;
    cond = false -> (pre (false -> not (pre cond)));
  tel;


Les codages proposes ici ne cherchent pas l'efficacite. On pourra chercher,
en particulier, a reduire le nombre de copies inutiles de variables.

Principe de la traduction:

Pour chaque bloc, on calcule l'ensemble des
variables definies:

Def(D1 and D2) = Def(D1) U Def(D2)
Def(x = e) = {x}
Def(do D1 until e then D2) = Def(D1) U Def(D2)
                             (en verifiant que l'intersection est vide)
Def(do D1 unless e then D2) = Def(D1) U Def(D2)
                             (en verifiant que l'intersection est vide)
Def(loop D) = Def(D)
Def(D1 then D2) = Def(D1) U Def(D2)
                             (en verifiant que l'intersection est vide)
Def(wabort D when e) = Def(D)

Principe de la traduction:

Sous un bloc active par une condition c:

- e1 -> e2 devient if init(c) then e1 else e2.

- pour chaque bloc D qui ne definit pas x a chaque cycle (e.g.,
  activate D when e), la valeur de x devient:

  x = if c then D(x) else -1 -> pre(x)

  ou D(x) designe l'expression associee a x dans D.

- chaque occurrence de pre x dans un bloc D est remplacee
  par une variable fraiche pre_x_c et on ajoute en parallele l'equation:

  pre_x_c = -1 -> pre(if c then x else pre_x_c)

  autrement dit, pre_x_c contient la valeur precedente de x la derniere
  fois que c etait vraie.

Si Trad(c)(D) = { x1 = e1;...;xn = en }.

Trad(c)(activate D when c') =
  let { x1 = e1;...; xn = en } = Trad(c & c')(D) in
  { x1 = if c' then e1 else px1;
    ...;
    xn = if c' then en else pxn;
    px1 = -1 -> pre x1;...; pxn = -1 -> pre xn }

Trad(c)(when c' do D else D') =
  let { x1 = e1;...; xn = en } = Trad(c & c')(D) in
  let { x1 = e1';...; xn = en' } = Trad(c & not c')(D') in
  { x1 = if c' then e1 else e1';
    ...;
    xn = if c' then en else en' }

Trad(c)(D1 and D2) = Trad(c)(D1) U Trad(c)(D2)

La traduction d'une expression:

Trad(c)(e) = e' + { x1 = e1;...; xn = en}

Trad(c)(pre x) = px + { px = -1 -> pre (if c then x else px) }
Trad(c)(x) = x + { }
Trad(c)(e1 -> e2) = init(c)

Attention: il faut veiller a introduire des noms de variable frais
(ici px).

Rmq: pour traiter le reset, introduire directement
node init(c, r) returns ok
  let ok = true -> if r then true else pre(if x then false else ok);
  tel;
  
On demarre avec Trad(true)(D).

Question 4:
Il faut que la condition c ne depende pas instantanement des variables
de D (cad Def(D)).

Question 5:

-- code en Lustre. 
node question5(x: bool) returns (cpt: int;cond: bool)
  var 
      cpt0, cpt1: int;
  let
    cpt0 = if cond then if init(cond) then 42
           else pre cpt0 - 1 else -1 -> pre cpt0;
    cpt1 = if not cond then if init(not cond) then 45 else pre cpt1 + 1
           else -1 -> pre cpt1;
    cpt = if cond then cpt0 else cpt1;
    cond = false -> (pre (false -> (pre (false -> not (pre cond)))));
  tel;

Question 7:

(do D when c) peut se traduire en:

  (do D when c else x1 = px1 and ... and xn = pxn done) 
  and px1 = pre(x1) and ... and pxn = pre(xn)

Question 7:

(do D1 until c then D2 done) se traduit en:

(do D2 when (until(c)) else D1 done)

(do D1 until c then D2 done) se traduit en:

(do D2 when (unless(c)) else D1 done)

Question 8: La meme contrainte qu'auparavant convient. Dans le cas
de la transition faible (until), elle est trop contraignante cependant.
c peut dependre intantanement des variables de D1. Par contre, pour une
transition unless, c ne doit pas dependre des elements de Def(D1).


Question 9:

Le reset agit sur l'operation d'initialisation ->. Le plus
simple est d'introduire un init(c, r) et de definir:

Trad(c)(r)(e) et Trad(c)(r)(D)

qui parcourt recursivement les expression et les declarations. Par
rapport a la version precedente, on change la definition de ->. Le
reste est inchange.

Question 10:

- wabort D when e =def do D and end = false until e then end = true.
- loop D =def reset D every false -> pre end
- D1 then D2 =def do D1 until end then D2

Pour obtenir une solution satisfaisante, il faut traiter
le cas de definitions partielles, e.g.,

do x = ex when c else y = ey

qui peut etre interprete par:

do x = ex and y = py until c then y = ey and x = px
and
px = pre x and y = pre y

autrement, en l'absence de definition pour une variable, on
considere qu'elle maintient sa valeur.