Diese Funktion kann die Nichterreichbarkeit einer Markierung mittels der Zustandsgleichung entscheiden. Dabei reicht eine Teilmarkierung aus. Die Markierungen der restlichen Plätze werden als nicht definiert betrachtet, d.h. als don't care Bedingungen behandelt (siehe auch Seiteim Kapitel 6.5.3).
Es wird geprüft, ob die Zustandsgleichung
mit der
transponierten Inzidenzmatrix C des Netzes, der Anfangsmarkierung m0
und der parametrisierten Teilmarkierung m lösbar ist.
Dazu wird die Lösbarkeit einer zugeordenten Hilfsaufgabe dieses linearen
Problems mit der Simplexmethode betrachtet. Ist dieses nicht lösbar,
folgt daraus die Nichterreichbarkeit. Während der Berechnung läuft ein
Zähler (eliminated columns). Im Falle der Lösbarkeit der
Zustandsgleichung wird eine Lösung ausgegeben, es kann keine Entscheidung
bezüglich Nichterreichbarkeit getroffen werden.
Für das Netz 6.1 ist klar, daß der Platz fünf nicht markierbar
ist, aber mit dem Nichterreichbarkeitstest über Invarianten kann diese
Entscheidung nicht getroffen werden:
place invariants base
=================
1 | 1: 1, 2: 1, 3: -1, 4: -1
2 | 1: 1, 2: 1, 5: 1 +
At least the following places are covered by semipositive invariants:
1, 2, 5
Non-reachability test of the state:
p : 1 2 3 4 5 6
m(p): 0 0 0 0 1 0
No conclusions possible.
Mittels der Zustandsgleichung kann dagegen die Nichterreichbarkeit nachgewiesen
werden:
Testing non-reachability of a partial marking
target submarking:
5:1;
The marking is not reachable.
Für das gezeigte Netz kann mit der Zustandsgleichung keine Aussage über die (Nicht-)markierbarkeit von Platz zwei gewonnen werden, da die Zustandsgleichung lösbar ist:
Testing non-reachability of a partial marking
target submarking:
2:1;
The state equation is solvable:
t2: 1 t4: 1
© 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