6.4.2 Fast non-reachability test

In the analysis menu, a fast non-reachability test for partial markings can be executed. This test exists alongside the non-reachability test when computing invariants (see on page in chapter 6.6.1), and the reachability tests, which are based on a (partial) construction of the reachability graph (see on page ff in chapter 6.5).

<N> Non-reachability test of a partial marking using the state equation

This function can decide the non-reachability of a marking using the state equation. A partial marking is sufficient here: the marking of the remaining places is considered to be not defined, i.e. dealt with by means of don't care conditions (see also page in chapter 6.5.3).

INA determines whether the state equation $C\cdot x = m - m_0$, is solvable, where C is the transposed incidence matrix of the net, m₀ the initial marking, and m the parametrized partial marking. For this purpose, the solvability of an associated auxiliary problem is considered. If it is not solvable, the non-reachability can be deduced. During the computation, a counter named eliminated columns is running. If, however, the state equation is solvable, a solution is displayed - as far as non-reachability is concerned, no decision can be made.

Figure 6.1: A net in which one place is not markable (stateeq.pnt)

For the net 6.1, it is clear that the place five is not markable, but with the non-reachability test by invariants, this decision cannot be made:

place invariants basis
=================
   1 |     1: 1,  2: 1,  3: -1,  4: -1
   2 |     1: 1,  2: 1,  5: 1 +

At least the following places are covered by semipositive invariants:
       1,  2,  5

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

No conclusions possible.

Using the state equation, on the other hand, the non-reachability can be proved:

Testing non-reachability of a partial marking

target submarking:
   5:1;

The marking is not reachable.

For the net above, no statement about the (non-)markability of place two can be made by means of the state equation, since the latter is solvable:

Testing non-reachability of a partial marking
target submarking:
   2:1;
The state equation is solvable:
t2: 1    t4: 1