Modelovanie a vlastnosti Petriho sietí

Ciele
  1. Upraviť Petriho sieť popisujúcu problém obedujúcich filozofov tak, aby branie a vrátenie vidličiek bolo nedeterministické.
  2. Z modelov jednotlivých procesov vytvoriť model výrobného procesu.
Úvod
    V tomto cvičení budeme pokračovať v práci s obyčajnými a zovšeobecnenými PS a nástrojom mFDTE/PNtool2. Budeme sa venovať modelovaniu pomocou PS a niektorým vlastnostiam PS, najmä živosti.
    Obyčajné a zovšeobecnené PS sa tiež označujú ako Place Transition nets (PT nets, PT siete).
Postup
  1. Stiahnite si a rozbaľte archív fssCvicenie3_4projekt.zip. Projekt fssCvicenie3_4 otvorte v nástroji mFDTE/PNtool2.
  2. Vyhľadajte si na internete definíciu problému obedujúcich filozofov. Pomocou simulácie zistite ako sieť diningPhils z projektu fssCvicenie3_4 vyjadruje deterministický variant tohto problému pre troch filozofov.
  3. Sieť diningPhilsND z projektu fssCvicenie3_4 upravte tak, aby branie a vrátenie vidličiek bolo nedeterministické. To znamená, že vidličky filozof berie po jednej a nie je určené, či najprv zoberie vidličku sprava alebo zľava.
    Obr.: Petriho sieť diningPhils
  4. V PNtool2 preskúmajte sieť assemblyV0. Zistite, ako modeluje 2 oddelené procesy, kde
    • prvý proces (zelená časť) je montáž na linke s jedným montážnym miestom a
    • druhý proces (červená časť) činnosť žeriavu, ktorý vie zostavený výrobok presunúť z konca montážnej linky do zásobníka (box).
    Obr.: Petriho sieť assemblyV0
    Poznámka: Význam miest a prechodov v sieti je nasledovný:
    • AtBeginL - súčasti výrobku, ktorý sa má zostaviť sú na začiatku výrobnej linky.
    • startMove1 - súčasti výrobku sa začnú presúvať zo začiatku linky na montážne miesto.
    • MovingToAs - súčasti výrobku sú v stave presúvania na montážne miesto.
    • stopMove1 - súčasti výrobku zastanú na montážnom mieste a prebieha zostavenie (montáž) výrobku.
    • Modified – výrobok je zostavený.
    • StartMove2 – začína pohyb zostaveného výrobku na koniec montážnej linky.
    • MovingToEnd – výrobok je v stave presúvania na koniec linky.
    • stopMove2 – výrobok zastal na konci linky.
    • AtEndL – výrobok čaká na konci linky na odstránenie.
    • remove_placeNew – hotový výrobok je odstránený z konca linky a na začiatok sú pridané súčasti pre nový výrobok.

    • AtBox - žeriav sa nachádza nad zásobníkom s hotovými výrobkami (box).
    • startMoveBL - žeriav začne pohyb od zásobníka ku koncu výrobnej linky (line).
    • MovingBL - žeriav sa presúva od zásobníka ku koncu výrobnej linky.
    • stopMoveBL - žeriav zastane nad koncom výrobnej linky.
    • AtLine - žeriav stojí nad koncom výrobnej linky.
    • pickUp - žeriav zoberie hotový výrobok z konca výrobnej linky.
    • AtLineWP - žeriav stojí nad koncom výrobnej linky s uchopeným výrobkom (WP = with product).
    • startMoveLB - žeriav začne pohyb od konca výrobnej linky k zásobníku s uchopeným výrobkom.
    • MovingLB - žeriav sa posúva od konca výrobnej linky k zásobníku s uchopeným výrobkom.
    • stopMoveLB- žeriav zastane nad zásobníkom s uchopeným výrobkom.
    • AtBoxWP - žeriav stojí nad zásobníkom s uchopeným výrobkom.
    • drop - žeriav pustí výrobok do zásobníka.
  5. Sieť assemblyV1 upravte tak, aby bolo odstránenie hotového výrobku z konca linky stotožnené s uchopením výrobku žeriavom.
    Poznámka: Je potrebné zlúčiť príslušné prechody.
  6. Sieť assemblyV1 ďalej upravte tak, aby obsahovala miesto evidujúce počet hotových výrobkov v zásobníku.
  7. Sieť assemblyV1 ďalej upravte tak, aby
    • zásobník mal kapacitu 100 výrobkov a
    • výrobky by z neho bolo možné odstraňovať po 10.
    Poznámka: Inšpirujte sa spôsobom ako z kapacitne obmedzenej PS vyrobíme sieť bez kapacitných obmedzení, ktorá sa bude správať rovnako.
  8. Pomocou simulácie odhadnite stupeň živosti prechodov siete liveness z projektu fssCvicenie3_4. Vašu voľbu zdôvodnite.
    Obr.: Petriho sieť liveness
Zdroje
  1. Nástroj mFDTE/PNtool2.
  2. Projekt fssCvicenie3_4 pre nástroj mFDTE/PNtool2.
  3. Š.Korečko: Doplnkové učebné texty z Formálnych špecifikácií systémov.
comments powered by Disqus