6.7 Strukturanalyse

Die Funktionen zur strukturellen Analyse werden nur in den Fällen angeboten, in denen die Petri-Netz-Theorie es gestattet, aus erkannten Strukturen auf dynamische Eigenschaften des Netzes zu schließen. Als Grundvoraussetzung müssen die Optionen wie folgt gesetzt sein: Keine Zeitbewertung, normaler Schaltmodus, keine Prioritäten und Schalten einzelner Transitionen. Weitere Bedingungen für die Verfügbarkeit der Kommandos ergeben sich durch die bereits durchgeführte Voranalyse des aktuellen Netzes.

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

Es hat folgende stark zusammenhängende Komponenten, die Zustandsmaschinen sind:

Abbildung 6.4: Drei stark zusammenhängende Zustandsmaschinen-Komponenten des Netzes 6.2

Die Plätze der Komponenten entsprechen auch den minimalen Deadlocks und den zugehörigen maximalen Fallen, die Deadlock-Falle-Eigenschaft ist also erfüllt.

Das Netz ist nicht zustandsmaschinenauswählbar, da eine Vorplatzauswahl [Sta90, Definition 16.3 (182)] existiert, die keine stark zusammenhängende Zustandsmaschinen-Komponente auswählt. Die oben abgebildeten Komponenten $K_1=\{\textrm{gr\uml {u}n}_\textrm{\footnotesize eins},\textrm{gr\uml {u}n}_\textrm{\footnotesize zwei},\textrm{gelb}_\textrm{\footnotesize eins}\}$, $K_2=\{\textrm{gr\uml {u}n}_\textrm{\footnotesize eins},\textrm{gr\uml {u}n}_\textrm{\footnotesize zwei},\textrm{gelb}_\textrm{\footnotesize zwei}\}$ und $K_3=\{\textrm{rot}_\textrm{\footnotesize eins},\textrm{rot}_\textrm{\footnotesize zwei}\}$haben die Nachtransitionen $T_1=\{t_1,t_2,t_3,t_4\}$, $T_2=\{t_1,t_2,t_3,t_4\}$ bzw. $T_3=\{t_2,t_4\}$. Die Vorplatzauswahl $\alpha$ mit $\alpha(t_1)=\textrm{gr\uml {u}n}_\textrm{\footnotesize eins}$, $\alpha(t_2)=\textrm{gelb}_\textrm{\footnotesize zwei}$, $\alpha(t_3)=\textrm{gr\uml {u}n}_\textrm{\footnotesize zwei}$ und $\alpha(t_4)=\textrm{gelb}_\textrm{\footnotesize eins}$ wählt keine Komponente aus, da $t_2\in T_1$, aber $\alpha(t_2)=\textrm{gelb}_\textrm{\footnotesize zwei}\notin K_1$, $t_4\in T_2$, aber $\alpha(t_4)=\textrm{gelb}_\textrm{\footnotesize eins}\notin K_2$, bzw. $t_2\in T_3$, aber $\alpha(t_2)=\textrm{gelb}_\textrm{\footnotesize zwei}\notin K_3$.

Die verwendeten Begriffe und Abkürzungen können Sie im Index bzw. im Kapitel 6.2 ab Seite nachschlagen.

Den aufgeführten Ausschnitten aus dem Session-Report können Sie neben der eigentlichen Berechnung auch die jeweils gefolgerten Netzeigenschaften entnehmen.

<D> Check the deadlock-trap-, SMD-, SMA-properties

Dieses Kommando entscheidet die Deadlock-Falle-Eigenschaft (DTP), sowie für gewöhnliche Netze, ob das Netz in stark zusammenhängende Zustandsmaschinenkomponenten dekomponierbar (SMD) und ob es Zustandsmaschinen-auswählbar (SMA) ist.

Nach der Abfrage der Schreiboptionen berechnet INA zunächst die Liste der bezüglich Mengeninklusion minimalen Deadlocks. Deadlocks, die bei der Anfangsmarkierung nicht ausreichend markiert sind, werden als sauber (clean) bzw. nicht ausreichend markiert (not sufficiently marked) gemeldet. Die maximale Falle in einem solchen Deadlock kann nicht ausreichend markiert sein, Transitionen, die Vorplätze in diesem Deadlock haben, sind tot.

Anschließend werden die zugehörigen maximalen Fallen berechnet, die Falle mit der Nummer i ist dabei die maximale Falle im Deadlock Nummer i. Auch hier werden Fallen, insbesondere die leere Menge, die keine oder zuwenig Marken haben, als sauber bzw. nicht ausreichend markiert gemeldet.

