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é //