next up previous contents index
Next: 6.6.3 Invariantentest Up: 6.6 Invariantenanalyse Previous: 6.6.1 Invariantenberechnung

Unterabschnitte


6.6.2 Semipositive Invarianten

In diesem Abschnitt finden Sie eine Beschreibung der Berechnung einer Basis semipositiver Invarianten mit dem Analysekommando <S> und die Formatierung der berechneten Basis mit <F> . Beachten Sie auch die Bemerkungen zur Komplexität und die zusätzlich zur Verfügung stehenden Ausgabeformate.

Semipositive (Sub/Sur)-Invarianten

Für viele Anwendungen von Invarianten sind nur die semipositiven (echten) [Sta90, Definition 11.3/4 (112,114)], d.h. Invarianten, die in allen Komponenten $\geq 0$ sind, interessant. Ein Platz ist z.B. beschränkt, wenn sein Gewicht in einer semipositiven P-Invariante positiv, d.h. >0 ist [Sta90, Satz 11.9.1 (116)].

Neben semipositiven Invarianten können auch semipositive Sub- bzw. Sur-Invarianten berechnet werden: Beispielsweise ist ein Vektor y eine semipositive Sur-T-Invariante, wenn $C\cdot y \geq 0$. Ein Netz, das eine solche nichttriviale Invariante besitzt, kann nicht bei jeder Anfangsmarkierung beschränkt (strukturell beschränkt - siehe Kapitel 6.2.2) sein, weil y der Zählvektor eines Wortes ist, das beim Schalten aus der Markierung m eine Markierung $m'=m+C\cdot y$ erzeugt, die größer als m ist.


Bemerkungen zur Komplexität

Das Problem, eine Basis oder ein Erzeugendensystem für den Halbraum aller semipositiven Invarianten zu berechnen, ist von wesentlich größerer Komplexität als das Problem, eine Basis für alle Invarianten zu bestimmen. Es gibt Netze, die exponentiell viele minimale Invarianten haben. Daher sei Ihnen empfohlen, auch wenn Sie sich nur für semipositive Invarianten interessieren, zunächst mit <I> eine Basis für alle Invarianten zu berechnen, beim Ausschreiben der Basis werden die semipositiven Invarianten durch ein + gekennzeichnet. Unter Umständen genügen die in dieser Weise gefundenen semipositiven Invarianten bereits, um die beabsichtigten Schlüsse zu ziehen.


Interaktive Berechnung

Aufgrund der Kompliziertheit des Problems wird es INA in vielen Fällen nicht möglich sein, in der zur Verfügung stehenden Zeit und mit dem verfügbaren Speicherplatz ein vollständiges Erzeugendensystem zu berechnen. Im Modus ,,interaktiv`` können Sie den Fortgang der Berechnung durch Angabe der als nächstes zu bearbeitenden Spalte der Matrix steuern und so partielle Lösungen erhalten. Sollten Sie sich bei der Berechnung von P-Invarianten für bestimmte Plätze interessieren, so können Sie dies erreichen, indem Sie die Nummern der Vor- und Nachtransitionen dieser Plätze bevorzugen. Dadurch erhalten Sie unter Umständen wenigstens einen Teil der Platzinvarianten, die diese Plätze berühren, bevor Sie die Untersuchung mit <Q> aus Zeitgründen stoppen.


Ausgabeformate

Auch für die Ausgabe semipositiver Invarianten stehen verschiedene Formate zur Verfügung. Neben den bereits in 6.6.1 vorgestellten Formaten sind dies (als Beispiele wieder P-Invarianten des Netzes 6.2):

<S> print supports

Dieses Format zeigt die Invarianten in Form ihres Supports (Trägers), d.h. über die Nummern der positiven Komponenten des Vektors [Sta90, Definition 11.5 (119)].

  1 |     1,  2,  3
  2 |     1,  2,  4
  3 |     5,  6

<N> print supports with names

Es wird ebenfalls der Support ausgegeben, aber die Komponenten werden mit ihren Namen versehen.

  1 |     1.gruen_eins      ,
    |     2.gruen_zwei      ,
    |     3.gelb_eins       
  2 |     1.gruen_eins      ,
    |     2.gruen_zwei      ,
    |     4.gelb_zwei       
  3 |     5.rot_eins        ,
    |     6.rot_zwei

Basisberechnung semipositiver (Sub/Sur)-Invarianten

Dieses Kommando berechnet die unformatierte Invariantenbasis.

<S> Compute a base for all semipositive S/T-[sub/sur]-invariants

Zuerst können Sie die angezeigten Optionen ändern:
     computation of place-invariants..................................P
     no computation of subinvariants..................................B
     no computation of surinvariants..................................R
     covered sub/surinvariants not to be deleted......................D
     run automatically................................................I
     output format = complete table...................................F

Mit der Option <P> wählen Sie zwischen der Berechnung von Platz- und Transitionsinvarianten, mit <I> wählen Sie den interaktiven bzw. automatischen Modus und mit <F> bestimmen Sie wieder die Form, in der Invarianten ausgegeben werden sollen. Außerdem können Sie durch Eingabe von <B> bzw. <R> bestimmen, ob Sub- bzw. Sur-Invarianten berechnet werden sollen. Beides kann nicht gleichzeitig ausgewählt werden. Mit der Option <D> können Sie weiterhin bestimmen, ob überdeckte Sur-/Sub-Invarianten während der Berechnung gelöscht werden sollen.

