Vlastnosti, algoritmické problémy a analýza Petriho sietí

Ciele
  1. Určiť vlastnosti a vyriešiť algoritmické problémy Petriho sietí.
  2. Vypočítať a interpretovať invarianty Petriho sietí.
Úvod
    Počas tohto cvičenia preskúmame vlastnosti sietí, ktoré sa vyskytli v predchádzajúcich cvičeniach. Tiež si vyskúšame štrukturálnu analýzu Petriho sietí, kde výpočtom tzv. invariantov miest (S-invarianty) a invariantov prechodov (T-invarianty) zistíme vlastnosti siete, ktoré platia v každom jej značení.
Postup
  1. Pre sieť MuTex z projektu fssCvicenie2 vyriešte
    • problém ohraničenia,
    • deadlock problém,
    • problém živosti,
    • problém reverzibility,
    • problém domovského stavu a
    • problém pokrytia pre q1=( 1,0,0,1,1) a q2=( 8,6,0,3,1) (poradie vo vektoroch je (sem, p1In, p1Out, p2In, p2Out)).
    Obr.: Petriho sieť MuTex
    Poznámka: Využite fakt, že množina dosiahnuteľných stavov tejto siete je konečná a malá.
  2. Vypočítajte ručne invarianty siete RW_limited10 z projektu fssCvicenie3_4. Výsledky výpočtu porovnajte s výsledkami z mFDTE/PNtool2.
    Obr.: Petriho sieť RW_limited10
  3. Určite význam invariantov siete RW_limited10.
  4. Vypočítajte (ručne resp. pomocou mFDTE/PNtool2) invarianty ostatných sietí z projektu fssCvicenie3_4 a interpretujte ich.
  5. Vysvetlite, prečo pre sieť liveness nie sú výsledky výpočtu invariantov správne interpretovateľné.
Zdroje
  1. Nástroj mFDTE/PNtool2.
  2. Projekt fssCvicenie3_4 pre nástroj mFDTE/PNtool2.
  3. Projekt fssCvicenie2 pre nástroj mFDTE/PNtool2.
  4. Š.Korečko: Doplnkové učebné texty z Formálnych špecifikácií systémov.
comments powered by Disqus