6.3 Analysemenü und Voranalyse

Im Analysemenü werden in Abhängigkeit vom Netztyp unterschiedliche Analyseprozeduren angeboten. Nicht für jeden Netztyp sind alle Verfahren bereits theoretisch begründet bzw. überhaupt sinnvoll. Netze unter Zeitbewertung sind z.B. mit der TURING-MASCHINE gleichwertig, was die Existenz von Algorithmen zur Entscheidung z.B. der Beschränkheit ausschließt. Es werden für jeden Netztyp nur die Verfahren angeboten, die zu Aussagen über die wichtigen dynamischen Eigenschaften führen können. Die Rückkehr ins Hauptmenü erfolgt durch <Q> .

Analysis menue:
Decide structural boundedness...............................................B
Non-reachability test of a partial marking using the state equation.........N
Compute the symmetries of the net...........................................Y

Compute a shortest path from the initial state to a target marking..........P
Compute a minimal path from the initial state to satisfy a predicate........O
Compute a reachability graph................................................R
Compute a coverability graph to decide boundedness and coverability.........G

Compute a base for all S/T-invariants [non-reachability test]...............I
Compute a base for all semipositive S/T-[sub/sur]-invariants................S
Format lines written to INVARI.HLP earlier..................................F
Test place- or transition-vectors for invariant properties..................T

Check the deadlock-trap-, SMD-, SMA-properties [boundedness, liveness]......D
Compute all components [check SMD-,SMA-properties]..........................C
Decide state-machine coverability [for boundedness].........................M

choice >

Voranalyse

Bevor das Analysemenü angezeigt wird, führt INA eine Voranalyse des Netzes durch. Dabei wird auch geprüft, welche Funktionen überhaupt verfügbar sind.

Untersucht werden strukturelle Eigenschaften (siehe Seite bis ). Zu Beginn können Sie Schreiboptionenen setzen. Dazu gehört unter anderem die Ausgabe der statischen Konflikte: Print the static conflicts? Mit <Y> werden diese ausgegeben.

Beispiel

Für das Netz 2.1 der drei Programmierer, die sich zwei Terminals teilen, ergibt die Voranalyse folgende Ergebnisse:

Information on elementary structural properties:
The net is not statically conflict-free.
The net is pure.
The net is not ordinary.
The net is not conservative.
The net is not subconservative.
The net is not a state machine.
The net is not free choice.
The net is not extended free choice.
The net is extended simple.
The net is not safe.
The net is not live and safe.
The net is marked.
The net is not marked with exactly one token.
The net is not a marked graph.
The net is not homogenous.
The net has not a non-blocking multiplicity.
The net has no nonempty clean trap.
The net has no transitions without pre-place.
The net has no transitions without post-place.
The net has no places without pre-transition.
The net has no places without post-transition.
Maximal in/out-degree:  3
The net is connected.
The net is strongly connected.

INA kann daraus schon einige Eigenschaften folgern:

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

Die statischen Konflikte des Netzes sind:

Static conflicts:
transition 1.login_Prog1 is in conflict with:
       2.login_Prog2,  3.login_Prog3,
transition 2.login_Prog2 is in conflict with:
       1.login_Prog1,  3.login_Prog3,
transition 3.login_Prog3 is in conflict with:
       1.login_Prog1,  2.login_Prog2,