Nach der Optionseinstellung beginnt die Berechnung. Im interaktiven Modus erhalten Sie einen Überblick über die positiven und negativen Einträge in den Spalten der aktuellen Matrix und die zu erwartende Änderung. Bei der Berechnung von T-Invarianten entsprechen die Spalten den Plätzen, bei P-Invarianten den Transitionen. INA erwartet die Eingabe einer Spaltennummer. Mit <P> oder <cr> kann die vorgeschlagene Spalte (proposal for next to process) ausgewählt, mit <A> in den automatischen Modus gewechselt und mit <Q> die Berechnung unterbrochen werden. Im automatischen Modus können Sie jederzeit durch Eingabe von <I> in den interaktiven Modus zuruckkehren.

Die berechneten Invarianten, die im allgemeinen kein minimales System bilden, werden automatisch in die Datei INVARI.hlp geschrieben. Auf dem Ausgabemedium muß (besonders unter DOS) ausreichend Speicherplatz zur Verfügung stehen.

Die Berechnung eines minimalen Erzeugendensystems und die Formatierung der Invarianten wird mit der Funktion <F> vorgenommen, die nach dem Ende der Berechnung automatisch von INA gerufen wird. Eine Fortführung der Beschreibung der Invariantenberechnung finden Sie deshalb im nächsten Abschnitt.


Formatierung von Invarianten

Diese Prozedur dient zur Ausgabeaufbereitung, insbesondere reduziert sie das zuvor mit <S> berechnete System von Vektoren.

<F> Format lines written to INVARI.hlp earlier

Der Aufruf muß unter den gleichen Optionen wie die Erzeugung der Datei INVARI.hlp erfolgen. Diese Datei wird von INA automatisch geöffnet und eingelesen, initiale Reduktionsoptionen werden entsprechend der Art der Vektoren automatisch gesetzt.

Zu Beginn fragt INA , ob eine gewisse Zahl von Vektoren in der Datei übergangen werden sollen: skip a certain number of lines? Das kann dann sinnvoll sein, wenn die Datei mehr Vektoren enthält, als in den Speicher passen. In diesem Fall kann die Formatierung abschnittweise vorgenommen werden. Nach der Eingabe von <Y> können Sie die Anzahl der zu übergehenden Zeilen bestimmen.

Falls die Datei INVARI.hlp nicht existiert, meldet INA not found und fordert eine Datei mit der Endung .hlp an: lines input file. Diese Datei kann eine von Ihnen umgenannte Datei INVARI.hlp sein, die die unformatierten Invarianten 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, so meldet INA : INVARI.hlp and actual net do not match. INA kehrt in diesem Fall in das Analysemenü zurück. Gleiches geschieht, wenn die geöffnete Datei überhaupt keine Invariantendatei ist: wrong file.

Folgende Optionen können Sie für die Formatierung setzen:

     Delete repeated occurrences of the same support.................O
     Do not delete covered sub/sur/invariants........................C
     Delete strict invariants covering sub/sur/invariants............I
     Reset to default reductions.....................................R
Beim Öffnen der Datei werden Voreinstellungen gesetzt, die gewährleisten, daß keine Informationen verloren gehen. Als Warnung gibt INA deshalb NOTE that information may be lost by non-default reductions aus, mit <R> können Sie nach Änderungen die Voreinstellung wiederherstellen. Mit <O> können Sie einstellen, ob mehrfache Vorkommen des gleichen Supports gelöscht werden sollen, oder nicht. Mit <C> bestimmen Sie über die Löschung überdeckter Sur-/Sub-/Invarianten, mit <I> über das Löschen von strikten Invarianten, die Sur-/Sub-/Invarianten überdecken.

Nach der Optionseinstellung zeigt INA den Fortgang der Formatierung an, indem die eingelesenen Zeilen gezählt werden: reading line. Falls eine bestimmte Anzahl von Zeilen übergangen werden sollte, so werden diese nicht mitgezählt. Das Einlesen können Sie jederzeit mit <Q> abbrechen.

Nach eventuellen Warnungen, wie z.B. results may be incomplete oder covered solutions may be lost (option "c "), werden einige erste Folgerungen gezogen und die Ergebnisse in den Session-Report geschrieben: writing solutions. Das Schreiben können Sie ebenfalls mit <Q> abbrechen. Danach erscheint wieder folgende Zeile: results by other format (f) or exit (e). Falls Sie <E> eingeben, kehrt INA in das Analysemenü zuruck, mit <F> können Sie die Formatierung mit anderen Optionen erneut durchführen oder das Ausgabeformat ändern. Ebenso können Sie eine Ausgabedatei bestimmen oder die Ausgabe mit <esc> auf den Bildschirm umleiten. Im Format complete table in eine .inv Datei geschriebene Vektoren können später mit <T> getestet werden (siehe Seite [*] und [*]).


next up previous contents index
Next: 6.6.3 Invariantentest Up: 6.6 Invariantenanalyse Previous: 6.6.1 Invariantenberechnung

© 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