6.4.2 Schneller Nichterreichbarkeitstest

Im Analysemenü kann ein schneller Nichterreichbarkeitstest für partielle Markierungen durchgeführt werden. Dieser Test steht neben dem Nichterreichbarkeitstests bei der Invariantenberechnung (siehe auf Seite im Kapitel 6.6.1) und den Erreichbarkeitstests, die auf einem (teilweisen) Aufbau des Erreichbarkeitsgraphen basieren (siehe ab Seite im Kapitel 6.5).

<N> Non-reachability test of a partial marking using the state equation

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 Seite im Kapitel 6.5.3).

Es wird geprüft, ob die Zustandsgleichung $C\cdot x = m - m_0$ mit der transponierten Inzidenzmatrix C des Netzes, der Anfangsmarkierung m₀ 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.

Abbildung 6.1: Ein Netz bei dem ein Platz nicht markierbar ist (stateeq.pnt)

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