6.6.1 Invariantenberechnung

In diesem Abschnitt finden Sie eine Beschreibung des Analysemenükommandos <I> , welches eine Invariantenbasis berechnet und einen schnellen Nichterreichbarkeitstests anbietet. Desweiteren wird die Ausgabe der Inzidenzmatrix und der Invarianten vorgestellt.

In allen Beispielen wird auf das Netz 6.2 zurückgegriffen, das die Steuerung zweier Ampeln modelliert.

Inzidenzmatrix

Bei der Berechnung von P-Invarianten kann die transponierte, bei T-Invarianten die Inzidenzmatrix selbst ausgegeben werden. Die Matrix zeigt, wie die Transitionen und Plätze verbunden sind [Sta90, Definition 11.1 (110)]. Plätze werden in den Zeilen, die Transitionen in den Spalten aufgeführt (für die transponierte Matrix gilt umgekehrtes).

Für das Netz 6.2 sieht die transponierte Inzidenzmatrix wie folgt aus:

Input matrix (transposed incidence matrix):

           1  2  3  4  5  6
~~~~~~~~~~~~~~~~~~~~~~~~~~~
   1 |    -1  0  1  1  0  0
   2 |     0  1 -1 -1  1 -1
   3 |     0 -1  1  1  0  0
   4 |     1  0 -1 -1 -1  1

Der Eintrag -1 in der ersten Spalte der ersten Zeile bedeutet, daß die Transition t₁ vom Platz $\textrm{gr\uml {u}n}_\textrm{\footnotesize eins}$ eine Marke abzieht, der Eintrag 1 der sechsten Spalte der vierten Zeile dagegen, daß das Schalten der Transition t₄ eine Marke auf den Platz $\textrm{rot}_\textrm{\footnotesize zwei}$aufbringt.

Falls in der Matrix Einträge mit 00 statt mit 0 versehen sind, so sind diese Einträge durch die Unreinheit des Netzes entstanden (siehe Seite im Kapitel 6.2.1).

Ausgabeformate

Invarianten können in verschiedenen Formen ausgegeben werden, mit der Option <F> der Invariantenkommandos wird ein Format ausgewählt.

Als Beispiel sehen Sie P-Invarianten des Netzes 6.2.

<T> complete table

Die Basis wird in Form einer Tabelle geschrieben, wobei die Zeilen die Nummern der Invarianten, die Spalten dagegen die Nummern der Plätze bzw. Transitionen sind.

Nr.        1  2  3  4  5  6
~~~~~~~~~~~~~~~~~~~~~~~~~~~
   1 |     1  1  1  0  0  0 +
   2 |     1  1  0  1  0  0 +
   3 |     0  0  0  0  1  1 +

Invarianten, die Sie in diesem Format auf eine separate Datei geschrieben haben, können Sie später mit dem Kommando <T> testen (siehe Seite ). Sie werden deshalb in eine Datei mit der Extension .inv gespeichert. Alle anderen Formate ermöglichen keinen späteren Test und werden deshalb in eine Datei mit der Extension .res geschrieben.

<Z> complete table, zero's not printed

Die Basis wird ebenfalls in Form einer Tabelle geschrieben, aber statt Nullen werden Leerzeichen ausgedruckt.

Nr.        1  2  3  4  5  6
~~~~~~~~~~~~~~~~~~~~~~~~~~~
   1 |     1  1  1          +
   2 |     1  1     1       +
   3 |                 1  1 +

<E> print non-zero entries only

Die Basisvektoren werden als Liste ihrer von Null verschiedenen Komponenten in der Form <Knotennummer> : <Wert> ausgegeben.

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

<#> print non-zero entries with names

Die Basisvektoren werden ebenfalls als Liste ihrer von Null verschiedenen Komponenten ausgegeben, aber mit ihren Namen versehen.

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

Bitte beachten Sie: Semipositive Invarianten werden bei der Ausgabe durch ein + gekennzeichnet (siehe auch Seite ).

Basisberechnung

Die P- bzw. T-Invarianten bilden einen linearen Raum, der gegenüber (komponentenweiser) Addition, Multiplikation mit einer ganzen Zahl und Division durch den größten gemeinsamen Teiler aller Komponenten abgeschlossen ist. Dieser Raum wird durch endlich viele Basisvektoren aufgespannt, enthält aber im allgemeinen unendlich viele Invarianten. Mit dem Kommando <I> wird eine Basis berechnet.

<I> Compute a base for all S/T-invariants

Zuerst können Sie die angezeigten Optionen ändern:

     computation of place-invariants..................................P
     output (transposed) incidence matrix.............................O
     output format = complete table...................................F

Mit der Option <P> wählen Sie zwischen der Berechnung von Platz- und Transitionsinvarianten, mit <O> können Sie bestimmen, ob die (transponierte) Inzidenzmatrix ausgegeben werden soll und mit <F> bestimmen Sie die Form, in der Invarianten ausgegeben werden sollen.

Danach berechnet dieses Kommando eine Basis für den Raum aller Invarianten des gewählten Typs. INA meldet, ob Invarianten gefunden wurden, und zieht eventuell daraus weitere Folgerungen. Das Programm entscheidet, ob das Netz mit Invarianten des gewählten Typs überdeckt ist, d.h. ob eine in allen Komponenten positive Invariante existiert. Falls diese tatsächlich berechnet wurde, wird sie auch ausgegeben.

