Teoria współbieżnosci - Sieci Petriego

Do zajęć będziemy używać symulatora Pipe2

Maszyna stanów. Prosty model maszyny stanów swiateł ulicznych przedstawia sieć na rysunku poniżej:

Stanami są miejsca sieci, zaś znacznik pokazuje w jakim stanie aktualnie się znajdujemy.

Narysować przykład w symulatorze.
Sprawdzić właściwości sieci (ograniczoność, bezpieczeństwo i możliwy deadlock) w symulatorze Pipe w menu "State Space Analysis".
Wygenerować graf osiągalnosci "Reachability/Coverability Graph". Zaobserwować:
- Jakie znakowania są osiągalne?
- Ile wynosi maksymalna liczba znaczników w każdym ze znakowań? Jakie możemy wyciągnać z tego wnioski n.t. ograniczoności i bezpieczeństwa?
- Czy każde przejście jest przedstawione jako krawędz w grafie? Jaki z tego wniosek n.t. żywotnosci przejść?
- Czy wychodząc od dowolnego węzła grafu (znakowania) można wykonać dowolne przejście? Jaki z tego wniosek n.t. żywotności sieci? Czy są możliwe zakleszczenia?
Wykonać analizę niezmienników (wybrać w menu "Invariant Analysis").
- wynik analizy niezmienników przejść (T-invariants) pokazuje nam, ile razy trzeba odpalić dane przejście (T), aby przekształcić znakowanie początkowe z powrotem do niego samego (wynik nie mówi nic o kolejności odpaleń). Z wyniku możemy m.in. wnioskować o odwracalności sieci.
- wynik analizy niezmienników miejsc (P-invariants) pokazuje nam zbiory miejsc, w których łączna suma znaczników się nie zmienia. Pozwala to wnioskować n.t. zachowawczości sieci (czyli własności, gdzie suma znaczników pozostaje stała) oraz o ograniczoności miejsc.

Rozwiązania do zadań wraz z dyskusją należy zawrzeć w sprawozdaniu

Zadanie 1 - zasymulować poniższą sieć.

Dokonac analizy niezmienników przejść. Jaki wniosek mozna wyciagnać o odwracalności sieci? Wygenerować graf osiągalności. Proszę wywnioskować z grafu, czy sieć jest żywotna i ograniczona. Objaśnić wniosek.
Zadanie 2 - uruchomić problem producenta i konsumenta z ograniczonem buforem (mozna posłużyć się przykładem, menu: file/xamples). Dokonać analizy niezmienników. Czy sieć jest zachowawcza? Które równanie mówi nam o rozmiarze bufora ?
Zadanie 3 - stworzyć symulację problemu producenta i konsumenta z nieograniczonym buforem. Dokonać analizy niezmienników. Zaobserwować brak pełnego pokrycia miejsc.
Zadanie 4 - zasymulować wzajemne wykluczanie dwóch procesów na wspólnym zasobie. Dokonać analizy niezmienników. Wyjaśnij znaczenie równań (P-invariant equations). Które równanie pokazuje działanie ochrony sekcji krytycznej?
Zadanie 5 - zasymulować prosty przykład ilustrujący zakleszczenie. Wygenerować graf osiągalności i zaobserwować znakowania, z których nie można wykonać przejść. Zaobserwować właściwości sieci w "State Space Analysis". Ponizej przykład sieci z możliwością zakleszczenia (należy wymyślić inny):

Katarzyna Rycerz, kzajac at agh.edu.pl
Bartosz Baliś, balis at agh edu pl