Zeitbehaftete Petri Netze

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Zeitbehaftete Petri Netze
hi,

hat jemand ne ahnung wie man mithilfe eines Klassendiagrammes eines TPN feststellt, ob ein TPN tot ist, aktivierbar, lebendig, erreichbar etc.
das geht aus den folien nicht so klar heraus.


Glaub nicht, dass das so relevant ist für die Prüfung … und bin mir nicht sicher ob das anhand des Klassendiagrams überhaupt geht. Die Folien suggerieren ja, dass man sich dazu direkt das TPN anschauen müsste.


es geht mir um die Aufgabe 5.1 aus den Übungsblättern. Dort findet man eine richtige Variante und ne fehlerhafte Variante des TPN. Bei der Fehlerhaften Variante müsste es doch am Klassendiagramm sichtbar sein, dass das TPN einen Zustand erreicht wo es tot ist, dazu macht man doch diese Klassendiagramme???


Ich hab mir die Aufgabe nochmal angeschaut … sowohl die richtige als auch die fehlerhafte Variante erreichen einen Zustand, in dem sie tot sind(Das ist der Fall in dem die Markierungen auf p3 und p6 liegen). Das macht auch Sinn, weil in diesem Zustand der Backuprechner die Kontrolle übernommen hat und das Petri Netz, das ja nur dazu da ist nach einer gewissen Zeit den Backuprechner zu aktivieren, seine “Aufgabe” erfüllt hat.
Erkennen kann man das im Klassendiagram daran, dass es eine Klasse gibt, aus der man nicht mehr rauskommt(In der richtigen Variante ist das Klasse 5, in der fehlerhaften Klasse 7).

Der Unterschied zwischen richtiger und fehlerhafter Variante hat also nichts mit Lebendigkeit zu tun, sondern damit, dass in der fehlerhaften Variante, der Backuprechner die Kontrolle übernimmt, obwohl der andere Rechner noch arbeitet und eben nicht ausgefallen ist. Der Knackpunkt ist Transition t4, die in der richtigen Variante das statische Zeitintervall [3,4] hat(im Gegensatz zur fehlerhaften Variante, in der das Zeitintervall [3,5] ist).


ich glaube, nicht nur Korrektheit sondern Erreichbarkeit auch durch Zustandsklassengraphen nachgewiesen bzw. widerlegt wird.