Le corrigé de l'exercice

Voici ce que je vous ai proposé :

P1 = (get -> in -> put -> P1).
P2 = (get -> out -> put -> P2).
SEM =(get -> put -> SEM).
SYS = (P1 // P2 // SEM).

Il est évident (il suffit de lire) que la première action sera une action commune aux trois processus : get. Cela signifie que P1 et P2 prennent la main (c'est le cas de synchronisation). IL N'Y A donc pas exclusion mutuelle !

Entrez la spec sur LTSA et faites un run, vous verrez...

Voici ce qu'il fallait faire :
P1 = (p1.get -> in -> p1.put -> P1).
P2 = (p2.get -> out -> p2.put -> P2).
SEM =(get -> put -> SEM).
SYS = (P1 // P2 // {p1,p2}:: SEM).

Faites l'automate et vous verrez.

Si vous ne saviez pas ce que faisait ::
vous pouviez écrire :

P1 = (p1.get -> in -> p1.put -> P1).
P2 = (p2.get -> out -> p2.put -> P2).
SEM =(p1.get -> p1.put -> SEM p2.get -> p2.put -> SEM).
SYS = (P1 // P2 // SEM).

Remarque : j'ai constaté que le "pipe" ne "passait" pas sur blogspot. Aussi ai-je utilisé //

Exercice. Faisons feu de tout bois

Je reçois ce courriel du directeur du labo d'informatique de Nantes.

A faire : l'automate (le diagramme de transition d'états) du processus. Vous étiquetterez les transitions par les événements.

"Bonjour à tous,

Le CNRS et le précédent conseil du LINA viennent de donner leur accord pour la composition de notre nouveau conseil de laboratoire.Nous vous proposons donc d'organiser l'élection de ses membres élus selon l'agenda ci-dessous et les règles décrites dans un courriel (un peu long) à suivre.Ce conseil joue un rôle essentiel dans la vie du laboratoire dont il rythme les prises de décision importantes.Nous vous invitons donc à vous porter nombreux candidats.

Pierre Cointe et Béatrice Daille

PS.

Agenda
vendredi 8 février12h00 : date et heure limites de modification des listes
jeudi 14 février 18h00 : date et heures limites de déclaration des candidatures
lundi 3 mars 10h00 : date et heure de début de réception des bulletins de vote aux trois secrétariats du LINA
vendredi 7 mars 12h00 : date et heure de clôture de réception des bulletins de vote aux trois secrétariats du LINA "