Neben semipositiven Invarianten können auch semipositive Sub- bzw. Sur-Invarianten berechnet werden: Beispielsweise ist ein Vektor y eine semipositive Sur-T-Invariante, wenn . 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 erzeugt, die größer als m ist.
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
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
Dieses Kommando berechnet die unformatierte Invariantenbasis.
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...................................FMit 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.
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:
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.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.....................................RNach 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 ).
© 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