Falls dies für keine Falle zutrifft, ist die Deadlock-Falle-Eigenschaft erfüllt und deshalb keine tote Markierung erreichbar [Sta90, Satz 15.5 (165)].

Wenn das Netz eine nichtblockierende Vielfachheit (NBM) hat, homogen (HOM) und extended-simple (ES) ist, dann ist es lebendig [Sta90, Satz 15.6 (165)].

Ist eine der Fallen nicht ausreichend markiert, dann ist die Deadlock-Falle-Eigenschaft nicht erfüllt. Für ein extended-free-choice Netz (EFC) folgt daraus die Nichtlebendigkeit [Sta90, Satz 15.10 (173)].

Für gewöhnliche Netze (ORD) berechnet INA anschließend alle minimalen stark zusammenhängenden Zustandsmaschinenkomponenten, daneben weitere minimale Komponenten, um die Eigenschaft Zustandsmaschinendekomponierbarkeit (SMD) zu testen. In diesem Fall ist das Netz strukturell beschränkt (SB). Komponenten, die bei der Anfangsmarkierung sauber sind, werden gemeldet.

Wenn das Netz SMD und zusammenhängend (CON) ist, so prüft INA die Zustandsmaschinenauswählbarkeit (SMA). Wenn diese Eigenschaft nicht gegeben ist, so finden Sie im Session-Report eine Vorplatzauswahl als Liste der Form <transnr> ==> <vorplatznr> , die keine SCSM-Komponente auswählt.

Für das Netz des Beispiels 6.2 ergibt sich folgende Berechnung:

Structural liveness properties of net nr. 14.Zwei_Ampeln     :
processed candidates: 13
There are  3 minimal deadlocks:
-------------------------------
   1: 5.rot_eins, 6.rot_zwei,
   2: 1.gruen_eins, 2.gruen_zwei, 4.gelb_zwei,
   3: 1.gruen_eins, 2.gruen_zwei, 3.gelb_eins,

Corresponding maximal traps:
----------------------------
   1: 5.rot_eins, 6.rot_zwei,
   2: 1.gruen_eins, 2.gruen_zwei, 4.gelb_zwei,
   3: 1.gruen_eins, 2.gruen_zwei, 3.gelb_eins,
The deadlock-trap-property is valid.
The net has no dead reachable states.
The net is live.
The net has no dead transitions at the initial marking.
The net is live, if dead transitions are ignored.

SM-allocatability of net nr.  0:
********************************
Some minimal place sets Q with QF=FQ, but all SCSM's:

   1: 5.rot_eins, 6.rot_zwei, SCSM 
   2: 1.gruen_eins, 2.gruen_zwei, 4.gelb_zwei, SCSM 
   3: 1.gruen_eins, 2.gruen_zwei, 3.gelb_eins, SCSM 
 3 minimal component(s) found.

The net is state-machine decomposable (SMD).
The net is coverable by state-machines (SMC).
The net is covered by semipositive P-invariants.
The net is structurally bounded.
The net is bounded.
The net is covered by semipositive T-invariants.
There are no proper semipositive T-surinvariants.

The net is not state-machine allocatable (SMA).
A pre-place allocation allocating no SCSM:
   1==>   1,   2==>   4,   3==>   2,   4==>   3,
The net is covered by 1-token SCSM's.

ORD HOM NBM PUR CSV SCF CON SC  Ft0 tF0 Fp0 pF0 MG  SM  FC  EFC ES 
 Y   Y   Y   Y   N   N   Y   Y   N   N   N   N   N   N   N   N   Y  
DTP SMC SMD SMA CPI CTI  B  SB  REV DSt BSt DTr DCF  L   LV L&S 
 Y   Y   Y   N   Y   Y   Y   Y   ?   N   N   N   ?   Y   Y   ?

Die Zeile 1==> 1, 2==> 4, 3==> 2, 4==> 3 beschreibt die zu Beginn angegebene Vorplatzauswahl $\alpha$.

Da die Suche der minimalen Deadlocks erheblichen Rechenaufwand bedeutet, können Sie die laufende Berechnung jederzeit mit <Q> unterbrechen.

Eventuell vorher berechnete Symmetrien verkürzen die Suche: Für das Netz 6.2 ergibt sich mit der in 6.5.1 berechneten Symmetriegruppe, daß statt 13 nur noch 7 Kandidaten untersucht werden müssen.

<C> Compute all components

