next up previous contents index
Next: 6.5.4 Graphberechnung und -analyse Up: 6.5 Erreichbarkeitsanalyse Previous: 6.5.2 Prädikate und CTL-Modellchecking

Unterabschnitte


6.5.3 Pfadberechnung

Die Pfadberechnung beruht auf der teilweisen Berechnung des Zustandsgraphen und gehört deshalb zur Erreichbarkeitsanalyse.

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.

<P> Compute a shortest path from the initial state to a target marking

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.


Ergebnisanzeige

Am Beispiel des Netzes 2.1 wird die Berechnung eines Pfades gezeigt. Dabei bedeutet die verwendete Teilmarkierung, daß die Programmierer zwei und drei am Terminal arbeiten.

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.


Weitere Pfadberechnungen

Neben der zuvor beschriebenen Pfadberechnung gibt es weitere Möglichkeiten:

<O> Compute a minimal path from the initial state to satisfy a predicate

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.


next up previous contents index
Next: 6.5.4 Graphberechnung und -analyse Up: 6.5 Erreichbarkeitsanalyse Previous: 6.5.2 Prädikate und CTL-Modellchecking

© 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