Lernziele

Unterlagen

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.

Invarianten Beispiel

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:

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.