Réinitisalisation (modulaire)

Bloc = Soit une liste de blocs, soit une liste d’équations soit la réinitialisation d’un bloc (entre let et tel)
Exemple de bloc de réinitialisation : reset bloc every expression

node nat_reset() returns (o : int)
var c : bool;
let
  reset o = 0 fby (o + 1) every c;
  c = true fby false fby false fby c;
tel

(* qui est équivalent à *)
node nat_reset2() returns (o : int)
var c : bool;
let
  o = if c then 0 else (0 fby (0 + 1));
  c = true fby false fby false fby c;
tel

(* exemple avec une fonction externe *)
node nat() returns (o : int)
let
  o = 0 fby (o + 1);
tel

node nat_reset() returns (o : int)
var c : bool;
let
  (* fonctionne avec une fonctionne *)
  reset o = nat() every c;
  c = true fby false fby false fby c;
tel

(* ça, ça ne fonctionne pas *)
node nat_reset2() returns (o : int)
var c : bool;
let
  o = if c then 0 else nat();
  c = true fby false fby false fby c;
tel

Reset = réinitialisation modulaire, passe à travers les abstractions
Utile, mais rend le programme rapidement incompréhensible.

Types structurés et énumérés

Types structurés

type cpl = { re : float; im : float }

node add(x, y: cpl) returns (o: cpl)
let
  o = { re = x.re +. y.re
      ; im = x.im +. y.im };
tel

node conj(x: cpl) returns (o: cpl)
let
  o = { re = x.re
      ; im = -.x.im };
tel

Mot-clé fun permet de définir une node qui ne dépend pas du temps (pas d’état). Donc, par exemple, fby est rejeté des fun.

type cpl = { re : float; im : float }

fun add(x, y: cpl) returns (o: cpl)
let
  o = { re = x.re +. y.re
      ; im = x.im +. y.im };
tel

fun conj(x: cpl) returns (o: cpl)
let
  o = { re = x.re
      ; im = -.x.im };
tel

Types énumérés

type alpha = A | B | C (* commence par une majuscule, alpha est soit A, B, ou C *)
type etats = X | Y | Z | Mort

node automate(l : alpha) returns (accept : bool)
var etat_courant, etat_precedent : etats;
let
  etat_courant =      if (etat_precedent, l) = (X, A) then Y
                 else if (etat_precedent, l) = (Y, B) then Z
                 else if (etat_precedent, l) = (Y, C) then Y
                 else if (etat_precedent, l) = (Z, A) then Y
                 else Mort;
  etat_precedent = X fby etat_courant;
  accept = (etat_courant = Z);
tel

Horloges

Exercice : Définir une suite o : int telle que o_{2k} = k o_{2k+1}=0

o = 0, 0, 1, 0, 2, 0, 3, 0, 4, 0, \dots

node k() returns (o: int)
var p: bool; v: int;
let
  o = if p then v else 0;
  v = 0 fby if p then v else (v + 1);
  p = true fby not p;
tel

On remarque que o c’est la suite naturelle séparée de 0.
On peut donc mélanger/entrelacés la suite des entiers naturels et la suite des 0.

Opérateur d’entrelacement merge

node nat() returns (o : int)
let
  o = 0 fby (o + 1);
tel

node k() returns (o: int)
var p: bool; v: int;
let
  o = merge p v 0;
  v = nat();
  p = true fby not p;
tel

Contrairement au if qui va perdre des données, le mélange entrelace les flux alors que le if/else choisis quelle valeur garder à un instant t.

Dans notre cas, p est notre horloge, p permet d’alterner le calcul entre p et v.

Sémantique

\begin{aligned} & \lb \text{merge } c e_{1} e_{2} \rb \\ &\begin{cases} \lb e_{1} \rb_{k} & \text{si } \lb c \rb_{k} = \text{ true et } \lb e_{1} \rb \neq \text{abs}, \lb e_{2} \rb_{k} = \text{abs} \\ \lb e_{2} \rb_{k} & \text{si } \lb c \rb_{k} = \text{ false et } \lb e_{1} \rb = \text{abs}, \lb e_{2} \rb_{k} \neq \text{abs} \\ \text{abs} & \text{si } \lb c \rb_{k} = \text{ abs et } \lb e_{1} \rb = \lb e_{2} \rb_{k} = \text{abs} \end{cases} \end{aligned}

Opérateur de sélection (échantillonnage) e when c

Sémantique

\begin{aligned} & \lb e \text{ when } c \rb \\ &\begin{cases} \lb e \rb_{k} & \text{si } \lb c \rb_{k} = \text{ true et } \lb e \rb_{k} \neq \text{abs} \\ \text{abs} & \text{si } \lb c \rb_{k} = \text{ false et } \lb c \rb_{k} = \text{abs} \end{cases} \end{aligned}

En contraste, voici le tableau pour les additions

\lb e_{1} \rb_{k}	\lb e_{2} \rb_{k}	\lb e_{1} + e_{2} \rb_{k}
\neq abs	\neq abs	\lb e_{1} \rb_{k} + \lb e_{2} \rb_{k}
abs	abs	abs

Si on a une sortie avec une horloge spéciale, il faut renvoyer l’horloge

node nat() returns (o : int)
let
  o = 0 fby (o + 1);
tel

node h() returns (p: bool; o: int)
var x : int;
let
  x = nat();
  p = true fby not p;
  o = x when p;
tel

when false(p) = when not p