Mit diesem Kommando werden alle Komponenten des aktuellen Netzes berechnet. Als erstes können Sie Schreiboptionen setzen, danach startet die Berechnung. Die Anzahl der schon berechneten Komponenten wird dabei ausgegeben. Für jede Komponente wird getestet, ob sie eine Zustandsmaschine (SM und stark zusammenhängend (SC) ist. Am Ende werden die Eigenschaften SMD und SMA überprüft und entsprechende Folgerungen gezogen.

Für das Netz des Beispiels 6.2 finden Sie im Session-Report folgende Untersuchungsergebnisse:

candidates: 117
 All components of net nr. 14.Zwei_Ampeln     :

   1:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,  5.rot_eins,
       6.rot_zwei,
   2:  5.rot_eins,  6.rot_zwei, SM SC 
   3:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei,  5.rot_eins,  6.rot_zwei,
   4:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei,  6.rot_zwei,
   5:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei, SM SC 
   6:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei,  5.rot_eins,
   7:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  5.rot_eins,  6.rot_zwei,
   8:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  6.rot_zwei,
   9:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins, SM SC 
  10:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  5.rot_eins,
  11:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,  6.rot_zwei,
  12:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,
  13:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,  5.rot_eins,

The net is state-machine decomposable (SMD).
The net is coverable by state-machines (SMC).
The net is covered by semipositive P-invariants.
The net is structurally bounded.
The net is bounded.
There are no proper semipositive T-surinvariants.

The net is not state-machine allocatable (SMA).
A pre-place allocation allocating no SCSM:
   1==>   1,   2==>   4,   3==>   2,   4==>   3,

ORD HOM NBM PUR CSV SCF CON SC  Ft0 tF0 Fp0 pF0 MG  SM  FC  EFC ES 
 Y   Y   Y   Y   N   N   Y   Y   N   N   N   N   N   N   N   N   Y  
DTP SMC SMD SMA CPI CTI  B  SB  REV DSt BSt DTr DCF  L   LV L&S 
 ?   Y   Y   N   Y   ?   Y   Y   ?   ?   N   ?   ?   ?   ?   ?

Da die Berechnung sehr aufwendig ist, kann sie jederzeit mit <Q> abgebrochen werden.

<M> Decide state-machine coverability

Dieses Kommando entscheidet für gewöhnliche Netze, ob sie mit (nicht notwendigerweise stark zusammenhängenden) Komponenten, die Zustandsmaschinen sind, überdeckt werden kann.

Zuerst können Sie wieder Schreiboptionen ändern. Danach berechnet INA alle minimalen Komponenten [Sta90, Definition 16.1 (177)], dabei wird die Anzahl der bereits berechneten Komponenten ausgegeben. Sie können die Untersuchung mit <Q> jederzeit abbrechen.

Alle berechneten Komponenten werden daraufhin untersucht, ob sie Zustandsmaschinen [Sta90, Definition 14.3 (152)] sind. Im Session-Report werden diese als SM gekennzeichnet. Komponenten, die bei der Anfangsmarkierung nicht markiert sind, werden als sauber (clean) gemeldet.

Wenn die Platzmenge des Netzes eine Vereinigung von Platzmengen minimaler Zustandsmaschinen-Komponenten ist, dann ist das Netz SMC und folglich beschränkt [Sta90, Folgerung 16.4].

Für das Netz des Beispiels 6.2 sieht die Ausgabe wie folgt aus:

SM-coverability of net nr. 14.Zwei_Ampeln     :

Minimal place sets Q with QF=FQ:

   1:  5.rot_eins,  6.rot_zwei, SM 
   2:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins, SM 
   3:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei, SM 
 3 minimal component(s) found.

candidates created: 29
The net is coverable by state-machines (SMC).
The net is covered by semipositive P-invariants.
The net is structurally bounded.
The net is bounded.
There are no proper semipositive T-surinvariants.

ORD HOM NBM PUR CSV SCF CON SC  Ft0 tF0 Fp0 pF0 MG  SM  FC  EFC ES 
 Y   Y   Y   Y   N   N   Y   Y   N   N   N   N   N   N   N   N   Y  
DTP SMC SMD SMA CPI CTI  B  SB  REV DSt BSt DTr DCF  L   LV L&S 
 ?   Y   ?   ?   Y   ?   Y   Y   ?   ?   N   ?   ?   ?   ?   ?

Falls das Netz nicht mit Zustandsmaschinen überdeckt werden kann, so finden Sie im Session-Report eine Übersicht der Plätze, die in Zustandsmaschinen-Komponenten liegen und deshalb beschränkt sind.

Wenn INA bereits bekannt ist, daß das Netz mit Zustandsmaschinen überdeckbar ist (the net is known to be state machine coverable), lautet die erste Abfrage: Compute the SM-components? Falls Sie diese Abfrage mit <Y> beantworten, führt INA die Berechnung trotzdem durch.

Auch hier kann jederzeit die Berechnung mit <Q> abgebrochen werden.