Chapitre 9 sur 10. Modéliser une capacité explicite puis une exclusion mutuelle sur des opérations qui durent.
1. Compter les emplacements libres
Un service produit des dossiers que le suivant consomme. Le tampon comporte deux emplacements. Deux places suffisent pour le modèle atomique : Libres et Pleines, initialement (2,0). Produire prend un jeton Libre et produit un jeton Pleine. Consommer réalise l’inverse.
La capacité n’est pas un nombre décoratif attaché au dessin : elle est représentée par les deux jetons disponibles. Quand Libres = 0, Produire est bloquée. Quand Pleines = 0, Consommer est bloquée.
2. Lire toutes les occupations possibles
Les trois marquages accessibles sont (2,0), (1,1) et (0,2). L’invariant Libres + Pleines = 2 démontre que le tampon ne dépasse jamais deux éléments. Le modèle n’est pas sauf, mais il est 2-borné.
Il n’existe aucun état bloqué : tampon vide, on peut produire ; tampon plein, on peut consommer ; à mi-capacité, les deux sont possibles. Les deux transitions sont vivantes dans ce modèle fermé. Il ne calcule toutefois ni débit ni temps d’attente ; aucun temps de production ou de consommation n’a été fourni.
3. Réserver un accès pendant une opération
Pour représenter une écriture ou une lecture en cours, ajoutons Mutex, Écriture et Lecture. L’ordre devient (Libres, Pleines, Mutex, Écriture, Lecture) et M₀ = (2,0,1,0,0). Début écriture prend Libre + Mutex et produit Écriture. Fin écriture consomme Écriture, produit Pleine et rend Mutex. La lecture suit le même principe en sens inverse.
Deux relations doivent rester vraies : Libres + Pleines + Écriture + Lecture = 2, et Mutex + Écriture + Lecture = 1. La première compte les emplacements, y compris ceux réservés par une opération ; la seconde interdit que lecture et écriture soient en cours simultanément.
4. Vérifier les hypothèses du tampon
L’exploration trouve sept états et huit arcs pour cette variante. Une lecture en cours réserve son élément jusqu’à sa fin ; une écriture réserve déjà son emplacement. Oublier ces réservations dans l’invariant ferait croire à une perte temporaire de capacité.
Les éléments restent anonymes : ce modèle compte les occupations mais ne prouve pas un ordre FIFO. Le mutex sérialise volontairement les accès ; un tampon réel peut autoriser davantage de parallélisme avec d’autres hypothèses. Une panne qui empêcherait une transition de fin demande aussi un modèle supplémentaire.
Trois exercices corrigés
Exercice 1 : Tampon plein
Depuis (0,2), quelles transitions sont franchissables dans le modèle atomique ?
Voir la correction de l’exercice 1
Consommer seulement : il existe un élément plein et aucun emplacement libre. Après consommation, on obtient (1,1), où Produire et Consommer sont toutes deux activables.
Exercice 2 : Écriture en cours
Depuis (2,0,1,0,0), donner le marquage après Début écriture puis Fin écriture.
Voir la correction de l’exercice 2
Le début donne (1,0,0,1,0) : un emplacement et le mutex sont réservés. La fin donne (1,1,1,0,0). Dans les deux états, la conservation des emplacements vaut 2 et celle du mutex vaut 1.
Exercice 3 : Repérer une propriété non prouvée
Le réseau à deux places prouve-t-il que le premier dossier produit sera le premier consommé ?
Voir la correction de l’exercice 3
Non. Les jetons n’ont pas d’identité ni d’ordre. Le réseau prouve la capacité et certaines possibilités d’évolution, mais pas une discipline FIFO ; il faut enrichir le modèle pour exprimer cette propriété.
Références pour approfondir
Introduction universitaire PetriSim, Javier Esparza : notes universitaires sur les réseaux de Pétri. Cours, cas et figures rédigés pour PandaCodeur ; aucune figure universitaire reproduite. Les exemples NKILItech sont fictifs.