Beachten Sie bei Netzen mit Zeitbewertung, daß transiente Zustände nicht betrachtet werden. Wenn Ihre Markierung nur in einem transienten Zustand vorkommt, wird INA sie nicht finden und sie als unerreichbar qualifizieren, sofern der gesamte Zustandsgraph konstruiert werden kann.
Eine Markierung wird auf Erreichbarkeit getestet und eventuell ein Pfad ausgegeben. Der Weg ist ein kürzester in bezug auf die Zahl der Schaltvorgänge. Dabei reicht eine Teilmarkierung aus. Die Markierungen der restlichen Plätze werden als nicht definiert betrachtet, d.h. als don't care Bedingungen behandelt.Die zu untersuchende Markierung kann von einer Datei eingelesen werden oder (durch Eingabe von <esc> ) auch direkt eingegeben werden.
Bei einem zeitbewerteten Netz kann neben der Berechnung eines kürzesten Pfades alternativ ein Pfad berechnet werden, der minimal in Bezug auf Zeitverbrauch (d.h. ein schnellster) ist (compute a minimal time path). Auf jeden Fall wird die Zeitbewertung abgefragt.
Nach dem Eingeben bzw. Einlesen der Zielmarkierung beginnt INA damit, den Zustandsgraphen des Netzes in der Breite zuerst aufzubauen. Die Anzahl der berechneten Zustände wird angezeigt: States generated.
Trifft INA auf eine Markierung, die mit der Zielmarkierung auf den definierten Plätzen übereinstimmt, so bricht die Untersuchung ab. Die Zielmarkierung wird auf dem Bildschirm als erreichbar gemeldet: The marking is reachable. Der Weg kann in eine separate Datei mit der Endung .tra oder in den Session-Report geschrieben werden.
Wenn die Zielmarkierung nicht erreichbar ist, gibt es zwei Möglichkeiten: Kann der gesamte Zustandsgraph aufgebaut und gespeichert werden, dann wird die Markierung als unerreichbar gemeldet (The marking is not reachable), anderenfalls (bei unbeschränktem Netz immer) bricht INA mit der Meldung Nodeoverflow ab und zeigt an, daß keine Entscheidung getroffen werden kann: No decision possible.
Der Berechnungsprozeß kann jederzeit durch Eingeben von <Q> abgebrochen werden.
Eventuell gefundene tote Zustände werden für die weitere Analyse berücksichtigt.
Falls die Methode der sturen Reduktion angewendet werden kann (siehe Seite im Kapitel 6.5.1), wird mit Hilfe einer Netzkonstruktion der Zustandsgraph so stur reduziert aufgebaut, daß trotzdem ein minimaler Pfad zur gesuchten Teilmarkierung gefunden wird.
Computation of a shortest path.
target submarking:
2:1; 3:1;
The marking is reachable.
Trace of length 2
State nr. 1
P.nr: 0 1 2 3 4 5 6
toks: 2 0 0 0 1 1 1
n1====2.login_Prog2 ==> n3
State nr. 3
P.nr: 0 1 2 3 4 5 6
toks: 1 0 1 0 1 0 1
n3====3.login_Prog3 ==> n5
State nr. 5
P.nr: 0 1 2 3 4 5 6
toks: 0 0 1 1 1 0 0
States generated: 6
In diesem Beispiel ist zweimaliges Schalten nötig, um von der Anfangsmarkierung zur Zielmarkierung zu gelangen. In der Anfangsmarkierung n1 wird der Zustand n3 durch das Schalten der Transition 2 und in diesem Zustand durch das Schalten der Transition 3 die Zielmarkierung im Zustand n5 erreicht. Einfach gesagt: Falls die beiden Programmierer zwei und drei in der Anfangssituation das Login ausführen, wird die gegebene Zielmarkierung erreicht.
Diese Funktion berechnet einen minimalen Pfad zu einem Zustand, der ein zuvor eingegebenes Zustandsprädikat (zur Definition und Eingabe siehe ab Seite im Kapitel 6.5.2) erfüllt.
Im Gegensatz zur Pfadberechnung mit <P> stehen folgende Minimalitätskriterien zur Verfügung:
Computation of a minimal path to a state satisfying a predicate:
'minimal' to be understood as minimal length........L
'minimal' to be understood as minimal time..........T
'minimal' to be understood as minimal value.........V
Minimale Länge und minimaler Zeitverbrauch sind analog zu den bei <P> beschriebenen Möglichkeiten definiert. Bei der Berechnung eines Pfades mit minimalem Wert wird zuvor jeder Transition ein Wert zugewiesen. Diese Werte können von einer Datei mit der Extension .val gelesen oder nach Eingabe von <esc> am values input file Prompt auch direkt eingeben werden. Der Wert eines Pfades ergibt sich als Summe der Bewertungen der gefeuerten Transitionen: The value of a path is the sum of the values of the fired transitions (zur Verwendung von Bewertungen siehe auch ab Seite im Kapitel 6.5.4).
Nach dem Einlesen eines Prädikates können Sie durch Angabe eines sogenannten ,,bad`` Prädikat den Suchraum einschränken: Falls das Prädikat durch einen Zustand erfüllt wird, wird der Zustand nicht mehr weiter entwickelt (siehe auch Seite im Kapitel 6.5.4).
Ansonsten ist der Ablauf und die Ergebnisanzeige dieser Funktion analog zu der zuvor bei <P> beschriebenen.
© 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