Falls P-Invarianten gefunden wurden, wird ein schneller Nichterreichbarkeitstest angeboten: Test a marking for non-reachability? Eine Beschreibung dieses Tests finden Sie auf Seite .

Am Ende werden folgende Zeilen auf dem Bildschirm ausgegeben: You may display the results by typing 'F <cr> Y <esc> ' und results by other format (f), exit (e).

Mit <E> kehren Sie ins Analysemenü zurück, mit <F> werden erneut die vier möglichen Ausgabeformate gezeigt. Falls Sie sich die Invarianten auf dem Bildschirm ausgeben lassen möchten, so drücken Sie jetzt einfach <cr> . Beantworten Sie die Frage Open a separate output file mit <Y> und geben danach <esc> ein, so werden die berechneten Invarianten wie gewünscht auf dem Bildschirm ausgegeben. Falls Sie dagegen die Ausgabe in eine separate Datei umleiten wollen, so geben Sie einen Dateinamen ein, die Endung .inv bzw. .res wird automatisch angehängt. Falls gewünscht, kann selbstverständlich auch das Ausgabeformat vorher geändert werden. Die Abfrage eines Nichterreichbarkeitstests erscheint erneut, danach ebenso die eben vorgestellten Zeilen. Falls Sie die Ergebnisse in eine separate Datei geschrieben haben und erneut <F> eingeben, wird zuerst die Frage Close separate output file ? gestellt. Falls Sie mit <Y> antworten, wird die Datei geschlossen und Sie können eine andere Ausgabedatei öffnen, sonst wird die Ausgabe an die bereits geöffnete Datei angehängt.

Beispiel für eine Invarianteninterpretation

Die oben aufgeführte Invariantenbasis für das Netz 6.2 und dessen Anfangsmarkierung besagt, daß

1.

die Summe der Marken der Plätze $\textrm{gr\uml {u}n}_\textrm{\footnotesize eins}$, $\textrm{gr\uml {u}n}_\textrm{\footnotesize zwei}$ und $\textrm{gelb}_\textrm{\footnotesize eins}$ immer gleich eins ist,

2.

die Summe der Marken der Plätze $\textrm{gr\uml {u}n}_\textrm{\footnotesize eins}$, $\textrm{gr\uml {u}n}_\textrm{\footnotesize zwei}$ und $\textrm{gelb}_\textrm{\footnotesize zwei}$ ebenfalls immer gleich eins ist,

3.

die Summe der Marken der Plätze $\textrm{rot}_\textrm{\footnotesize eins}$ und $\textrm{rot}_\textrm{\footnotesize zwei}$ ebenfalls immer gleich eins ist

und somit

• genau eine Ampel rot zeigt,
• genau eine Ampel grün zeigt,
• eine Ampel nur gelb zeigt, wenn keine der beiden Ampeln auf grün geschaltet ist, d.h. eine Ampel zeigt genau dann gelb, wenn die andere Ampel auf rot-gelb geschaltet ist.

Als T-Invariantenbasis ergibt sich $1\cdot t_1, 1\cdot t_2, 1\cdot t_3, 1\cdot t_4$, d.h. wenn alle vier Transitionen geschaltet haben, ist die Anfangsmarkierung wiederhergestellt.

Für das Netz 6.2 können durch die Invariantenanalyse die Eigenschaften CPI, CTI, SB und B gefolgert werden.

Schneller Nichterreichbarkeitstest

Falls die Berechnung von P-Invarianten zu einem Ergebnis geführt hat, wird Ihnen ein schneller Nichterreichbarkeitstest angeboten. Mit den berechneten Invarianten kann INA dies einfach überprüfen, da folgende Gleichung gilt: Für die Anfangsmarkierung m₀, eine Invariante x und eine Markierung mist immer $m_0\cdot x = m\cdot x$, falls m von m₀ erreichbar ist. Für eine angeforderte Markierung wird diese Gleichung für alle berechneten Basisinvarianten getestet, eventuell werden die Nummern der die Gleichung verletzenden P-Invarianten ausgegeben.

Anhand des Netzes 6.2 wird im folgenden ein solcher Nichterreichbarkeitstest gezeigt, der die zuvor berechneten P-Invarianten als Ausgangsbasis benutzt:

Non-reachability test of the marking m:
  p :  1  2  3  4  5  6
-----------------------
m(p):  1  1  .  .  .  .

The marking is not reachable from m0.
invariant nr.  3
invariant nr.  2
invariant nr.  1

Non-reachability test of the marking m:
  p :  1  2  3  4  5  6
-----------------------
m(p):  1  .  .  .  1  .

No conclusions possible.

Non-reachability test of the marking m:
  p :  1  2  3  4  5  6
-----------------------
m(p):  .  .  1  1  .  .

The marking is not reachable from m0.
invariant nr.  3

Wie Sie sehen können, ist der Zustand ,,beide Ampeln zeigen grün`` nicht erreichbar, er verstößt gegen alle drei berechneten P-Invarianten. Weiterhin kann nicht entschieden werden, ob die Markierung ,,Ampel 1 zeigt gleichzeitig grün und rot`` nicht erreicht werden kann. Die Markierung ,,beide Ampeln zeigen gelb`` verstößt gegen die Invariante mit der Nummer drei, die besagt, daß genau eine Ampel rot zeigen muß, und ist deshalb nicht erreichbar.