Home

Manuel d`utilisation

1. d acc s au fichier cont txt Figure 9 Format d un fichier esa txt Note suivant l emplacement choisi pour l enregistrement du projet les chemins d acc s enregistr s seront soit absolus exemple c projet fichier struct txt soit relatifs exemple fichier struct txt e Un chemin sera relatif lorsque le fichier r f rencer se trouve dans le m me P r pertoire que le fichier esa txt du projet ou dans l un de ses sous r pertoires e Sice n est pas le cas le chemin sera absolu De cette mani re le r pertoire entier contenant le fichier esa txt du projet peut tre d plac tout en conservant des r f rences valides Par contre si les fichiers qui sont r f renc s de mani re absolue sont d plac s le lien sera rompu FICHIER ESA TXT GRAPH Le deuxi me fichier tre enregistr lors de la sauvegarde d un projet est le fichier esa txt graph Il contient s ils existent les graphes de pr c dence affich s ainsi que les ventuels commentaires associ s ces graphes Remarque contrairement tous les autres fichiers celui ci n est pas lisible par un diteur de texte 2 10 LES MESSAGES D ERREURS Le tableau si dessous donne la liste de tous les messages d erreurs qui peuvent appara tre dans la barre d tat de la fen tre principale de ESA PetriNet Chaque erreur y est expliqu e et certaines actions pour pallier ces erreurs sont fournies Explication Action Soluti
2. de m thodes ont t d finis vous devez reservoir O0 cliquer sur Enregistrer choisir le r pertoire du projet et nommer le R Ev1 ndr fichier cr er res com txt dans notre cas Apr s avoir enregistr le E Ev struct tt fichier l diteur de fichier de communications se ferme et le champ de R EVS nr E EVS struct txt l interface relatif au fichier com txt se compl te automatiquement amp res nat Ci dessous la figure 15 pr sente le contenu du fichier res com txt El res struct tt Z res com txt trappes O0 Fichier Communications version 1 0 res T11 EV1 t11 r s TI4 EVS t14 res T15 EVS t15 Figure 15 Fichier res com txt 3 7 GENERER LES SCENARIOS Arriv cette tape vous allez demander ESA PetriNet de g n rer les sc narios Par d faut comme les options n ont pas t chang es les sc narios g n r s seront les sc narios redout s minimaux uniquement Pour cela vous devez cliquer sur le bouton G n rer les sc narios Comme aucun fichier de r sultat n a t sp cifi un fichier par d faut est cr automatiquement esa result txt Ensuite cliquez sur Graphe de Pr c dence pour afficher les sc narios contenus dans ce fichier de r sultat esa result txt sous la forme de graphes de pr c dence voir figure 16 ESA Petribet Fichier Options Aide alol al Fichier s 5truct 4 E exemples RdPireservoir OO EY1 structtxt 2 E exemples
3. r pertoire que ex cutable de ESA PetriNet 2 V rifier que le r pertoire o ce trouve l ex cutable de ESA PetriNet soit autoris en criture 1 V rifier que le fichier ndr et le fichier struct txt se trouvent dans le m me r pertoire 2 Red finir ex cutable de TINA l aide du menu le chemin d acc s Option voir section 2 2 Red finir le chemin d acc s ex cutable de TINA l aide du menu Option voir section 2 2 Si toute fois vous souhait utilis 2 fois le m me objet RdP dans votre mod le copier le fichier struct txt vers un autre nom de fichier et ajouter ce nouveau fichier la liste 1 Recommencer la sauvegarde du projet 2 Si l action pr c dente ne r sout pas le probl me r g n rer les graphes de pr c dence avant de tenter une nouvelle sauvegarde du projet 1 V rifier qu aucun projet de m me nom n existe dans le r pertoire choisi 2 V rifier autoris en criture sinon choisir un que le r pertoire est autre r pertoire 1 V rifier que le fichier s lectionn est bien celui du projet 2 Si l erreur persiste diter le fichier du projet et v rifier son contenu ou recommencer le projet et faite une nouvelle sauvegarde V rifier que le fichier du projet est accessible en lecture 3 LES ETAPES DE L UTILISATION SUR UN EXEMPLE spil PRESENTATION DE L EXEMPLE Dans cette partie du manuel un tutorial illustre la d marche suivre p
4. tails de mod lisation de ce syst me sont expliqu s dans la th se de S Khalfaoui soutenue le 26 septembre 2003 rapport LAAS n 03574 Electrovanne 1 R servoir Electrovanne de secours Figure 11 Mod le RdP orient objets du syst me de r gulation d un r servoir 32 EDITER LES RDP AVEC TINA La premi re tape consiste reproduire les 3 RdP bien format s ci dessus sous TINA dans des fichiers s par s Ainsi vous obtiendrez trois fichiers ndr comme le montre la figure 12 Fichier EV1 ndr Fichier res ndr Fichier EV3 ndr Figure 12 Les 3 fichiers ndr 3 3 ENREGISTRER LES FICHIERS NDR j exemples rdp Pour un suivi ais et une sauvegarde claire du projet il est conseill de Cas d tude cr er un dossier sp cifique pour chaque projet Ici il s agit de reservoir OO a D reservoir 06 Les diff rents fichiers ndr du projet sont alors enregistr dans ce DM ndr r pertoire Pour un projet important il peut tre int ressant de regrouper E EWS ngr m tes ndr trappes GG les fichiers ndr dans des sous r pertoires des packages afin d organiser l ensemble des objets utilis s Par exemple nous aurions pu cr er un sous r pertoire electrovanne qui contiendrait EV1 ndr et EVS ndr 3 4 GENERER LES FICHIERS STRUCT TXT Ensuite toujours sous l outil TINA il s agit d effectuer une analyse fn exemples rdp structurelle pour chaque objet RdP et de sauvegarder
5. 1 nomObj2 nomEvt2 nomPlace s par s par des espaces o nomPlace repr sente l atome cr par nomObj1 nomEvt1 et consomm par nomObj2 nomEvt2 B et C sont des listes de nomObj1 nomEvt1 nomObj2 nomEvt2 s par s par des espaces Le est une liste de nomObj e nomPlace s par s par des espaces o nomPlace correspond l atome cr par l v nement d enrichissement e dans le RdP de l objet nomObj Note si aucun fichier result txt n est renseign travers l interface lorsque la recherche des sc narios est lanc e un fichier result txt est automatiquement cr dans le m me r pertoire que le premier fichier de la liste des fichiers struct txt et le champ de l interface correspondant est automatiquement compl t 21 FICHIER CONTRAINTES L utilisation des fichiers de contraintes n a pas t impl ment e dans la version 1 0 de ESA PetriNet Il s agirait de v rifier des propri t s temporelles sur l ensemble des sc narios g n r s ce qui signifie que l extraction des sc narios devrait se faire avant cette v rification et que par cons quent cette v rification n est pas utile pour la g n ration des sc narios redout s 2 8 ZONE DES GRAPHES DE PRECEDENCES Les graphes de pr c dences s affichent dans la zone 4 de la figure 1 section 2 1 apr s avoir cliqu sur le bouton Graphe de Pr c dence et ceci d apr s le fichier result txt renseign dans l interface Il est possible d ajouter des c
6. 5 o la transition tO de l objet 1 appelle les deux transitions nomm es t1 des objets 2 et 3 et la transition t2 de l objet3 appelle la transition t4 de lobjet4 ESA PetriNet wersion 1 0 Fichier Communications objet1 to s objetaftl objet3 t1 objet3 t2 objetd td Figure 5 Structure d un fichier de communication com txt On constate qu il est possible que 2 transitions de 2 objets diff rents aient le m me nom m me si cela n est pas recommand afin d viter des confusions Note il n est pas possible de d finir une transition qui appelle une ou des transitions et en m me temps est appel e par une ou des transitions 2 5 EDITEUR DE FICHIER DE COMMUNICATION Le fichier de communication peut tre cr l aide de l diteur de fichier Com fourni avec ESA PetriNet voir figure 6 en cliquant sur le bouton une fois que la liste des fichiers de structure des RdP qui interviennent dans le mod le a t renseign e j ESA _FPetriHet Edition de fichier Com communication entre objets omObjetHomTransition Transitions appelantes gt Transitions appel es par une appelante i 3 Figure 6 Editeur de fichier de communication Toutes les transitions du mod le apparaissent gauche dans l diteur zone 1 Le fonctionnement de l diteur est alors le suivant e La premi re tape consiste d finir les transitions appelantes c est dire celles qui appellent une
7. CHIER DE STRUCTURE La figure 4 donne le fichier de structure du RdP bien format de la figure 3 pongo rquiller Windows Bureau cas Etiquette Nom de transition Poids de l arc Figure 3 Exemple de RdP bien format struct version 2 8 4 1027706 LAAS CHRS parsed net cas_etude 4 places 3 transitions net cas_etude def Rs_ok gt R5_ko a red 3 w N gt E red t1 0 3 N RS Ok gt N Rs_ok E red 0 0 li M o N 1 Rs ko JI 0 Rs_ok N 1 inwariant Rs_ko R5_0k 2 E red N 0 000s T SEMI FLOWES GENERATING SET not consistent t1 0 000s ANALYSIS COMPLETED Figure 4 Exemple de fichier de structure Il est a not que seul les parties encadr es sur la figure 4 sont utilis es par ESA PetriNet le reste peut ventuellement tre supprim Attention vitez de nommer des transitions par il i2 el e2 ou f1 f2 car ces notations sont utilis es respectivement pour les v nements d dinitialisation les v nements d enrichissement et les v nements finaux 2 4 FICHIER DE COMMUNICATION Le fichier de communication est utile pour une mod lisation orient e objets c est dire lorsque plusieurs RdP interviennent Mais il est parfaitement possible de n utiliser qu un seul RdP pour la mod lisation dans ce cas aucun fichier de communication ne doit tre d fini La structure de ce fichier est donn e en figure
8. NA s ouvre avec un fichier vierge Si un fichier de structure 7 R seau de Petri d un RdP est s lectionn et si son fichier ndr se trouve dans le m me r pertoire que ce fichier struct txt TINA ouvrira directement le RdP s lectionn Des modifications peuvent alors tre faites sur le RdP mais il ne faudra pas oublier de proc der une nouvelle analyse structurelle du r seau pour obtenir le fichier de structure du RdP jour voir la section 2 3 pour plus de d tails concernant les fichiers de structure d un RdP 2 2 BARRE DE MENU La barre de menu contient 3 sous menus Fichier Options et Aide voir figure 2 Fichier Aide OUruTIr O tous les sc narios propos Enregistrer sc narios redout s non minimaux Options Imprimer sc narios redout s minimaux Figure 2 Barre de menu Le sous menu Fichier propose des commandes classiques tel que cr er un nouveau projet ouvrir un projet existant enregistrer le projet courant imprimer la page seul les graphes de pr c dences s impriment et quitter le logiciel Le sous menu Options permet de sp cifier l adresse de TINA c est dire le chemin de l ex cutable nd exe sous Windows sans quoi il serait impossible d appeler l outil TINA depuis ESA PetriNet par l interm diaire du bouton pr vu cet effet voir la section 2 1 Ce m me sous menu permet aussi de choisir entre la g n ration de tous les sc narios des sc nar
9. Notice v 1 0 F vrier 2008 Guide d utilisation de ESA PetriNet Temporal Edition Version 1 0 2007 Copyright LAAS CNRS Groupe ISI TABLE DES MATIERES LRO Onein i a a E S E E A ea 1 1 1 Description rapide QU IOBICIBl 222 5 sidi nent sccsendnees caen iieii 1 1 2 CON HPUEATION F QUISR a a ee ne ed Eee 1 1 3 Description de la finalit du manuel sise 1 2 Presenta ON EENI nE EA A ETA 2 2 1 RSS RERO A E E A E E T A 2 2 2 Barre de OU De D hs 3 2 3 Fichier de structure d un RdP nn ans srnessenocsans sens dasss se ncs amie srmes monte 3 2 4 Fichier de COMENUDICAEION a ae ae ds bone id 5 2 5 Editeur de fichier de communication LL 6 2 6 PCR RSS RSR ec 7 2 7 Fichier COPINE dt dec te don nn net en recto et duree 8 2 8 Zone des graphes de pr c dences 2 rates st nencnnenebe seen nec nn eseuetot recoit hiene 8 2 9 CSS E E 9 210 L NES RES d ee N E 10 3 Les tapes de l utilisation sur un exemple ss 11 3 1 Pr sentation de l exemple iii nerss sense ssnnnsssnnsscennsssenssse 11 2 Editer les RdP avec TINA sssessssesereeessssssssssesrreesssssssseesererosssessseerereroessssssereeeeeossssssseeeereresee 12 3 3 Enregistrer les tieni inde cn nant crane ane es le et ee Du 13 3 4 G n rer les fichiers strUct DT 02e rssssserneliterotenssenenrreeerereseesiteess the node en 13 3 5 COmPE Er er E e E E E E N 13 3 6 Ceerle TIC E CON OR a E Ea 14 3 7 Genereer ICS SCOOTER a nt ce 15 3 8 Commenter les Scen
10. RdP reservoir OCEYS structtat 3 E exemples RdP reserwoir OOres struct txt Fichier Com E jexemples RdPireservoir G ires com tt Fichier Resultat 1 Eexemples RdPireservoir OOesa result tt 4 Fichier Contraintes Le ELELELELELELELELELELELEE D E Sc nario 1 redout ES der EES f3 LT t a a Le ue A 1 AAC 113 E red fl Elaboration des graphes termin Figure 16 Graphe de pr c dence g n r 3 8 COMMENTER LES SCENARIOS Une fois les sc narios g n r s et affich s il est possible de commenter chaque sc nario dans une zone gris e gauche de chaque graphe Par exemple dans notre cas nous pouvons ajouter le commentaire d faillance de l EV1 et d faillance de l EVS voir figure 17 Sc nario 1 redoute Ewi d faillance de l E e del 13 et d faillance de l EYS Elaboration des graphes termin Figure 17 Graphe de pr c dence comment 29 SAUVEGARDER LE PROJET a 0 exemples rdp Dans une derni re tape nous allons sauvegarder le projet De Cas d tude 2 reservoir GO REV 4 nd EY1 struct txt ES nr E EVS struct txt Pon E res a 2 nouveaux fichiers se sont alors cr s dans le r pertoire du mani re tr s intuitive vous trouverez dans le menu Fichier la commande Enregistrer Cliquez sur cette commande puis s lectionnez le r pertoire du projet reservoir OO et nomm le projet par exemple par reservoir OO esa tx
11. arios isisssissisissiisririrsriisinurainiseriinkins isinsi nandi kia siana rene Eini eet one 16 3 9 Sauvecarder le projet a ee dites N 16 1 INTRODUCTION LT DESCRIPTION RAPIDE DU LOGICIEL ESA PetriNet est un logiciel d velopp par le groupe ISI du LAAS CNRS Il permet de g n rer les ensembles d v nements qui conduisent un syst me dans un tat particulier pr d fini Ces ensembles d v nements forment des sc narios qui dans le cas o l tat particulier repr sente un tat de d faillance du syst me sont appel s sc narios redout s Par construction de son algorithme ESA PetriNet fournit tous les sc narios strictement n cessaire et suffisant pour atteindre l tat sp cifi notions de compl tude et de minimalit Pour fonctionner le logiciel a besoin d une mod lisation faite soit d un unique r seau de Petri soit de plusieurs r seaux de Petri li s entre eux par des appels m thodes comme le permet l aspect orient objets 102 CONFIGURATION REQUISE ESA PetriNet est crit en langage Java c est pourquoi il n cessite une machine virtuelle Java pour s ex cuter La JDK install e doit tre la JDK version 6 ou une version sup rieure puisque la g n ricit et certaines structures de donn es dynamiques ou non contraintes tel que arraylist lt E gt ou hashmap lt K E gt sont n cessaires Les r seaux de Petri peuvent tre con us l aide de l outil TINA d velopp par le g
12. ent Kit Time petri Net Analyzer Outils Logiciels pour la Communication 2 PRESENTATION GENERALE 2 1 INTERFACE PRINCIPAL L interface principal de ESA PetriNet voir figure 1 est compos e d une barre de menu assez classique suivie par une barre d outil zone 1 d un r capitulatif des fichiers du mod le zone 2 auquel est adjoint une s rie de boutons permettant la gestion de ces fichiers droite de la zone 2 d un ensemble de boutons principaux permettant de g n rer les sc narios ou les graphes de pr c dence zone 3 d un cadre principal r serv l affichage de ces graphes de pr c dence zone 4 et enfin d une barre d tat indiquant certaines actions r alis es ou des messages d erreurs zone 5 voir la section 2 9 de ce manuel pour les explications des diff rents messages d erreurs possibles L ESA Petribet Fichier Options Aide Fichier s Struct Fichier Com Fichier Resultat Fichier Contraintes Figure 1 Interface principal de ESA PetriNet Le bouton en forme de loupe situ dans la zone 2 ouvre un diteur de fichiers de communications qui permet aussi bien de cr er un nouveau fichier que de modifier un fichier existant voir la section 2 4 pour plus de d tails propos des fichiers de communications et de leur diteur L outil TINA peut tre appel l aide du bouton rouge 74 droite de la zone 2 Si aucun fichier de structure d un RdP n est s lectionn TI
13. ios redout s non minimaux seulement ou des sc narios redout s minimaux uniquement Le troisi me et dernier sous menu est celui intitul Aide Comme son nom l indique il propose d ouvrir l aide de l outil mais permet aussi d afficher une fen tre propos about en anglais 2 3 FICHIER DE STRUCTURE D UN RDP Les fichiers repr sentatifs des RdP utilis s par ESA PetriNet sont les fichiers struct txt g n r s par le module d analyse structurelle de l outil TINA car ceux ci contiennent en plus des informations structurelles telles que les invariants de marquages la structure du RdP sous forme textuelle Ainsi les fichiers ndr d dition graphique ne sont pas utilis s par ESA PetriNet La pr sence de ces fichiers ndr n est donc pas obligatoire mais plac s dans le m me r pertoire que leurs fichiers struct txt elle permet leurs ouvertures directes dans TINA depuis ESA PetriNet voir section 2 1 LE FORMAT DES ETIQUETTES ASSOCIEES AUX PLACES Avant d effectuer l analyse structurelle du RdP il faut bien formater les tiquettes label associ es chaque place du RdP En effet celles ci sont utilis es pour d finir le type de place et le marquage initial du RdP global dans les conditions de fonctionnement normal attention il ne s agit pas ici du marquage utilis pour d buter le raisonnement arri re Les diff rents types de places possibles sont les suivants e _ N places de fonctionnement no
14. ommentaires aux graphes de pr c dence dans des cadres pr sents gauche de chaque graphe comme le montre la figure 8 Sc nario 1 redout EVS D faillance EY1 ei EW EL defi EW RE f3 et o d faillance EYS e trappe1 gn a 5 gt t 5 gt rea lt r f EV1 F4 12 se der S fa D x Figure 8 Exemple de graphe de pr c dence comment Comme l illustre le graphe ci dessus les v nements sont regroup s par objet dans des rectangles d pla ables en blocs Les fl ches noires forment les liens directs les bleues en pointill s repr sentent les liens indirects et les grises montrent les appels de m thodes entre objets Les atomes appartenant l tat redout et leurs liens entre v nements sont en rouge 2 9 FICHIERS PROJET Un projet peut tre sauvegard tout moment et son enregistrement est compos de 2 fichiers FICHIER ESA TXT Le premier est le fichier esa txt I contient toutes les donn es renseign es dans les diff rents champs de l interface fichier s struct txt fichier com txt et ou fichier result txt Sa structure dans sa forme la plus volu e est donn e en figure 9 ESA PetriNet version 1 0 net et inv chemin d acc s au 1 fichier struct txt net et inv chemin d acc s au 2 fichier struct txt lasad net et inv chemin d acc saun me fichier struct txt com chemin d acc s au fichier com txt chemin d acc s au fichier res txt cont chemin
15. on Impossible de sauvegarder l adresse de Tina Impossible de trouver Tina ou le fichier ndr Impossible de trouver Tina Impossible d ajouter 2 fois le m me fichier Impossible de s rialiser les graphes Impossible de sauvegarder le fichier dans le r pertoire s lectionn Fichier non reconnu Impossible de charger le fichier esa txt l crire du fichier qui doit stoker le chemin d acc s l ex cutable de TINA n est pas possible Lorsqu un fichier struct txt est s lectionn et que l on cherche ouvrir TINA depuis ESA PetriNet ce message appara t si l ex cutable de TINA ou du fichier struct txt ne sont pas trouv s le fichier ndr Lorsque aucun fichier struct txt n est s lectionn et que l on cherche ouvrir TINA depuis ESA PetriNet ce message appara t si l ex cutable de TINA n est pas trouv Il n est pas possible d ajouter 2 fois le m me fichier struct txt la liste des fichiers d finissant les objets RdP Une erreur c est produite lors de de pr c dence du projet sauvegarder l enregistrement des graphes La sauvegarde du projet ne peut pas tre r alis e dans le r pertoire choisi Lors du chargement du projet le logiciel ne reconnait pas un fichier projet ESA PetriNet version 1 0 Il est impossible de lire le projet s lectionn 1 V rifier qu il n y ait pas un fichier nomm adresseTina txt interdit en criture dans le m me
16. ou plusieurs autres transitions Pour ce faire il suffit de s lectionner la transition dans la liste de gauche zone 1 et de l ajouter dans la liste des transitions appelantes zone 2 en cliquant sur le bouton gt gt gauche de la zone 2 e La deuxi me tape consiste d finir les transitions appel es pour chaque transition appelante Le principe est de s lectionner la transition appelante consid r e zone 2 puis de s lectionner la transition appeler dans la zone 1 et enfin d ajouter cette derni re transition la liste des transitions appel es de la transition appelante consid r e dans la zone 3 en cliquant sur le bouton gt gt Les 2 boutons X gauche de la zone 2 et gauche de la zone 3 permettent respectivement de supprimer la transition appelante s lectionn e ou la transition appel e s lectionn e 2 6 FICHIER RESULTAT Obtenu apr s la recherche de sc narios le fichier result txt contient justement les sc narios g n r s Il sert ensuite comme donn e d entr e la construction et l affichage des graphes de pr c dence forme beaucoup plus commode et lisible que l criture textuelle des sc narios pr sente dans le fichier result txt dont le format est le suivant ESA PetriNet version 1 0 Fichier R sultats RED places appartenant l tat redout Sc nario 1 redout E i instances de tir de transitions internes ou appelantes et venements i e etf E2 ins
17. our utiliser ESA PetriNet L exemple trait se base sur une mod lisation orient e objets d un syst me de r gulation du volume d un r servoir Le syst me est constitu d un calculateur d une pompe de deux lectrovannes d un capteur de volume d un r servoir r gul et d un r servoir de vidange voir figure 10 Le r servoir r gul alimente des utilisateurs et le but du calculateur est de maintenir le volume entre deux valeurs pr d finies Vmin et Vmax Pour ce faire le calculateur dispose de l information fournie par le capteur et commande l lectrovanne principale EV1 Si cette derni re tombe en panne le calculateur peut encore agir sur le volume de liquide dans le r servoir par l interm diaire de l lectrovanne de secours EVS tant que celle ci reste op rationnelle Pompe EV1 EvS R servoir de vidange Figure 10 Syst me de r gulation d un r servoir Les diff rents r seaux de Petri utilis s pour mod lise ce syst me sont donn s en figure 11 o pour simplifier seul trois objets sont consid r s le r servoir principal EV1 et EVS Sur cette figure les r seaux de Petri sont format s pour ESA PetriNet et la pr sence d un jeton dans la place E red1 indique le choix de l tat redout analyser il correspond au d bordement du r servoir Les communications entre objets sont aussi notifi es sur le sch ma travers 3 appels m thode Remarque les d
18. rmal e D places appartenant l tat partiel redout analyser e IR places appartenant un tat d faillant r parable mais non l tat redout e I places appartenant un tat d faillent non r parable mais non l tat redout Le format utilis pour les tiquettes des places est alors Identificateur_ type de _place nombre de jetons dans _ la_place Exemples N 1 D 0 IR 0 L 0 LES INTERVALLES DE TIR DES TRANSITIONS Il faut aussi d finir les intervalles de tir des transitions avant de proc der l analyse structurelle pour que ces informations soient contenues dans les fichiers r sultant de cette analyse Dans cette premi re version d ESA PetriNet seuls les intervalles du type a ou a b sont accept s sachant qu un intervalle non sp cifi est autoris puisqu il signifie 0 ce qui est compris dans a Ainsi il n est pas possible d utiliser les formes Ja b Ja b ou a bl LE MARQUAGE INITIAL Le v ritable marquage initial du ou des RdP c est dire celui qui est effectivement repr sent par la pr sence de jetons dans certaines places et non travers l information fournie par les tiquettes des places qui indiquent le marquage initial du RdP global dans les conditions de fonctionnement normal voir quelques lignes plus haut correspond l tat partiel redout analyser LE FI
19. roupe OLC du LAAS CNRS Dans ce cas la version 2 8 4 de TINA est recommand e La compatibilit des versions ant rieurs n a pas t v rifi e il faut au moins disposer des tiquettes ou abel associ es aux places et aux transitions du r seau de Petri et la compatibilit des versions suivantes n est pas garantie 1 3 DESCRIPTION DE LA FINALITE DU MANUEL Ce manuel a t r dig pour des personnes ayant d j des connaissances concernant les r seaux de Petri et leur concept d invariant de marquage la mod lisation Orient Objets de ces r seaux de Petri et toutes les notions relatives celle de sc nario Mise part l introduction ce manuel s articule en 2 grandes parties l La premi re intitul Pr sentation G n rale fournie toute l information n cessaires l utilisateur qui souhaite tester et d couvrir par lui m me le logiciel Mais le principe tant celui de l acc s direct une section cette partie conviendra plus particuli rement aux personnes ayant d j utilis ESA PetriNet au moins une fois Il La deuxi me partie quant elle invite le lecteur suivre un tutorial d o son titre les tapes de l utilisation sur un exemple Le principe ici est donc plut t celui de la lecture continue Extraction Scenarios amp Analyzer by Petri Net model 2 Fe o i Ing nierie Syst me et Int gration Laboratoire d Analyse et d Architecture des Syst mes Java Developem
20. t E res struct txt projet reservoir OO esa txt qui contient l information des res com ixt champs de l interface et reservoir OO esa txt graph qui est E esa resuit ta l enregistrement du graphe de pr c dence affich et de son Z reservoir _O0 esa txt E reservoir _O0 esa tt graph Ca trappes GO commentaire Ainsi il est possible de rouvrir le projet par la suite ceci en cliquant sur la commande Ouvrir du menu Fichier puis en s lectionnant le fichier reservoir_OO esa txt Auteur Hamid DEMMOU Nabil SADOU et Romaric GUILLERM au LAAS CNRS 7 avenue du Colonel Roche 31077 TOULOUSE Cedex 4 FRANCE
21. tances de tir de transitions appel es liens directs liant des l ments de E et ou de E2 avec le nom des atomes liens indirects liant des l ments de E et ou de E2 liens d appels de m thodes liant des l ments de E avec des l ments de E2 Le jetons d enrichissement Sc nario 2 non redout E instances de tir de transitions internes ou appelantes et venements i e etf E2 instances de tir de transitions appel es liens directs liant des l ments de E et ou de E2 avec le nom des atomes liens indirects liant des l ments de E et ou de E2 liens d appels de m thodes liant des l ments de E avec des l ments de E2 jetons d enrichissement Figure 7 Format d un fichier result txt RED ensemble des places appartenant l tat redout est une liste de nomObj nomPlace s par s par des espaces Un sc nario peut tre redout ou non redout suivant les options s lectionn s voir section 2 2 E est une liste de nomObj nomEvt s par s par des espaces o nomEvt est e soit un nom de transition interne ou appelante augment par num roOccurence par exemple EV1 def1 1 e soit un v nement initial i1 i2 un v nement d enrichissement e1 e2 ou un v nement final f1 f2 par exemple EV1 f2 E2 est une liste de nomObj nomEvt s par s par des espaces o nomEvt est un nom de transition appel e A est une liste de nomObj1 nomEvt
22. tous les fichiers Cas d tude struct txt issus de ces analyses cot de leurs fichiers ndr respectifs a reservoir 00 REV 4 ndr Pour ce faire il faut pour chaque fichier ndr ouvert dans TINA cliquer sur E EY1 struct tt le menu tools puis s lectionner structural analysis laisser les options par E EVS nar E EY S struct tt E res ndr Z res struct txt il suffit de vouloir fermer la fen tre bouton X en haut droite B trappes 00 d faut et cliquer sur OK A l issue le contenu du texte du futur fichier struct ndr appara t dans une nouvelle fen tre Pour en faire la sauvegarde RI COMPLETER L INTERFACE Maintenant vous pouvez fermer TINA et lancer ESA PetriNet Vous devez alors renseigner les 3 fichiers struct txt dans l interface voir section 2 1 Pour cela cliquez sur le bouton en forme de dossier droite de la zone 2 et en haut dont le message est Ajouter un fichier Struct S lectionnez le fichier ajouter et cliquez sur Ouvrir pour effectivement l ajouter la liste des fichiers struct txt de l interface R p tez l op ration autant de fois qu il y a de fichiers struct txt c est dire 3 fois dans notre cas pour EV1 struct txt pour EVS struct txt et pour res struct txt voir figure 13 ESA PetriHet SI Fichier Options Aide Fichier s SHUL 1 E exemples RdPireservoir OOEV1 structtxt 2 Eexemples RdP reservoir OC EVS struct tt x 3 Erexemples RdPireservoir OOres struct t
23. xt Fichier Com A Ci fichier Resutat 2 Figure 13 Fichiers struct txt renseign s dans l interface t 3 6 CREER LE FICHIER COM TXT Une fois seulement que tous les fichiers struct txt ont t renseign s dans l interface vous pouvez ouvrir l diteur de fichier de communications en cliquant sur la loupe voir section 2 5 II s agit alors de d finir les appels m thodes que montre la figure 11 Dans un premier temps vous allez d finir les trois transitions appelantes T11 T14 et T15 en les s lectionnant une une dans la liste de gauche et en cliquant chaque fois sur le bouton gt gt de la liste des transitions appelantes Ensuite pour d finir les transitions appel es vous devez s lectionner une une les transitions appelantes par exemple T11 dans un premier temps et pour chacune des ces transitions s lectionner une une les transitions appel es par la transition appelante courante dans la liste de gauche et cliquer chaque fois sur le bouton gt gt de la liste des transitions appel es pour T11 la transition appel e ajouter il n y en a qu une est t11 voir figure 14 ESA_PetriHet Edition de fichier Com communication entre ob omObhjet NomTransition Transitions appelantes Transitions appel es par une appelante Figure 14 D finition de t11 comme transition appel e par T11 a 2 exemples rdp Cas d tude Une fois que tous les appels

Manuel d`utilisation

Contents

Download Pdf Manuals

Related Search

Related Contents