In diesem Abschnitt finden Sie eine Beschreibung der Berechnung eines Zustands- bzw. Überdeckbarkeitsgraphen, beginnend mit einer Vorstellung der Optionen, über den allgemeinen Ablauf bis zur Form der Ergebnisausgabe. Am Ende finden Sie eine Beschreibung des optionalen Tests auf Erreichbarkeit bzw. Überdeckbarkeit einer Markierung.
INA bietet folgende Funktionen zur Graphberechnung an:
Dieses Kommando baut den Zustandsgraphen auf, wobei dieser symmetrisch bzw. stur reduziert berechnet werden kann. Im Anschluß kann optional ein Test auf Erreichbarkeit bzw. Überdeckbarkeit einer Markierung durchgeführt werden.
Dieses Kommando baut den Überdeckbarkeitsgraphen auf, wobei dieser symmetrisch reduziert bzw. nach FINKELS Methode berechnet werden kann. Im Anschluß kann optional ein Test auf Erreichbarkeit bzw. Überdeckbarkeit einer Markierung durchgeführt werden.
Alle Graphberechnungen erstellen die Datei STATES.gra,
die als Schnittstelle für die weitere Analyse (siehe Kapitel
6.4.4 ab Seite 
) dient. In
dieser Datei wird die Information über die Struktur des Graphen abgelegt.
Einige Folgerungen werden unmittelbar im Anschluß an die Berechnung der
Zustände gezogen.
INA zeigt zu Beginn der Berechnung die Optionen an, unter denen
diese durchgeführt werden soll:
Current analysis options are:
no depth restriction ............................................D
transition names not to be written ..............................W
place names not to be written ...................................V
do not print all states .........................................M
print the dead states............................................O
print the bad states.............................................B
to the session file .............................................S
no reachability / coverability test .............................T
Sie können folgende Einstellungen vornehmen:
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.4.2.
Mit <R> können Sie für Überdeckbarkeitsgraphen zusätzlich eine Reduktion nach der Methode von FINKEL auswählen.
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.
Sie können mit <W> , <V> , <C> und <V> angeben, ob die Platz- bzw. Transitionsnamen (und Farben bei gefärbten Netzen) bei der Ergebnisausgabe aufgeführt werden sollen oder nicht.
Durch Ändern der Option <M> kann festgelegt werden, ob nur tote ( <O> ) und ,,schlechte`` ( <B> ) oder alle Zustände ausgegeben werden, durch <S> , in welche Datei dies geschehen soll: Zur Auswahl steht der Session-Report und eine separate Datei mit der Endung .res, die angefordert wird, sobald die Liste der Zustände berechnet wurde.
Durch setzen der Option <T> kann im Anschluß an die Berechnung auf Grund des aufgebauten Graphen eine Markierung auf Erreichbarkeit oder Überdeckbarkeit getestet werden (siehe dazu die folgende Beschreibung).
Nach dem Einstellen der Optionen wird der Graph aufgebaut. Der laufende Fortschritt wird durch die Anzahl der erzeugten Zustände angezeigt. Die Datei STATES.gra wird während der Berechnung des Graphen geschrieben und dient zur späteren Analyse.
Die laufende 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.
Falls Sie eine symmetrische Reduktion angefordert haben und zuvor die Symmetrien nicht vollständig berechnet wurden (symmetries have not been computed completely), weil Sie die Berechnung unterbrochen haben oder der Speicherplatz nicht ausgereicht hat, müssen Sie den weiteren Fortlauf bestätigen: Execute nevertheless?
Bei der Berechnung des Überdeckbarkeitsgraphen wird im unbeschränkten Fall
nicht abgebrochen, sondern die Markierung an den entspechenden
Stellen oo ( 
) 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 ( -- 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.
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. Die Ausgabe der Zustandsliste ist verkürzt, die Datei STATES.gra wird aber analog zu allen anderen Graphberechnungsalgorithmen aufgebaut.
Sollten Sie eingestellt haben, daß die Zustände in eine separate Datei gespeichert werden sollen, so wird am Ende einer Graphberechnung ein state output file mit der Standarderweiterung .res angefordert. Durch Eingabe von <esc> können Sie dies umgehen, die Informationen der Berechnung werden auf dem Bildschirm angezeigt.
Als erstes wird Ihnen ein Überblick über die benutzen Kapazitäten gegeben: Für jeden Platz wird angezeigt, wieviele Marken auf ihm während der Berechnung maximal gelegen haben. Bei unvollständiger Zustandsberechnung sind entsprechend nur die bis dahin berechneten Markierungen berücksichtigt (capacities needed so far).
In
der Ausgabe (entweder im Session-Report, der separaten Datei oder
auf dem Bildschirm) wird jedem Zustand eine laufende Nummer zugeordnet
(die Reihenfolge entspricht der Berechnung). Ausgehend vom Zustand 1, dem
Anfangszustand (initial), wird für jeden Zustand
angezeigt, aus welchem Zustand er durch Schalten welcher Transition
entstanden ist und wie die Markierung in diesem Zustand aussieht.
Eine Beschreibung der Zustandsdarstellung finden Sie im Kapitel
4.2 ab Seite .
Für das Netz 2.1 sieht die Zustandsliste wie folgt aus:
State nr: 1 initial
PL: 0 1 2 3 4 5 6
MA: 2 0 0 0 1 1 1
State nr: 2 generated from 1 by 1
PL: 0 1 2 3 4 5 6
MA: 0 1 0 0 0 1 1
State nr: 3 generated from 1 by 2
PL: 0 1 2 3 4 5 6
MA: 1 0 1 0 1 0 1
State nr: 4 generated from 3 by 3
PL: 0 1 2 3 4 5 6
MA: 0 0 1 1 1 0 0
State nr: 5 generated from 4 by 5
PL: 0 1 2 3 4 5 6
MA: 1 0 0 1 1 1 0
Im Beispiel bedeutet generated from 4 by 5, daß Zustand 5 aus Zustand 4 durch Schalten der Transition 5 entstanden ist.
Bei der Schaltstrategie maximale Schritte wird zuerst eine Schrittliste ausgegeben, statt Transitionsnummern werden dann Schrittnummern als Übergänge ausgegeben.
Falls Sie die entsprechende Option gesetzt haben, können Sie direkt nach der Berechnung der Zustände Erreichbarkeits- bzw. Überdeckbarkeitstests durchführen und (nicht notwendig kürzeste) Wege von der Anfangsmarkierung zu einer Zielmarkierung abfragen. Sollte zu diesem Zeitpunkt schon der Speicher übergelaufen sein, so bricht INA die weitere Untersuchung mit no space for reachability test ab.
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 und eventuell in eine separate Datei 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 Analysemenü auf dem Bildschirm.
Zuletzt geändert am: Thu Apr 10 15:08:18 MET DST 1997