6.4.1 Fast boundedness test

In the analysis menu, a fast boundedness test can be executed. This can be useful in order to avoid the search for covering markings during a subsequent graph computation.

<B> Decide structural boundedness

This function decides whether the net is covered by P-subinvariants. If this is the case, it is structurally bounded, i.e. bounded in every initial marking (see also the explanation in chapter 6.6 on page ff, and under SB in chapter 6.2.2 on page ).

INA determines whether the system of equations $C\cdot x \leq 0$, $x \geq 1$ is solvable, where C is the incidence matrix of the net. For this purpose, the solvability of an associated auxiliary problem is considered. If it is solvable, the net is covered with P-subinvariants. During the computation, a counter named eliminated columns is running.

For the net 2.2 of the dining philosophers, the computation yield the following results:

Deciding structural boundedness
The net is structurally bounded.
The net is bounded.
There are no proper semipositive T-surinvariants.
The net is covered by semipositive place sub-invariants.
  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
  1  1  1  1  1  1  1  1  1  1  1  1  1  1  1  2  2  2  2  2

In the last line, information on a covering P-subinvariant is displayed.