Lernziele
- Modellierung mit Petri-Netzen
- Berechnung von Invarianten
- Entwurf und Verifikation einer einfachen Steuerung am Modell
- Arbeit mit TimeNET
Unterlagen
- Vorlesungsunterlagen zu Petri-Netzen
- TimeNET User Manual Version 3, Version 4
- TimeNET-Umgebung
- TimeNET Installationshinweise
- Vorgegebenes Modell ~pdv/lehre/pmfe/Eisenbahn.net (TimeNET 3.x) bzw. ~pdv/lehre/pmfe/Eisenbahn.xml (TimeNET 4.x)
Aufgabenstellung
Für die Modelleisenbahnanlage ist eine Steuerung mit Hilfe eines GSPN-Modells zu entwerfen und auf Funktionstüchtigkeit zu prüfen.
Teil 1 - Berechnen von Invarianten
Berechnen Sie von Hand die minimalen Stellen-Invarianten des folgenden Petri-Netz-Modells. Verwenden Sie dazu einen der in der Vorlesung bzw. Großübung dargestellten Algorithmen.
Teil 2 - Modell der Fahrpläne
Kopieren Sie sich das vorgegebene Petri-Netz-Modell in Ihr TimeNET-Modellverzeichnis. Das Modell zeigt beispielhaft den Fahrplan einer Lok auf dem Gleisplan. Erweitern Sie das Modell in TimeNET und löschen Sie überflüssige Teile so, dass es nebeneinander/ineinander die unabhängigen Fahrpläne der Loks 1 und 2 zeigt.
Fahrplan
Lok 1 fährt aus dem Abschnitt K6-K1 Richtung K1 auf dem Außenkreis (K1 K13 K14 K7 K12 K16 K15 K6 usw.), während Lok 2 aus dem Abschnitt K12-K7 in Richtung K7 in Form einer Acht über die Kreuzungsweiche (K7 K8 K9 K4 K5 K6 K1 K2 K3 K10 K11 K12 usw.) fährt. Achten Sie auf eine sinnvolle und verständliche Benennung der Modellelemente. Außerdem muss die Anfangsmarkierung des Modells entsprechend der genannten Startposition gewählt werden.
Teil 3 - Modell der gesteuerten Strecke
Überlegen Sie sich, wie die Loks so gesteuert werden können, dass folgende Bedingungen erfüllt sind:
- Es befindet sich maximal eine Lok in jedem Streckenabschnitt.
- Als zusätzliche Sicherheit bei Kontaktausfällen muss sich zwischen den durch die Loks belegten Abschnitten immer mindestens ein freier Sicherheitsabschnitt befinden.
- Loks können angehalten werden, um die genannten Bedingungen zu erfüllen.
- Es tritt kein deadlock auf, d.h. jede Lok kann nach einem Halt wieder weiter fahren.
- Es findet keine unnötige Beschränkung der Fahrtmöglichkeiten statt.
Erweitern Sie das Modell aus Teil 2 um Ihre Steuerstrategie. Dazu dürfen ausschließlich zusätzliche Stellen verwendet werden, die wie Semaphore die Freigabe und das Anfordern von Streckenabschnitten modellieren. Diese Stellen werden durch Kanten mit den Transitionen verbunden, die Betreten bzw. Verlassen eines Abschnittes (Überfahren eines Kontakts) modellieren. Verwenden Sie so wenig wie möglich Stellen und Kanten, so dass das entstehende Modell möglichst einfach und übersichtlich bleibt. Achten Sie auch auf die richtige Anfangsmarkierung der Semaphorstellen.
Testen Sie die Funktionsfähigkeit Ihrer Steuerstrategie am Modell mit Hilfe des token games von TimeNET.
Teil 4 - Untersuchung des Steuermodells
Berechnen Sie die Stellen-Invarianten Ihres Modells mit TimeNET. Ist jede Stelle in mindestens einer Invariante enthalten? Falls nicht, liegt wahrscheinlich ein Modellfehler vor. Überlegen Sie, ob aus den Invarianten die Gültigkeit der ersten Bedingung für Ihre Steuerstrategie nachweisbar ist.
Zur Abgabe der Aufgabe gehört die Angabe der Invarianten aus Teil 1 mit Rechenweg, jeweils ein Ausdruck/PDF der Modelle aus Teil 2 und 3, die Angabe (oder Ausdruck) der Stellen-Invarianten für das Eisenbahnmodell, sowie der Nachweis für die erste Bedingung mit Hilfe der Stellen-Invarianten für den Streckenabschnitt K7-K12.
