Figure 7 presents the selection of qualitative
analysis algorithms implemented in *QPN-Tool*. Apart from `classical'
algorithms like reachability graph analysis and calculation of P- and
T-invariants, rather new algorithms for special net classes are
offered. Qualitative analysis within *QPN-Tool * aims at liveness and
boundedness. If the QPN does not have these properties, information of
the employed algorithm is extracted in order to demonstrate the reason
for a QPN being unbounded or not live. All implemented qualitative
analysis algorithms are based on Petri net theory and ignore timing
aspects as firing delays and frequencies and interpret timed places
as ordinary places. Properties of this `untimed' QPN carry over to the
timed QPN under certain circumstances, if conditions Equal-conflict
and Station are satisfied (cf. [3]). Condition
Equal-conflict demands that only transitions of the same kind, either
timed or immediate, are in conflict and condition Station states that
the scheduling strategy has to be of a type like PS or IS. If the QPN is
live, bounded and unveils an extended free choice net-structure these
conditions are sufficient for the existence of the steady-state
distribution.

The choice of algorithms contain:

- reachability graph analysis
- The algorithm generates the reachability graph and recognises firing sequences of transitions which lead to unbounded markings. The reachability graph is checked and it is determined whether the net is bounded and live. If this is not the case a firing sequence is presented which demonstrates unboundedness or non-liveness.
- computation of P- or T-invariants
- A system of 'base vectors' for all positive P- and T-invariants is computed.
- cover of P- or T-invariants
- The algorithm checks whether the net can be covered by positive P- or T-invariant. If not, the set of uncovered places, resp. transitions is presented.
- deadlock/trap condition
- For the class of simple nets it is possible to ensure liveness by checking the deadlock/trap condition. The algorithm is taken from [16] and generates the set of minimal deadlocks and checks if any minimal deadlock contains a marked trap.
- check state-machine-decomposability
- The algorithm is taken from
[14][13]. It allows to recognise live and bounded Free-Choice nets
by checking the net structure. This is highly efficient compared to
other analysis algorithms.

Tue Jan 9 09:20:20 MET 1996