Obyčajné a zovšeobecnené Petriho siete a nástroj mFDTE/PNtool2

Ciele
  1. Preskúmať základnú funkcionalitu nástroja mFDTE/PNtool2.
  2. Určiť, ako pomocou Petriho sietí modelujeme nedeterminizmus, paralalelizmus a súbežné správanie.
  3. Vyjadriť Petriho sieť v textovej podobe.
  4. Modifikovať vytvorené siete podľa požiadaviek.
Úvod
    Petriho siete (PS) sú formálna metóda, podobná konečným automatom, ktorá umožňuje ľahko pochopiteľným spôsobom popísať nedeterministické a nesekvenčné správanie. Ľahká pochopiteľnosť vyplýva z jednoduchého princípu zmeny stavu a grafickej podoby PS. Súbežné správanie je ľahko opísateľné vďaka tomu, že stav je distribuovaný do vrcholov, nazývaných miesta, a celá sieť tak môže byť budovaná ako sústava komunikujúcich konečných automatov.
    V tomto cvičení sa oboznámite s grafickou a textovou reprezentáciou obyčajných a zovšeobecnených PS a nástrojom mFDTE/PNtool2, ktorý umožňuje ich tvorbu, simuláciu a analýzu.
Postup
  1. Nainštalujte si nástroj mFDTE/PNtool2 a otvorte v ňom projekt fssCvicenie2.
    Poznámka: Podrobný postup:
    1. Rozbaľte archívy fssCvicenie2projekt.zip a PNtool2.zip na vami zvolené miesto.
    2. Spustite mFDTE/PNtool2 dvojklikom na PNtool2.jar alebo príkazom java -jar PNtool2.jar v priečinku PNtool2.
    3. Z menu File vyberte položku Open project.
    4. V dialógu Open vyberte súbor fssCvicenie2.pnproj z priečinka fssCvicenie2.
  2. V mFDTE/PNtool2 si vyskúšajte simuláciu obyčajnej Petriho siete.
    Poznámka: Podrobný postup:
    1. V strome projektu dvojkliknite na názov prvej siete (automaton).
    2. Zapnite simuláciu stlačením tlačidla On/Off.
    3. Simulujte výpočet siete klikaním na prechody so zeleným okrajom (resp. aj vnútrom) alebo použitím panelu simulácie.
    4. Vypnite simuláciu stlačením tlačidla On/Off.
  3. Modifikujte sieť automaton pomocou manipulácie s jej časťami, zmenami ich vlastností a pridávaním a odoberaním častí pomocou panela nástrojov.
  4. Simuláciou sietí nondeterminism, paralelism a MuTex zistite, ako Petriho siete modelujú nedeterminizmus, paralalelizmus a súbežné správanie.
  5. Pomocou modulov POST a PRE, dostupných z panela modulov, zobrazte tabuľky funkcií post a pre siete automaton.
  6. Zapíšte množiny pre- a post- miest, resp. prechodov, siete automaton.
    Poznámka: Pre prechod \(a1\) máme množinu pre-miest \(^{\bullet}a1 =\{q0\}\) a post-miest \( a1^{\bullet} =\{q1\}\). Pre miesto \(q0\) máme množinu pre-prechodov \(^{\bullet}q0 =\{a3\}\) a post-prechodov \(q0^{\bullet} =\{a1\}\).
  7. Zapíšte ručne tabuľky funkcií post a pre ostatných sietí projektu fssCvicenie2. Ich správnosť overte v nástroji mFDTE/PNtool2..
  8. Modifikujte sieť nondeterminism alebo paralelism tak, aby po dosiahnutí stavu finalState bolo možné prejsť do initState.
  9. Modifikujte sieť MuTex tak, aby modelovala vzájomné vylúčenie 3 procesov.
  10. Modifikujte sieť MuTex pre 3 procesy tak, aby do kritickej oblasti mohli vojsť 2 procesy naraz.
Zdroje
  1. Nástroj mFDTE/PNtool2.
  2. Projekt fssCvicenie2 pre nástroj mFDTE/PNtool2.
  3. Š.Korečko: Doplnkové učebné texty z Formálnych špecifikácií systémov.
comments powered by Disqus