Diese Funktion entscheidet, ob das Netz mit P-Subinvarianten überdeckt ist. Ist dies der Fall, so ist es bei jeder Anfangsmarkierung, d.h. strukturell beschränkt (siehe auch die Erläuterungen im Kapitel 6.6 ab Seite und unter SB im Kapitel 6.2.2 auf Seite ).Es wird geprüft, ob das Gleichungssystem , mit der Inzidenzmatrix C des Netzes lösbar ist. Dazu wird die Lösbarkeit einer zugeordenten Hilfsaufgabe dieses linearen Problems mit der Simplexmethode betrachtet. Ist dies der Fall, so ist das Netz mit P-Subinvarianten überdeckt. Während der Berechnung läuft ein Zähler (eliminated columns).
Für das Netz 2.2 der speisenden Philosophen ergibt die Berechnung folgendes:
Deciding structural boundedness
The net is structurally bounded.
The net is bounded.
There are no proper semipositive T-surinvariants.
The net is covered by semipositive place sub-invariants.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2 2 2 2 2
In der letzten Zeile ist die Ausgabe einer überdeckende P-Subinvariante zu sehen.
© 1996-98 Prof. Peter H. Starke (starke@informatik.hu-berlin.de) und Stephan Roch (roch@...)
INA Handbuch Version 2.1 zuletzt geändert: 1998-03-24