Im folgenden finden Sie eine Beschreibung der weiteren Analyse der zuvor berechneten Graphen. Auf der Basis der Datei STATES.gra untersucht INA Eigenschaften, die eine Kenntnis des Inhalts der Zustände (Markierungen und ggf. Uhrenstellungen) nicht erfordern.
Dieses Kommando führt die weitere Analyse der zuvor mit den Kommandos <R> bzw. <G> berechneten Graphen durch.
Zuerst werden die aktuellen Optionen angezeigt, die Sie wieder mit <Y>
ändern können. Angeboten wird ein Satz von Funktionen, die im folgenden
genauer beschrieben werden. Die von Ihnen ausgewählten
Funktionen werden in der Reihenfolge nacheinander ausgeführt, wie sie
im Optionsmenü angezeigt werden:
Current graph analysis options are:
transition names not to be written ..............................W
draw the graph as a tree ........................................G
to the session file .............................................S
output of the graph matrix ......................................X
computation of the dynamic conflicts ............................Y
no computation of the distances .................................D
no computation of the circuits ..................................Z
computation of terminal SC-components, resetability .............R
liveness test ...................................................L
Nachdem Sie die Optionseinstellung mit <N> beendet haben, öffnet INA die Datei STATES.gra. Falls diese Datei nicht existiert, meldet INA not found und fordert eine Datei mit der Endung .gra an: graph input file. Diese Datei kann eine von Ihnen umgenannte Datei STATES.gra sein, die die Graphstrukturinformationen des aktuellen Netzes enthält. Sie können diese Datei nicht direkt am Terminal eingeben. Sollte die geöffnete Datei nicht mit dem aktuellen Netz übereinstimmen, oder nicht unter den gleichen Optionen (Markenart, Zeitoption, Schaltregel, Benutzung von Prioritäten, Schaltstrategie) erzeugt worden sein, meldet INA : wrong file und graph analysis is impossible und kehrt ins Analysemenü zurück.
Standardmäßig wird der Zustandsgraph als Baum in den Session-Report gezeichnet und die Graphmatrix, die dynamischen Konflikte, und die terminalen starken Zusammenhangskomponenten ausgegeben und die Reversibilität und Lebendigkeit entschieden.
Hier nun eine Beschreibung aller Möglichkeiten:
Mit <W> werden Transitionsnamen und bei gefärbten Netzen mit <C> Transitionsfarben in den Session-Report geschrieben oder nicht.
Mit <G> bestimmen Sie, ob der Graph als Baum gezeichnet werden soll oder nicht. Falls Sie diese Option ausgewählt haben, können Sie zudem mit <S> bestimmen, ob dies in den Session-Report oder in eine seperate Datei mit der Endung .tre geschehen soll.
Der Baum zeigt die Zustandsübergänge des Zustandsgraphen,
wobei keine Bögen zu bereits früher erreichten Zuständen gezeichnet
werden. Ein erneutes Erreichen eines Zustandes wird durch * angezeigt.
Weiter werden tote Zustände durch d, ,,schlechte`` Zustände (Zustände,
in denen Fakten konzessioniert sind, siehe Kapitel 6.2.2
auf Seite 
) durch b und mit c werden
Beschneidungen des Graphen durch eine Tiefenbeschränkung (siehe Kapitel
6.4.3 auf Seite ) angezeigt.
Bei Netzen mit Zeitbewertung wird durch tt ein Verstreichen von Zeit
angezeigt.
Folgende Abbildung zeigt die Baumdarstellung des Zustandsgraphen des Netzes 2.1:
State tree of net 1
..d : dead state; ..* : state reached earlier
..b : bad state, the tree has been cut at this node
..c : cut by depth restriction
s1
|==1=>s2
| |==4=>s1*
|==2=>s3
| |==3=>s4
| | |==5=>s5
<1<<<<<<<<<<<<<<<<<<
s5
|==2=>s4*
|==6=>s1*
>>>>>>>>>>>>>>>>>>0>
| | |==6=>s3*
| |==5=>s1*
|==3=>s5*
Das Schalten der Transition 1 führt vom Anfangszustand s1 in den Zustand s2
(die Zustandsliste des Netzes finden Sie auf Seite ),
schalten der Transition 4 führt zurück in den Anfangszustand, angezeigt
durch s1*.
Falls die Breite des Ausgabemediums nicht ausreichend ist (siehe Kapitel
2.5.6 auf Seite ), werden die
Zeilen beim Erreichen des Randes umgebrochen. Durch <Zahl<<<<<<< wird
eine neue Ebene angedeutet, die Zahl bezeichnet dabei die Ebene, auf der sich
das Zeichnen befindet. Gestartet wird immer auf der Ebene 0. Durch
>>>>>>>Zahl> wird eine Rückkehr auf die Ebene Zahl angedeutet.
Im obigen Beispiel wurde die Zeilenlänge herabgesetzt: Bei Erreichen des Zustandes s5 wird das Zeichnen auf Ebene 1 fortgesetzt, Transition 2 und 6 geschaltet und dann wieder zurück auf Ebene 0 gesprungen und dort von s4 aus weitergezeichnet. Vollständig entfaltet sieht der Baum an dieser Stelle wie folgt aus:
| | |==5=>s5
| | | |==2=>s4*
| | | |==6=>s1*
| | |==6=>s3*
Analog könnten auch weitere Ebenen entfaltet werden.
Sollte die Ausgabe in eine separate Datei umgeleitet worden sein, wird diese nach dem Schreiben geschlossen. Alle weiteren Graphanalysen werden nun wieder in den Session-Report geschrieben.
Eine erneute Ausgabe der Schrittliste (siehe Seite
) kann bei der Schaltstrategie maximale Schritte
an dieser Stelle mit <M> angefordert werden.
Mit <X> bestimmen Sie, ob die Matrix des Zustandsgraphen in den Session-Report ausgegeben werden soll, oder nicht. In dieser Matrix sind die Zustandsnummern die Zeilen und die Transitions- oder Schrittnummern die Spalten. Der Eintrag der i-ten Zeile und j-ten Spalte enthält den Zustand, der erreicht wird, wenn die Transition j im Zustand i geschaltet wird, ein Punkteintrag bedeutet, daß die Transition j im Zustand i keine Konzession hat:
Graph matrix:
=============
| 1 2 3 4 5 6
-----|------------
1| 2 3 5 . . .
2| . . . 1 . .
3| . . 4 . 1 .
4| . . . . 5 3
5| . 4 . . . 1
Für das Netz 2.1 zeigt die Matrix, daß im Zustand 1 durch Schalten der Transition 3 der Zustand 5 erreicht wird, die Punkte in der zweiten Zeile, daß nur die Transition 4 Konzession im Zustand 2 hat.
Bei Netzen mit Zeitbewertung wird zusätzlich eine Matrix der Zeiten für die Übergänge zwischen den Zuständen ausgegeben.
) stehende Transitionen untersuchen soll oder
nicht. Zwei in einem Zustand i in dynamischen Konflikt stehende Transitionen
j und k werden in folgender Form in den Session-Report geschrieben:
i : j # k.
Für das Netz 2.1 wird nur eine Zeile ausgegeben:
1: 1 # 2; 1 # 3; d.h. im Anfangszustand stehen die Transitionen
1 und 2 bzw. 1 und 3 in einem dynamischen Konflikt.
Beachten Sie: Bei einer Reduktion des Zustandsgraphen ist eine Berechnung dynamischer Konflikte nicht möglich. INA meldet: Sorry, not possible for symmetrically or stubborn reduced graphs Für Netze, die unter der Schrittschaltregel betrachtet werden, erscheinen folgende Hinweise: Every two steps enabled at the same state are in conflict und Please, confront the graph matrix. Am Ende der Berechnung wird noch der maximale Ausgangsgrad der Graphknoten ausgegeben. Für das Netz 2.1 meldet INA : maximal outdegree of a graph node = 3.
Mit <D> können minimale und maximale Distanzen zwischen Knoten des Zustandsgraphen berechnet werden. Falls Sie die Abfrage compute minimal distances mit <Y> beantwortet haben, werden die minimalen Entfernungen des am source node Prompt eingegebenen Knotens des Graphen berechnet. Die dabei maximal gefundene Entfernung wird ausgegeben, ebenso eine Auflistung nicht erreichbarer Knoten. Mit der Abfrage print all the distances werden alle Entfernungen des eingegegebenen Knotens zu allen andereren Knoten aufgelistet. Für das Netz 2.2 wird z.B. die minimale Entfernung vom Anfangszustand zum Zustand 322 (alle Philosophen haben die rechte Gabel) als distance(1,322)=5 ausgegeben. Die maximal gefundene Entfernung vom Anfangszustand ist sieben: maximal computed distance = 7 to node nr. 33. Eventuell werden nur obere Schranken gefunden.
Falls Sie die oben erwähnte Abfrage mit N beantworten, berechnet INA die maximalen Entfernungen. Zu Beginn wird folgende Warnung ausgegeben:
Computation of a maximal (loop-free) distance is very hard, if the graph is
not circuit-free. If a graph with circuits is assumed to be circuit-free, then
only a lower bound for the maximal distance is (faster) computed.
Sollten Sie bei einem nicht kreisfreien Graphen nur an einer unteren Schranke interessiert sein, beantworten Sie die Abfrage assume the graph to be circuit-free mit <Y> . Die Berechnung kann sonst sehr aufwendig sein und nicht in der vorhandenen Zeit zu einem Ergebnis kommen. Sie können die Knotennummern zweier Knoten des Zustandsgraphen bestimmen, zwischen denen die maximale (kreisfreie) Entfernung bestimmt werden soll. Die Anzahl gefundener Pfade wird ausgegeben, die laufende Berechnung kann jederzeit mit <Q> abgebrochen werden. Als Ergebnis wird am Ende entweder eine untere Schranke oder die maximale Entfernung ausgegeben, falls die Berechnung diese gefunden hat.
Bitte beachten Sie: Ohne Zeitbewertung wird bei beiden Verfahren die Anzahl geschalteter Transitionen bzw. Schritte gezählt. Bei einer Zeitbewertung haben Sie die Möglichkeit durch Beantwortung der Frage count times mit <Y> stattdessen die dabei vergangene Zeit betrachten zu lassen.
Mit <Z> können Sie entscheiden, ob Kreise im Zustandsgraphen berechnet und bewertet werden sollen.
Zu Beginn der Kreisberechnung erscheinen folgende Optionen:
Work with transition values ..................................V
Print only selected circuits .................................A
Print circuits with minimal length ...........................B
Print circuits with maximal length ...........................C
Print circuits with minimal value ............................D
Print circuits with maximal value ............................E
Print circuits with best efficiency ..........................F
Print circuits with least efficiency .........................G
Print only circuits containing state nr. 0 ...............H
Print not only the first circuit of the selected type ........I
Mit <A> können Sie bestimmen, ob alle Kreise ausgegeben werden sollen. Falls Sie diese Option ausgewählt haben, steht nur noch die Option <V> zur Verfügung, sonst können Sie mit <B> bzw. <C> Kreise mit minimaler bzw. maximaler Länge ausgeben lassen. Die Länge ergibt sich aus der Anzahl geschalteter Transitionen bzw. Schritte.
Mit <V> können Sie eine Arbeit mit Bewertungen der Transitionen anfordern. Danach stehen weitere Optionen zur Verfügung: Mit <D> bzw. <E> können Sie Kreise mit minimaler bzw. maximaler Bewertung ausgeben lassen. Die Bewertung eines Kreises ist die Summe der Bewertungen der Transitionen des Kreises. Die Effizienz ergibt sich aus dem Quotienten der Bewertung und der Länge des Kreises. Mit <F> bzw. <G> können Sie Kreise mit minimaler bzw. maximaler Effizienz auswählen.
Mit <H> können Sie Kreise auswählen lassen, die einen bestimmten Zustand enthalten. Durch Eingabe einer Nummer eines Zustandes des Graphen werden nur Kreise ausgegeben, die diesen Zustand enthalten. Der Zustand 0 ist nie im Graph enthalten und dient zur Ausgabe aller Kreise unter Berücksichtigung der restlichen Optionen.
Durch Auswahl von <I> wird nur jeweils der erste Kreis der ausgewählten Typen ausgegeben.
Nach der Optionseinstellung beginnt die Berechnung. Falls Sie eine Arbeit mit Transitionsbewertungen angefordert haben, wird eine Datei mit der Endung .val am values input file Prompt angefordert. Nach Drücken von <esc> können Sie diese Datei auch direkt am Terminal eingeben. In diesem Fall werden die Transitionsbewertungen abgefragt. Nach Eingabe einer Transitionsnummer wird deren Namen angezeigt und die Bewertung (Kosten) angefordert. Nachdem Sie die Eingabe einer Zahl mit <Q> beendet haben, werden die Bewertungen der nicht spezifizierten Transitionen auf Null gesetzt. Sie haben die Möglichkeit, die eingegebene Bewertungen in eine Datei zu schreiben.
Der Fortschritt der Berechnung wird durch einen Zähler berechneter Kreise angezeigt. Selbstverständlich kann jederzeit mit <Q> abgebrochen werden.
Die Kreise werden in den Session-Report geschrieben, dabei wird jeder Kreis mit umgekehrter Orientierung ausgegeben. Mit Nx<-ty-Nz wird angedeutet, daß die Transition mit der Nummer y Teil eines Kreises ist und das Schalten der Transition y vom Zustand z zum Zustand y führt. Die Nummern der Zustände beziehen sich auf die zuvor berechnete Zustandsliste.
Ein Beispiel für das Netz 6.1 sieht so aus:
Circuit nr. 1:
N1<-t4--N4<-t3--N3<-t2--N2<-t1--N1
Corresponding T-invariant:
TR: 1 2 3 4
: 1 1 1 1
Livelocked transitions: none
Circuit length = 4
Der Kreis besteht aus den Transitionen t1, t2, t3 und t4 und führt vom Anfangszustand zurück in den selben.
Zusätzlich ausgegeben werden zugehörige Transitionsinvarianten. Diese
entsprechen realisierbaren T-Invarianten (siehe Seite
im Kapitel 6.5).
Weiterhin werden Transitionen ausgegeben, die sich in einem Livelock befinden. Eine Transition t befindet sich in einem Livelock, wenn es einen Kreis im Zustandsgraphen gibt, indem t nicht schaltet [Sta90, Kapitel 12 (123-133),]. Das zugehörige Netz kann also fortwährend schalten, ohne daß die lebendige Transition t geschaltet wird, t ,,verhungert``. Besonders deutlich wird dies in den Kreisen des Erreichbarkeitsgraphen des Netzes 2.2 der speisenden Philosophen, in dem es viele Transitionen gibt, die sich in einem Livelock befinden können.
Mit <R> werden die terminalen starken Zusammenhangskomponenten berechnet. Dies sind die starken Zusammenhangskomponenten des Zustandsgraphen, aus denen keine Bögen herausführen. Sie werden in Form eines Intervalls ausgegeben. Die Knoten des Erreichbarkeitsgraphen, die in einem der ausgegebenen Intervalle liegen, sind jeweils durch gerichtete Wege voneinander erreichbar. Tote Zustände bilden immer ein Intervall mit gleicher Ober- und Untergrenze. Für das Netz 2.2 werden folgende terminale starke Zusammenhangskomponenten berechnet: 1: [6..6] und 2: [322..322].
Falls der gesamte eingelesene Graph stark zusammenhängend ist, die
Berechnung zuvor nicht abgebrochen wurde und Sie keine sture Reduktion
angefordert haben, kann INA daraus folgern, daß der Graph rücksetzbar
(siehe im Kapitel 6.2.2 auf Seite ) ist.
Bitte beachten Sie: Überdeckbarkeitsgraphen sind nicht rücksetzbar [Sta90, Abbildung 6.3 (60),]. INA gibt eine entsprechende Warnung aus.
Für Netze unter Zeitbewertung wird gegebenenfalls eine Liste der Time-Deadlocks ausgegeben.
Mit <L> kann eine Lebendigkeitsanalyse
durchgeführt werden. Diese funktioniert nur für vollständig berechnete
Zustandsgraphen ohne sture Reduktion.
Für unter der maximalen Schrittschaltregel ausgeführte Netze kann die
Lebendigkeit von Schritten untersucht werden:
Test liveness of steps?.
Falls das Netz Transitionen enthält, die im Anfangszustand tot sind
(siehe Seite im Kapitel 6.2.2), dann bezieht sich
die Lebendigkeitsanalyse nur auf Transitionen, die nicht tot sind:
Liveness analysis refers to the net where all dead
transitions are removed (considered as facts).
Das Netz kann lebendig sein, wenn alle toten Transitionen als Fakten
betrachtet werden, die Eigenenschaft LV (Lebendigkeit unter Ignorierung
toter Transitionen) wird dann entsprechend gesetzt (siehe auch Seite
im Kapitel 6.2.2).
Weitere abgeschwächte Lebendigkeitsbegriffe werden gegebenenfalls auf dem
Bildschirm erklärt:
Zum einen die schwache Lebendigkeit (Seite im Kapitel
6.2.2: A transition is weakly live IFF it has a live colour),
zum anderen die kollektive Lebendigkeit (Seite im Kapitel
6.2.2: A net is collectively live IFF every transition is
collectively live at the initial state. A transition t is
collectively live IFF for every reachable state m there exists a colour c of
t and a state m' reachable from m such that t has concession in colour
c at m').
Eventuell werden Transitionsmengen ausgegeben, die nicht schwach lebendig sind, bzw. die kollektiv lebendig sind (the following transitions are not weakly live bzw. the set of collectively live transitions).
Zuletzt geändert am: Thu Apr 10 15:08:18 MET DST 1997