La piscine en FSP (LTSA)

Le sujet se trouve dans le polycopié des TD de Spec2, présent sur nos pages web.
Après l'avoir traité en RDP, on va le traiter en FSP.

Merci à Sébastien qui a eu l'idée et a appliqué LTSA au cas piscine.

Nous allons suivre une démarche archétypique.

Nous allons commencer par spécifier le comportement d'un client (BAIGNEUR) qui n'a aucune contrainte,i.e. comme s'il était seul client à la piscine. C'est plus facile que de vouloir tout dire du premier coup !
Bien sûr, on a dans la tête des patrons (patterns en anglais) de systèmes. Voila pourquoi nous avons utilisé des noms génériques habituels comme get une ressource, release, rendre, une ressource. Ici getp est mis pour prendre un panier, relp pour rendre panier.

BAIGNEUR = (entre -> getc -> deshabille ->
getp -> relc -> baignade -> getc -> relp ->
rhabille -relc -> sort -> BAIGNEUR).

On pouvait décomposer en :

PREPARATION = (getc -> deshabille -> getp -> relc -> BAIN),
BAIN = (baignade -> SORTIE),
SORTIE = (getc -> relp -> rhabille -relc -> sort -> BAIGNEUR),
BAIGNEUR = (entree -> PREPARATION -> BAIGNEUR).

On peut spécifier le nombre de baigneurs.

const NB_B = 3

Maintenant spécifions les contraintes.
Passons à l'économie (gestion des ressources rares). Les ressources sont les paniers, cabines.
Abstrayons le comportement des ressources, quelque soit le type de ressource, panier ou cabine.

RES_MULT(N=5) = RES_MULT[N],
RES_MULT[i:0..N]= (
when(i>0) get -> RES_MULT[i-1] |
when(i RES_MULT[i+1]
).

Spécifions le nombre de cabines et le nombre de paniers.

const NB_C = 2
const NB_P = 1

Maintenant, nous spécifions le système PISCINE en mettant en parallèle les processus baigneurs, cabines et paniers.

||PISCINE = (b[1..NB_B]:BAIGNEUR ||c: RES_MULT(NB_C) || p:RES_MULT(NB_P))

et en spécifiant les contraintes de synchronisation entre ces processus. Pour cela, on est amené à utiliser le renommage.

{b[1..NB_B].getc/c.get, b[1..NB_B].relc/c.rel, b[1..NB_B].getp/p.get, b[1..NB_B].relp/p.rel}

et l'opérateur interface :

@{b[1..NB_B].entre, b[1..NB_B].deshabille, b[1..NB_B].baignade, b[1..NB_B].rhabille, b[1..NB_B].sort}.

extrait de notre polycop Spec2, non distribué.

Petit à petit nous mettrons des extraits de ce poly (il nous faut enlever les commandes latex) sur ce bloc-notes ou sur nos pages.