 |
TIme petri |
 |
| Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
I Courte Introduction à l'analyse structurelle
Tina offre les fonctionnalites mettant en oeuvre l' analyse structurelle
(onglet tools - structural analysis). Plusieurs options sont possibles,
vous utiliserez l'option par défaut calcul des semi-flots
de place et de transition permettant d'obtenir les invariants de place et
de transition.
Base de Données .
- P-Semi-Flows (Invariants de Place)
P-SEMI-FLOWS GENERATING SET
invariant
wait_writers writers writting
lock reading writting*5
readers reading wait_readers- Invariant (Conservatif) indique que toutes les places du réseau appartiennent à un invariant de place. Le réseau est donc stucturellement borné.
- La base est constituée de 3 invariants
-- wait_writers + writers + writting = Cste1(Mo) (ici 3)
-- lock + reading + writting*5 = Cste2(Mo) (ici 5 )
-- readers + reading + wait_readers = Cste3(Mo) (ici 6 )
- T-Semi-Flows (Invariants de transition)
T-SEMI-FLOWS GENERATING SET
consistent
arrivee_lecteurs debut_lecture fin_lecture
arrivee_ecrivains debut_ecriture fin_ecriture- Consistent (Répétitif) indique que toutes les transitions
du réseau appartiennent à un invariant de transition.
- La base est constituée de 2 invariants
-- arrivee_lecteurs debut_lecture fin_lecture
-- arrivee_ecrivains debut_ecriture fin_ecriture
Si un multi-ensemble de transitions Sigma, comportant une occurence de chacune de ces 3 transitions est tirable dans un marquage M alors on aura M[Sigma>M.
Pour le marquage initial considéré, il est facile de voir sur ce réseau que chacun de ces invariants est effectif: il existe un marquage (par exemple le marquage initial) qui permet de tirer la sequence arrivee_lecteurs.debut_lecture.fin_lecture. Idem pour le second invariant.
- Consistent (Répétitif) indique que toutes les transitions
du réseau appartiennent à un invariant de transition.
Ci-dessous quelques commentaires d'explication:
Planteur de Bananes .
- P-Semi-Flows (Invariants de Place)
P-SEMI-FLOWS GENERATING SET
not invariant
no semiflows- Not Invariant (Non Conservatif) indique qu'au moins une place du réseau n'appartient à aucun invariant de place.
- no semiflows : il n'y a aucun invariant
- T-SEMI-FLOWS GENERATING SET
Not consistent
cueille jette mange- Not Consistent (Non Répétitif) indique qu'au moins
une transition du réseau n'appartient à aucun invariant de transition.
- La base est constituée d'un invariant
-- cueille jette mange
-- Il est facile de voir que celui-ci ne peut être effectif pour le marquage initial considéré (un seul planteur dans la plantation) ; Pour cueillir, il faut être au champ et pour manger il faut être à table et l'invariant ne comporte pas la transition rentre.
- Not Consistent (Non Répétitif) indique qu'au moins
une transition du réseau n'appartient à aucun invariant de transition.
Ci-dessous quelques commentaires d'explication: