next up previous contents index
Next: 6.6 Invariantenanalyse Up: 6.5 Erreichbarkeitsanalyse Previous: 6.5.3 Pfadberechnung

Unterabschnitte


6.5.4 Graphberechnung und -analyse

In diesem Abschnitt finden Sie eine Beschreibung der Berechnung und Analyse eines Zustands- bzw. Überdeckbarkeitsgraphen beginnend mit einer Vorstellung der Optionen und dem weiteren Ablauf.

INA bietet folgende Funktionen zur Graphberechnung an:

<R> Compute a reachability graph

Dieses Kommando baut den Zustandsgraphen auf, wobei dieser symmetrisch bzw. stur reduziert berechnet werden kann. Im Anschluß können verschiedene Graphanalysen durchgeführt, CTL-Formeln und Prädikate erzeugt bzw. gecheckt und verschiedene Ergebnisse in separate Dateien bzw. in den Session-Report geschrieben werden.

<G> Compute a coverability graph

Dieses Kommando baut den Überdeckbarkeitsgraphen auf, wobei dieser symmetrisch reduziert bzw. nach FINKELS Methode berechnet werden kann. Eine weitere Analyse des Graphen ist nicht möglich.


Optionen

INA zeigt zu Beginn der Berechnung die Optionen an, unter denen diese durchgeführt werden soll:
Current analysis options are:
     no symmetrical reduction ........................................Y
     no stubborn reduction ...........................................U
     no depth restriction ............................................D
     do not use a 'bad' predicate ....................................B

Sie können folgende Einstellungen vornehmen:


Berechnungsart

Mit der Berechnungsart können Sie die zuvor vorgestellten Graphreduktionen anwählen. Mit <Y> bzw. <U> können Sie eine symmetrische bzw. sture Reduktion des Graphen einstellen, falls dies für das aktuelle Netz möglich ist. Im Falle eines Erreichbarkeitsgraphen können beide Möglichkeiten (falls Sie angeboten werden) beliebig kombiniert werden, für Überdeckbarkeitsgraphen steht nur die symmetrische Reduktion zur Verfügung. Falls die Symmetriegruppe nicht schon vorher berechnet worden ist, geschieht dies unmittelbar nach der Optionseinstellung. Siehe dazu die Beschreibung des Kommandos <Y> auf Seite [*] im Kapitel 6.5.1.

Mit <R> können Sie für Überdeckbarkeitsgraphen zusätzlich eine Reduktion nach der Methode von FINKEL auswählen.


Tiefenbeschränkung

Mit der Option <D> kann die Tiefe festgelegt werden, bis zu der der Zustandsgraph berechnet werden soll. Durch Eingabe der Tiefe 0 wird die Tiefenbeschränkung aufgehoben.


,,Bad`` Prädikat

Eine Beschränkung der Berechnung des Zustandsgraphen ist mit einem ,,bad`` Prädikat möglich: Falls das Prädikat durch einen Zustand erfüllt wird, wird der Zustand nicht mehr weiter entwickelt, die Eigenschaft BSt (siehe Kapitel 6.2.2 auf Seite [*]) wird gesetzt. Zur Prädikateingabe siehe die Beschreibung auf Seite [*] im Kapitel 6.5.2. Die Benutzung eines solchen Prädikates bei Überdeckbarkeitsgraphen ist nicht möglich.

Erreichbarkeits- bzw. Überdeckbarkeitstest

Nur beiÜberdeckbarkeitsgraphen können Sie mit dieser Option ( <T> ) im Anschluß an die Graphberechnung einen Test auf Erreichbarkeit oder Überdeckbarkeit einer Markierung anwählen. Bei Erreichbarkeitsgraphen steht diese Möglichkeit dagegen als Funktion im Graphanalysemenü (mit <R> ) zur Verfügung. Zur Beschreibung siehe deshalb auch Seite [*].


Ablauf der Berechnung

Zu Beginn der Berechnung prüft INA , ob bereits die Beschränktheit des Netzes bekannt ist. Falls nicht, dann werden Sie gefragt, ob der Test auf überdeckende Markierungen bei der Graphberechnung ausgelassen werden soll oder nicht: omit boundedness test?. Falls Sie die Frage mit <Y> beantworten, oder INA automatisch den Test abschaltet, kann die Berechnung wesentlich schneller durchgeführt werden als mit eingeschaltem Test. Führen Sie deshalb vor der Graphberechnung eventuell einen Test auf strukturelle Beschränktheit durch.

Der laufende Fortschritt der Graphberechnung wird durch die Anzahl der erzeugten Zustände angezeigt.

Die Berechnung kann jederzeit durch Eingabe von <Q> abgebrochen werden. Im Fall, daß aus Platzgründen nicht der gesamte Zustandsgraph erzeugt werden kann, bricht INA mit der Meldung Nodeoverflow ab. Die Berechnung eines Zustandsgraphen wird unterbrochen, wenn INA entdeckt, daß das aktuelle Netz unbeschränkt ist (bei unbeschränkter Tiefe). In beiden Fällen ist der berechnete Graph nicht vollständig: computed graph is not complete.

Am Ende der Graphberechnung wird in den Session-Report ein Überblick über die berechneten Zustände (states generated) und erzeugten Bögen (arcs generated) und außerdem über die benötigten Kapazitäten (needed capacities) geschrieben: Für jeden Platz wird angezeigt, wieviele Marken auf ihm während der Berechnung maximal gelegen haben. Bei unvollständiger Zustandsgraphberechnung sind entsprechend nur die bis dahin berechneten Markierungen berücksichtigt. Nachfolgend können eventuell gefundene tote bzw. ,,schlechte`` Zustände ausgeschrieben werden (z.B. write the state numbers of the dead states?).

Für das Netz 2.2 der speisenden Philosophen sehen die ersten Ergebnisse wie folgt aus:

States generated: 393
Arcs generated: 1420

Capacities needed:
Place  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 Cap:  1  1  1  1  1  1  1  1  1  1  1  1  1  1  1  1  1  1  1  1
Dead states:
        6, 322,
Number of dead states found: 2

Bei der Berechnung des Überdeckbarkeitsgraphen wird im unbeschränkten Fall nicht abgebrochen, sondern die Markierung an den entspechenden Stellen oo ($\omega$) gesetzt. INA meldet zu Beginn, welche Konstante die höchste Markenzahl eines beschränkten Platzes sein kann: It is assumed that all bounded places are 4294836224-bounded. Diese Konstante ist abhängig von der Implementation und ist auf jeden Fall kleiner als der interne Wert von oo ($\omega$ -- der angegebene Wert entspricht dem der UNIX-Implementation).

Im beschränkten Fall unterscheiden sich die berechneten Graphen nicht, der Algorithmus von KARP und MILLER berechnet dann den Zustandsgraphen (dieser kann aber nicht weiter analysiert werden, bitte benutzen Sie deshalb in diesem Fall die Funktion <R> ).

Falls Sie bei der Berechnung des Überdeckbarkeitsgraphen die Methode von FINKEL ausgewählt haben, so unterscheidet sich die Bildschirmausgabe während der Berechnung. INA zählt die Anzahl der berechneten Bögen, erst am Ende wird die Zahl generierter Knoten ausgegeben.

Bei Überdeckbarkeitsgraphen wird optional ein Test auf Erreichbarkeit bzw. Überdeckbarkeit einer Markierung durchgeführt (siehe die Beschreibung im nächsten Abschnitt). Eine weitere Analyse des Überdeckbarkeitsgraphen ist nicht möglich.


Weitere Graphanalyse

Nach dem Aufbau des Zustandsgraphen werden erste Folgerungen gezogen. Dann wird das Graphanalysemenü angezeigt (nicht für Überdeckbarkeitsgraphen):

Graph analysis menue
Do You want to
     quit analysis of the computed graph ................. Q

     test the reachability/coverability of a marking ..... R
     convert a set of states to a predicate .............. C
     define an enabledness predicate ..................... E
     check a CTL-formula ................................. F
     compute distances ................................... A
     compute circuits .................................... K
     check liveness properties ........................... L
     compute strongly connected components ............... V
     check dynamic conflicts ............................. Y

     write all computed states ........................... W
     write all states satisfying a predicate ............. X
     write the dead states ............................... D
     write the bad states ................................ B
     write the list of executed steps .................... S
     write a trace to a state ............................ T
     write the matrix of the graph ....................... M
     write the matrix of the transitional periods ........ P
     inspect a result file ................................I
choice>

Die einzelnen Funktionen werden in den folgenden Abschnitten erläutert. Mit <Q> beenden Sie die Graphanalyse, INA kehrt in das Analysemenü zurück.

Erreichbarkeits-/Überdeckbarkeitstest

<R> test the reachability/coverability of a marking

Mit dieser Funktion können Sie Erreichbarkeits- bzw. Überdeckbarkeitstests durchführen und (nicht notwendig kürzeste) Wege von der Anfangsmarkierung zu einer Zielmarkierung abfragen.

Für Überdeckbarkeitsgraphen ist diese Funktion als Graphberechnungsoption mit <T> anwählbar (siehe Seite [*]).

INA fragt zuerst nach der Nummer der Markierung, die diese bei dem Aufbau des Zustandsgraphen erhalten hat. Durch Eingabe von <N> können Sie selbstverständlich eine Markierung von Datei einlesen oder direkt eingeben. Beachten Sie: Unter Zeitbewertung werden transiente Zustände nicht betrachtet.

Wenn die Markierung nicht erreichbar ist, meldet INA dies und bietet einen Überdeckbarkeitstest an. Sollte auch dieser negativ ausfallen, so wird die Markierung auch als nicht überdeckbar gemeldet. Sonst wird eine überdeckende Markierung ausgegeben, durch Beantwortung der Frage next? mit <Y> können Sie weitere anzeigen, bis INA meldet, daß keine mehr existiert: no more covering marking found. Unter Zeitbewertung wird die Markierung bei der Ausgabe als Komponente eines Zustandes bezeichnet.

Falls Sie eine symmetrische Reduktion des Graphen als Option gesetzt haben, so müssen Sie beachten, daß eventuell schwächere Ergebnisse erreicht werden: Es kann vorkommen, daß nur eine äquivalente Markierung gefunden wird: by symmetry the marking is reachable. Sollte die Anfangsmarkierung nicht symmetrisch sein, kann im allgemeinen Fall keine Erreichbarkeit entschieden werden: no conclusion on reachability possible Für den Überdeckbarkeitstest gilt entsprechendes, es kann dann nur eine äquivalente überdeckene Markierung gefunden werden: no conclusion, but equivalent covering marking found.

Sollte eine Markierung erreichbar bzw. überdeckbar sein, dann können Sie sich einen Weg zu dieser Markierung berechnen (backtracking) und eventuell in eine separate Datei mit der Endung .tra schreiben lassen. Falls Sie die Frage exit? verneinen, können Sie sich weitere Wege anzeigen lassen.

Wollen Sie eine weitere Markierung testen, so beantworten Sie die Abfrage once more? mit <Y> , sonst erscheint das Graphanalysemenü auf dem Bildschirm.


CTL-Modelchecking und Prädikatdefinition

Neben der direkten Eingabe von Prädikaten (siehe ab Seite [*] im Kapitel 6.5.2) stehen folgende Prädikatdefinitionsfunktionen zur Verfügung:

<C> convert a set of states to a predicate

Mit diesem Kommando wird für eine Menge von Zuständen ein Prädikat definiert, welches genau von den gegebenen Zuständen erfüllt wird. Zur Auswahl steht ein die Menge aller toten Zustände (beantworten Sie dazu die Abfrage convert the set of all dead states? mit <Y> ), oder ein eine beliebige Menge (antworten Sie dazu mit <N> ) erfüllendes Prädikat. Eine Zustandsmenge wird am state nr-Prompt angefordert, bis Sie <Q> eingeben. Das definierte Prädikat kann in eine Datei mit der Extension .pdc gespeichert werden.

<E> define an enabledness predicate

Mit dieser Funktion wird aus einer einzugebenden Transitionsmenge ein Prädikat definiert, welches durch genau die Zustände erfüllt wird, bei denen mindestens eine Transition aus der Menge Konzession hat:
We define a predicate satisfied by all states which enable at least one
of the transitions to be given.

Eine Transitionsmenge wird am transition nr-Prompt angefordert, bis Sie <Q> eingeben. Das definierte Prädikat kann in eine Datei mit der Extension .pdc gespeichert werden.

Basierend auf (zuvor definierten) Prädikaten können Formeln der Computational Tree Logik (CTL) gecheckt werden (siehe ebenfalls ab Seite [*] im Kapitel 6.5.2):

<F> check a CTL-formula

Mit dieser Funktion können Sie CTL-Formeln checken, d.h. deren Gültigkeit im Anfangszustand ermitteln, und Beweise erstellen lassen.

Am formula input file Prompt können Sie eine .ctl Datei einlesen lassen oder mit <esc> auch direkt eingeben. Bitte verwenden Sie nur mit INA erstellte Formeln (es erscheint folgende Warnung: please, use only formula files created by INA), die Syntax wird bei manueller Eingabe angezeigt:

<formula> ::= 'T' | 'P'<number> | '-'<formula> |
              '('<formula>'&'<formula>')' | '('<formula>'V'<formula>')' |
              'E''X'<formula> | 'E''F'<formula> | 'E''G'<formula> |
              'A''X'<formula> | 'A''F'<formula> | 'A''G'<formula> |
              'E''['<formula>'U'<formula>']' | 'A''['<formula>'U'<formula>']'
              'E''['<formula>'B'<formula>']' | 'A''['<formula>'B'<formula>']'
 <number> ::= <nonempty sequence of digits followed by a blank>

T steht für den Wahrheitswert ,,wahr``, mit P<number> wird auf Prädikate verwiesen, - steht für das logische ,,nicht``, & und V stehen für die logische Konnektoren ,,und`` und ,,oder``, und EX, EF, EG, AX, AF, AG, E U, E B, A U und A B stehen für die entsprechenden temorallogischen Quantoren (siehe Kapitel 6.5.2 ab Seite [*]. Bitte beachten Sie die verschiedenen Klammerungen mit ( ) bzw. [ ], ebenso die Eingabe eines Leerzeichens am Ende einer Prädikatnummer. Bei fehlerhaften Eingaben erscheint eine Liste der erwarteten Zeichen: expected. Fehlende schließende Klammern ergänzt INA selbstständig. Korrekturen sind teilweise unmöglich, geben Sie im Fehlerfall noch alle benötigen Zeichen ein und beantworten die Abfrage ok mit <N> . Größere Formeln können Sie durch Eingabe von <cr> und <space> beliebig formatieren.

Nach der Eingabe von <Y> können Sie die Formel in eine Datei mit der Extension .ctl schreiben. Danach werden die benötigten Prädikate erfragt, deren Nummern Sie in der Formel angegeben haben. Sie können entweder zuvor definierte Prädikate einlesen lassen oder mit <esc> diese auch direkt eingeben.

Falls der Erreichbarkeitsgraph tote oder ,,schlechte`` Zustände enthält oder wegen einer Tiefenbeschränkung oder Speicherplatzproblemen nicht vollständig berechnet wurde, können Sie durch Beantwortung der Abfrage consider the structure as total mit <Y> erreichen, daß an Graphendknoten eine Schleife eingeführt wird. Auf diese Art werden Aussagen über unendliche Pfade gewonnen, selbst wenn der Graph Endknoten enthält. Findet INA Endknoten, ohne daß Sie die Graphstruktur als total vorausgesetzt haben, so kann keine Aussage getroffen werden: No decision because dead graph nodes exist (siehe auch Seite [*] im Kapitel 6.5.2).

Sie können einen Beweis erstellen lassen, der entweder nur Zeugen und Gegenbeispiele (witnesses and counterexamples) oder mehr Informationen enthält. Diesen Beweis könnnen Sie in eine Datei mit der Extension .prf schreiben lassen. In Beweisen finden Sie Formulierungen über erfüllte bzw. nicht erfüllte Prädikate (sat) und eventuell bereits im Pfad enthaltene (is on path) bzw. bereits besuchte (visited) Zustände.

Am Ende einer Prüfung gibt INA eine Antwort, die sich bei symmetrischer bzw. sturer Reduktion und bei Tiefenbeschränkungen selbstverständlich nur auf den berechneten Teilgraphen beziehen kann: The formula is TRUE/FALSE (in the computed subgraph).

Berechnung der Distanzen

<A> compute distances

Mit diesem Kommando können minimale und maximale Distanzen zwischen Knoten des Zustandsgraphen berechnet werden. Die Ausgabe erfolgt in den Session-Report.

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 eingeben, 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.

Berechnung der Kreise

<K> compute circuits

Mit diesem Kommando können Sie Kreise im Zustandsgraphen berechnen und bewerten lassen.

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 oder auf Anforderung in eine Datei mit der Extension .cir 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 x führt. Die Nummern der Zustände beziehen sich auf die zuvor berechnete Zustandsliste.

Ein Beispiel für das Netz 6.2 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.6).

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.

Lebendigkeitstest

<L> check liveness properties

Mit diesem Kommando 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

A transition is weakly live IFF it has a live colour.
zum anderen die kollektive Lebendigkeit
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'.
Siehe dazu auch die Erklärungen von WL und CL auf Seite [*] im Kapitel 6.2.2.

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).

Starke Zusammenhangskomponenten und Rücksetztbarkeit

<V> compute strongly connected components

Mit dieser Funktion werden die starken Zusammenhangskomponenten berechnet und auf Anfrage in eine Datei mit der Extension .res geschrieben.

Ausgegeben wird ein Überblick über die starken Zusammenhangskomponenten des Zustandsgraphen. Die Knoten des Graphen, die in einer der ausgegebenen Komponente liegen, sind jeweils durch gerichtete Wege voneinander erreichbar. Nach der Komponentennummer werden die enthaltenen Zustände aufgelistet. Im Anschluß werden die erreichbaren Komponenten gezeigt (reachable scc's).

Terminale Zusammenhangskomponenten, d.h. Komponenten, aus denen keine Bögen herausführen, werden mit term gekennzeichnet. Tote Zustände bilden immer eine terminale Komponente mit genau einem Zustand.

Für das Netz 2.2 werden drei Komponenten ausgegeben. Die erste Komponente besteht aus insgesamt 391 Zuständen. Erreichbar von dieser ersten Komponente sind zwei weitere Komponenten ( Reachable scc's: 2, 3), die beide terminal und einelementig sind: 2: 322, term und 3: 6, term. Dies sind genau die Komponenten der toten Zustände.

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.

Für Netze unter Zeitbewertung wird gegebenenfalls eine Liste der Time-Deadlocks ausgegeben.

Berechnung dynamischer Konflikte

<Y> check dynamic conflicts

Mit dieser Funktion können Sie INA veranlassen, den Zustandsraum auf in einem dynamischen Konflikt (siehe im Kapitel 6.2.2 auf Seite [*]) stehende Transitionen zu untersuchen. Die

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 werden nur zwei Zeilen ausgegeben: 1: 1.login_Prog1 # 2.login_Prog2 und 1: 1.login_Prog1 # 3.login_Prog3, 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. Für Netze, die unter der Schrittschaltregel betrachtet werden, gilt, daß je zwei in einem Zustand konzessionierte Schritte in Konflikt miteinander stehen. Deshalb ist auch in diesem Fall die Suche nicht möglich, Sie können aber an der Graphmatrix erkennen, welche Schritte im Konflikt miteinander stehen.


Schreibfunktionen

<W> write all computed states

Mit diesem Kommando werden alle berechneten Zustände in den Session-Report oder auf Anforderung in eine Datei mit der Standarderweiterung .sta geschrieben. Durch Eingabe von <esc> können Sie die Ausgabe auf dem Bildschirm umlenken.

Für das Netz 2.1 sieht die vollständige Zustandsliste wie folgt aus:

State nr.    1
P.nr: 0 1 2 3 4 5 6
toks: 2 0 0 0 1 1 1
State nr.    2
P.nr: 0 1 2 3 4 5 6
toks: 0 1 0 0 0 1 1
State nr.    3
P.nr: 0 1 2 3 4 5 6
toks: 1 0 1 0 1 0 1
State nr.    4
P.nr: 0 1 2 3 4 5 6
toks: 0 0 1 1 1 0 0
State nr.    5
P.nr: 0 1 2 3 4 5 6
toks: 1 0 0 1 1 1 0

<X> write all states satisfying a predicate

Nach Eingabe eines Prädikates werden nur die Zustände geschrieben, die dieses Prädikat erfüllen.

<D> write the dead states

Es werden nur die toten Zustände ausgegeben.

<B> write the bad states

Es werden nur die Zustände ausgegeben, bei denen ein (vor der Berechnung eingebenes) ,,bad`` Prädikat erfüllt ist.

<S> write the list of executed steps

Bei der Schaltstrategie maximale Schritte kann eine Schrittliste ausgegeben werden. Alle bei anderen Funktionen angezeigten Übergangsnummern beziehen sich bei dieser Schaltstrategie statt auf Transitionen auf Schritte, aus der ausgebenen Liste sind die in einem Schritt enthaltenen Transitionen ersichtlich.

<T> write a trace to a state

Analog zum Backtracking bei einer Suche nach einer erreichbaren Markierung mit dem Kommando <R> kann mit dieser Funktion ein Weg zu einem berechneten Zustand ausgegeben werden.

<M> write the matrix of the graph

Mit dieser Funktion können Sie eine Matrixdarstellung des Zustandsgraphen in den Session-Report oder eine separate Datei mit der Extension .res ausgegeben lassen. 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 ha.

Für das Netz 2.1 zeigt die Matrix, daß im Zustand 1durch Schalten der Transition 3 der Zustand 5 erreicht wird, die Punkte in der zweiten Zeile, daß nur die Transition 4 Konzession im Zustand 2hat.

State transition matrix:
  | 1 2 3 4 5 6
---------------
 1| 2 3 5 . . .
 2| . . . 1 . .
 3| . . 4 . 1 .
 4| . . . . 5 3
 5| . 4 . . . 1

<P> write the matrix of the transitional periods

Bei Netzen mit Zeitbewertung kann zusätzlich eine Matrix der Zeiten für die Übergänge zwischen den Zuständen ausgegeben werden. Beachten Sie: ein erneutes Schreiben in eine Datei mit der Extension .res zerstört die eventuell zuvor gespeicherte Zustandsübergangsmatrix. Wählen Sie deshalb einen modifizierten Dateinamen oder eine andere Dateiextension.


Dateien anzeigen

<I> inspect a result file

Mit diesem Kommando können Sie sich verschiedene bei der Analyse erstellte Dateien ansehen.
Es erscheint folgendes Untermenü:
     See the session report ......R
     See a proof .................P
     See a circuits list .........C
     See a states list ...........S
     See a trace .................T
     See a result file ...........F
Zur Auswahl steht also mit <R> die Betrachtung von SESSION.ina, mit <P> können Sie eine Beweisdatei (.prf), mit <C> eine Datei mit berechneten Kreisen (.cir), mit <S> eine Zustandsliste (.sta), mit <T> einen Weg zu einem Zustand (.tra) und eine allgemeine Ergebnisdatei (.res) mit <F> anzeigen lassen.


next up previous contents index
Next: 6.6 Invariantenanalyse Up: 6.5 Erreichbarkeitsanalyse Previous: 6.5.3 Pfadberechnung

© 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