SED Chap 3
SED Chap 3
SED Chap 3
1
Chapitre III
Formalisation
• L'un des intérêts de ce formalisme, c'est la possibilité de
vérifier formellement des propriétés
M. F. Karoui 2
Chapitre III
Formalisation
Réseau de Petri: R = {P, T, Pre, Post}
• P = ensemble de places (P = {P1, P2, .., Pm} )
• T = ensemble de transitions (T= {T1, T2, .., Tn})
M. F. Karoui 3
Chapitre III
Formalisation
2
P0
T0
M. F. Karoui 4
Chapitre III
Formalisation
• Exercice T1
– P?
2 7
– T? 5 T2
3
– Pré (Pi, Tj) ? P1 1 P2
– Post (Pi, Tj) ? 6
T3 4
1
M. F. Karoui 5
Chapitre III
Formalisation
Réseau de Petri: R = {P, T, Pre, Post}
=> Représentation matricielle T1
2 7
5 T2
3
P1 1 P2
6
T3 4
1
Pré : Post :
M. F. Karoui 6
Chapitre III
Formalisation
Réseau marqué: N = {R,M}
Le marquage d'un RdP R=(P, T, Pre, Post) est son état.
Formellement, un marquage est une application M:P→N
donnant pour chaque place le nombre de jetons qu'elle contient.
Le marquage initial est généralement noté M0. M0= {1,0}
Notation matricielle:
– Transitions en colonnes
– Places en lignes
– Marquage = vecteur colonne
M. F. Karoui 7
Chapitre III
Formalisation
• Exercice
Notation matricielle
Pré?
Post?
C?
M0?
M. F. Karoui 8
Chapitre III
Formalisation
M. F. Karoui 9
Chapitre III
Formalisation
M. F. Karoui 10
Chapitre III
Formalisation
C=
C=
M. F. Karoui 11
Chapitre III
Formalisation
C=
M. F. Karoui 13
Chapitre III
2 1 1
2 1 0 5 0 1
= 3 - 0 + 0
0 6 4 7 3 0
0 0
2 2 5 5
= - + =
3 0 7 10
M. F. Karoui 14
Chapitre III
2 1
3 -1 1
= 3 + 0 = 5
7 -3 -4 10
0
M. F. Karoui 15
Chapitre III
Formalisation
• Exercice
– A partir du
marquage initiale ,
calculez les
marquage suivant:
M1 après tir de T1 ,
puis M2 après tir de
T3 puis M3 après tir
de T3 puis M5 après
tir de T2 puis M6
après tir de T1
M. F. Karoui 16
Chapitre III
Formalisation
T1 T2
T3 T3
T1 T2 T3 T4
T2 est une séquence de
transitions
franchissables
M. F. Karoui 17
Chapitre III
De plus
Mn = M + C . VsT
où Vs est le vecteur caractéristique de la séquence de transitions
s = t1 t2 ... tn
tel que Vs(t) donne le nombre d'occurrences de la transition t dans s
On note :
M /s→ Mn
M. F. Karoui 18
Chapitre III
Mf = M + C . VsT
Remarque :
s = s1 . s2 => Vs = Vs1 + Vs2
Vs1 = Vs2 => M + C . Vs1T = M + C . Vs2T même si s1≠s2
M. F. Karoui 19
Chapitre III
M. F. Karoui 20
Chapitre III
<T1, T2, T3, T2>, <T3, T1, T2, T2>, <T3, T2, T2, T1>, <T1, T3, T2, T2>,
<T1, T2, T2, T3>, …
M. F. Karoui 21
Chapitre III
M. F. Karoui 22
Chapitre III
Pb Pb Pb
L'équation d'état appliquée à une séquence réduite à une transition fournit le nombre de
jetons qui restent après « exécution » de cette transition.
=> Si ce nombre est négatif, alors la transition n'est pas franchissable.
M. F. Karoui
(Attention : réciproque fausse) 23
Chapitre III
M0 = Mf - C . VsT P1
P2
Eq. Eq. Eq.
M0 M1 M2 Mf
Etat Etat Etat 2
T1
Pb Pb Pb
P3
P4
– Exemple :
Quel marquage initial pour le marquage final T2
2
Mf= [2, 5, 1, 4, 0] et la séquence <T1, T2, T2> P5
M. F. Karoui 24
Chapitre III
x 2 0 -1 3
P3
y 5 -2 0 5
0 P4
M2 = z = 1 - 1 -1
1 => M2= 2
t 4 0 -1 5
u 0 0 2 -2
T2
2
P5
M. F. Karoui 25
Chapitre III
T1
P3
P4
T2
2
P5
M. F. Karoui 26
Chapitre III
=> calcul de M0
4 0 -1 4 T2
-2 0 7 2
5 1 P5
M0 = 3 - 1 -1 = 2
0
6 0 -1 6
1 0 2 1
M. F. Karoui 27
Chapitre III
M0 + C . VsT > 0
Pb Pb Pb
M. F. Karoui 28
Chapitre III
2
T1
P3
P4
T2
2
P5
M. F. Karoui 29
Chapitre III
Validation
M. F. Karoui 31
Chapitre III
M. F. Karoui 32
Chapitre III
M. F. Karoui 33
Chapitre III
Validation
Exemple : Marquage accessible et graphe de marquage
M. F. Karoui 34
Chapitre III
M. F. Karoui 35
Chapitre III
M. F. Karoui 36
Chapitre III
M. F. Karoui 37
Chapitre III
M. F. Karoui 38
Chapitre III
P0
T0
P1
T1
M. F. Karoui 39
Chapitre III
M. F. Karoui 40
Chapitre III
M. F. Karoui 41
Chapitre III
M. F. Karoui 42
Chapitre III
Ta
P3
P2
Tb Tc
P5
P4
Te Td
M. F. Karoui 43
Chapitre III
Graphe de couverture
M. F. Karoui 44
Chapitre III
Graphe de couverture
• Algorithme de construction du graphe de
couverture(GC) :
– début : idem que GM
– À chaque nouveau marquage trouvé, on vérifie qu'il
n'est pas supérieur à l'un des marquages existant.
– si c'est le cas, on transforme ce marquage en
remplaçant le marquage des places non bornées par ∞.
– on ne cherchera pas les successeurs de ces marquages.
– etc.
• Le graphe de couverture remplace le graphe de
marquage pour les RdP non bornés.
M. F. Karoui 45
Chapitre III
Graphe de couverture
Graphe de couverture ?
M. F. Karoui 46
Chapitre III
Graphe de couverture
M. F. Karoui 47
Chapitre III
Graphe de couverture
P1
Ta
Graphe de couverture ?
P3
P2
Tb Tc
P5
P4
Te Td
M. F. Karoui 48
Chapitre III
Graphe de couverture
P1
Ta
P3
P2
Tb Tc
P5
P4
Te Td
M. F. Karoui 49
Chapitre III
Vérification de propriétés
Pour un marquage initial donné:
• réseau borné: toutes ses places sont bornées
• place bornée: nombre de jetons toujous inférieur à une borne k.
∀M, ∀p : M(p) ≤k
• réseau sauf (binaire) : k=1.
• Exemple : modélisation d'un stock à capacité limitée.
• Exemple réseau sauf : modélisation d'un fonctionnement de
type automatisme logique (MEF).
M. F. Karoui 52
Chapitre III
Vérification de propriétés
• Exemple de réseaux borné et sauf
M. F. Karoui 53
Chapitre III
Vérification de propriétés
• Réseau vivant: chacune de ses transitions est vivante.
• Transition Ti vivante: pour tout marquage M, il existe une séquence de
franchissement (transitions) qui permettra de franchir Ti.
séquence de franchissement
permettant le tir de Ta à
partir de M3
M. F. Karoui 54
Chapitre III
Vérification de propriétés
M. F. Karoui 55
Chapitre III
Vérification de propriétés
Vérification de propriétés
• Une transition Tj est quasi-vivante si il existe au moins une
séquence de franchissement contenant Tj à partir de M0
Ex : dans l'exemple précédent, T3 est quasi-vivante.
• Un blocage (deadlock) est un marquage à partir duquel plus
aucune transition n'est tirable
• Remarque :
– Vivant ⊂ Quasi vivant
– Blocage⊂ Non vivant
M. F. Karoui 57
Chapitre III
Vérification de propriétés
• Réseau réinitialisable ou propre: pour chaque marquage, il
existe une séquence de franchissement permettant de revenir
dans l'état initial
M. F. Karoui 58
Chapitre III
Vérification de propriétés
• Exemple de réseau non réinitialisable:
M. F. Karoui 59
Chapitre III
Vérification de propriétés
• "Un système déterministe est un système dans lequel chaque
état n'a qu'un seul successeur possible".
• Application aux RdP: un RdP est déterministe s'il n'existe pas
de conflit effectif.
• Conflit structurel: le jeton d'une place est partagé entre deux
transitions. (indépendant du marquage)
M. F. Karoui 60
Chapitre III
Exercice: producteur/consommateur
Quand sa "production" est finie (production d'une seule pièce à la
fois), un producteur dépose la pièce produite dans un stock, s'il
y a de la place libre dans ce stock dont la capacité est de 3
unités. Dès qu'il a pu faire le dépôt, il commence à produire
une autre pièce. Un consommateur, dès qu'il a fini de
"consommer" (une seule pièce à la fois), prélève une pièce
dans le stock s'il n'est pas vide.
Représenter le fonctionnement de ce système par un RdP avec un
marquage initial correspondant à la figure.
Quels sont les invariants de marquage de ce système, et quelles
sont leurs significations ?
M. F. Karoui 61
Chapitre III
Correction: producteur/consommateur
M. F. Karoui 62
Chapitre III
M. F. Karoui 63
Chapitre III
Correction:
Gestion de cabine
M. F. Karoui 64
Chapitre III
Correction:
Gestion de cabine
M. F. Karoui 65
Chapitre III
Boule A Boule B
M. F. Karoui 66
Chapitre III
M. F. Karoui 67
Chapitre III
Analyse structurelle
M. F. Karoui 68
Chapitre III
Composantes répétitives
M. F. Karoui 69
Chapitre III
Composantes répétitives
2 invariants de transitions:
• 1er invariant :
• CommandeX
• Xfabriqué
• Xvendu
• 2ème invariant :
• CommandeY
• Yfabriqué
• Yvendu
• Toutes les transitions
appartiennent à un invariant.
⇒ Le réseau est vivant !
M. F. Karoui 70
Chapitre III
M. F. Karoui 71
Chapitre III
• S={T0,T1}
• Vs=[1 1]
• C. VsT>0
• S est une
composante non
stationnaire
• Le RDP est non
borné
M. F. Karoui 72
Chapitre III
Composantes conservatives
VpT.C =0
M. F. Karoui 73
Chapitre III
Composantes conservatives
1 invariant de places:
• Attente
• FabricationX
• FabricationY
• XAVendre
• YAVendre
Toutes les places sont couvertes
par des p-invariants.
⇒Le réseau est borné
M. F. Karoui 74
Chapitre III
Composantes conservatives
Exemples d'interprétations:
• Si une composante conservative est telle que K0 = 0 :
– aucune de ces places n’est marquée dans M0.
– elles restent vides quelque soit le marquage.
⇒C'est anormal
• Si une composante conservative est telle que K0 = 1 :
– il y a toujours une de ces places marquées d’un jeton, et pas plus
d'un jeton.
⇒L'interprétation de ces places doit donc être booléenne
• Si un RdP est tel que toutes ses places appartiennent à des
invariants de place de constantes = 1, il est sauf !
⇒L'interprétation du réseau doit donc être complètement
booléenne
M. F. Karoui 75
Chapitre III
Composantes conservatives
Exemple P1 -1 1 0 0
P2 1 -1 0 0
P1 P3 P= P3 C= 0 0 -1 1
P4 0 0 1 -1
P5 -1 1 -1 1
P2 P5 P4
f1 f2
M. F. Karoui 76
Chapitre III
Composantes conservatives
VpT.C =0 VpT.C => M2 – M1 – M5 = 0
M1 – M2 + M5 = 0
VpT = (M1, M2, M3, M4, M5)
M4 – M3 – M5 = 0
M3 – M4 + M5 =0
-1 1 0 0
VpT = (M1, M2, M3, M4, M5)
1 -1 0 0
C= 0 0 -1 1 (1 , 1 , 0 , 0 , 0 )
0 0 1 -1 (0 , 1 , 0 , 0 , 1 )
-1 1 -1 1 (0 , 0 , 1 , 1 , 0 )
(0 , 0 , 0 , 1 , 1 )
(0 , 1 , 0 , 1 , 1 )
M. F. Karoui 77
Chapitre III
Composantes conservatives
P1 P3
-1 1 0 0
1
1 -1 0 0
M0= 0
d1 d2 C= 0 0 -1 1
1
P2 P5 P4 0 0 1 -1
0
-1 1 -1 1
f1 f2 1
1 (P1 0 0
1 + P2) 0 1 (P2
V1= 0 V2= 1 (P3 V3= 0 Il est toujours
0 1 + P4) 1 + P4 possible de
+ P5) trouver
0 0 1
d’autres
•V1’.M0=1 et V1’.C= 0 =>V1’.Mi=1 => Mi(P1)+Mi(P2)=1 invariant s en
additionnant
•V2’.M0=1 et V2’.C= 0 =>V2’.Mi=1 => Mi(P3)+Mi(P4)=1 les invariants
•V3’.M0=1 et V3’.C= 0 =>V3’.Mi=1 => Mi(P2)+Mi(P4)+Mi(P5)=1 minimaux
M. F. Karoui 78
Chapitre III
Composantes conservatives
P3
c2
P1
P4
c1
P6 f2
P2
P5
f1
t2
P7
M. F. Karoui 79
Chapitre III
Composantes conservatives
P3
c2 P’ = {P1, P2 } ⇒ m1 + m2 = 1
P1
P4 P’’ = {P3, P4, P5} ⇒ m3 + m4 + m5 = 1
c1
P6 f2 P ’’’ = {P6, P7} ⇒ m6 + m7 = 1
P2
P5
f1
t2
P7
• Les ensembles P’, P’’, P ’’’, sont des composantes conservatives. A partir de cet
ensemble de relations, nous pouvons construite l’invariant suivant: m1 + m2 + m3+
m4 + m5+ m6 + m7 = 3
• Dans cet invariant nous pouvons trouver toutes les places du RdP
• RDP conservatif
M. F. Karoui 80
Chapitre III
Analyse Globale
•RDP A non bloqué
•RDP B non bloqué
•RDP A et RDP B bloqués
M. F. Karoui 81
Chapitre III
M. F. Karoui 82
Chapitre III
Transformation de Boussin: R1
M. F. Karoui 83
Chapitre III
Transformation de Boussin: R2
M. F. Karoui 84
Chapitre III
Transformation de Boussin: R3
M. F. Karoui 85
Chapitre III
Transformation de Boussin: R4
M. F. Karoui 86
Chapitre III
Transformation de Boussin: R5
M. F. Karoui 87
Chapitre III
Transformation de Boussin: R6
M. F. Karoui 88
Chapitre III
Transformations simples
Notion de résidu :
• RESIDU = RdP sur lequel on ne peut plus appliquer de
transformation.
• Il n’est pas unique. Il dépend de l’ordre des transformations.
M. F. Karoui 89
Chapitre III
Transformations simples
M. F. Karoui 90
Chapitre III
Exercice
Après Réduction
M. F. Karoui 91
Chapitre III
Exercice
Après Réduction
M. F. Karoui 92
Chapitre III
Exercice
Après Réduction
M. F. Karoui 93
Chapitre III
Exercice
Après Réduction
M. F. Karoui 94
Chapitre III
Exercice
Après Réduction
M. F. Karoui 95