6.6.1 Computing invariants

In this subsection, you find a description of the command <I> of the analysis menu, which computes a basis of the invariants space, and offers a fast non-reachability test. Furthermore, the outputting of the incidence matrix and the invariants is described.

Subsections

• Incidence matrix
• Output formats
• <T> complete table
• <Z> complete table, zero's not printed
• <E> print non-zero entries only
• <#> print non-zero entries with names
• Computation of a basis
• <I> Compute a basis for all P/T-invariants
• Example of an invariant interpretation
• Fast non-reachability test

In all examples, reference is made to the net 6.2, which models the controlling of two traffic lights.

Incidence matrix

When computing P-invariants, the transposed incidence matrix, and for T-invariants, the incidence matrix itself can be displayed. The matrix describes how transitions and places are linked [Sta90, Definition 11.1 (110)]. Places are listed in the rows, transitions in the columns (vice versa for the transposed matrix).

For the net 6.2, the transposed incidence matrix is as follows:

Input matrix (transposed incidence matrix):

           1  2  3  4  5  6
~~~~~~~~~~~~~~~~~~~~~~~~~~~
   1 |    -1  0  1  1  0  0
   2 |     0  1 -1 -1  1 -1
   3 |     0 -1  1  1  0  0
   4 |     1  0 -1 -1 -1  1

The entry -1 in the first column of the first row means that the transition t₁ subtracts a token from place $\textrm{green}_\textrm{\footnotesize one}$. The entry 1 in the sixth column of the fourth row means, on the other hand, that firing the transition t₄ adds a token onto place $\textrm{red}_\textrm{\footnotesize two}$.

If entries in the matrix are written as 00 instead of 0, these entries result from the impurity of the net (see page in chapter 6.2.1).

Output formats

Invariants can be displayed in different forms; you can select a format with the option <F> of the invariant commands.

As an example, you see P-invariants of the net 6.2.

<T> complete table

The basis is written in the form of a table where the rows are the numbers of the invariants, and the columns are the numbers of the places or transitions.

Nr.        1  2  3  4  5  6
~~~~~~~~~~~~~~~~~~~~~~~~~~~
   1 |     1  1  1  0  0  0 +
   2 |     1  1  0  1  0  0 +
   3 |     0  0  0  0  1  1 +

Invariants which you have written into a separate file using this format can be tested later with the command <T> (see page ). They are therefore saved in a file with the extension .inv. All other formats do not allow such a test, and are therefore written into a file with the extension .res

<Z> complete table, zero's not printed

The basis is likewise written in the form of a table; however, instead of zero's, blanks are printed.

Nr.        1  2  3  4  5  6
~~~~~~~~~~~~~~~~~~~~~~~~~~~
   1 |     1  1  1          +
   2 |     1  1     1       +
   3 |                 1  1 +

<E> print non-zero entries only

The basis vectors are displayed as a list of their non-zero components in the form <node number> : <value> .

   1 |     1: 1,  2: 1,  3: 1 +
   2 |     1: 1,  2: 1,  4: 1 +
   3 |     5: 1,  6: 1 +

<#> print non-zero entries with names

The basis vectors are likewise displayed as a list of their non-zero components, but with the names of the components included.

   1 |     1.gruen_eins      : 1,
     |     2.gruen_zwei      : 1,
     |     3.gelb_eins       : 1 +
   2 |     1.gruen_eins      : 1,
     |     2.gruen_zwei      : 1,
     |     4.gelb_zwei       : 1 +
   3 |     5.rot_eins        : 1,
     |     6.rot_zwei        : 1 +

Please note: semipositive invariants are denoted by a + when displayed (see also page ).

Computation of a basis

The P-(or T-)invariants form a linear space, closed under (componentwise) addition, scalar multiplication by integers, and division by the greatest commom divisor of all components. This space is spanned by a finite number of basis vectors, yet in general contains an infinite number of invariants. With the command <I> , a basis is computed.

<I> Compute a basis for all P/T-invariants

First, you can change the displayed options:

     computation of place-invariants..................................P
     output (transposed) incidence matrix.............................O
     output format = complete table...................................F

With the option <P> , you choose between computing place or transition invariants. With <O> , you can determine whether the (transposed) incidence matrix should be displayed, and with <F> , you determine the form in which the invariants are to be displayed.

Afterwards, this command computes a basis for the space of all invariants of the selected type. INA states whether invariants were found, and possibly derives further deductions from it. The program decides whether the net is covered by invariants of the selected type, i.e., whether an invariant exists which is positive in all components. If such an invariant was actually computed, it will be displayed as well.

If P-invariants were found, a fast non-reachability test is offered: Test a marking for non-reachability? A description of this test can be found on page .

At the end, the following lines are displayed on the screen: You may display the results by typing 'F <cr> Y <esc> ' and results by other format (f), exit (e).

With <E> , you return to the analysis menu, and with <F> , the four possible display formats are shown again. If you would like to have the invariants displayed on the screen, simply press <cr> now. If you answer the question Open a separate output file with <Y> and then press <esc> , the computed invariants are displayed on the screen, as desired. If, however, you want to direct the results into a separate file, then enter a file name; the extension .inv or .res is automatically appended. If desired, the display format can also be changed beforehand, of course. The question about a non-reachability test appears again, as well as the lines described above. If you wrote the results in a separate file and then enter <F> again, INA first asks Close separate output file ?. If you answer <Y> , the file is closed and you can enter another output file. Otherwise, the results are appended to the file already open.

Example of an invariant interpretation

The invariant basis listed above for the net 6.2 and its initial marking states that:

1.

the sum of the number of tokens on the places $\textrm{green}_\textrm{\footnotesize one}$, $\textrm{green}_\textrm{\footnotesize two}$, and $\textrm{yellow}_\textrm{\footnotesize one}$ is always equal to one;

2.

the sum of the number of tokens on the places $\textrm{green}_\textrm{\footnotesize one}$, $\textrm{green}_\textrm{\footnotesize two}$, and $\textrm{yellow}_\textrm{\footnotesize two}$ is also always equal to one;

3.

the sum of the number of tokens on the places $\textrm{red}_\textrm{\footnotesize one}$ and $\textrm{red}_\textrm{\footnotesize two}$ is also always equal to one.

and therefore

• exactly one traffic light indicates red,
• at most one traffic light indicates green,
• one traffic light is yellow, if and only if the other one is red-yellow.

For the T-invariant basis, we obtain $1\cdot t_1, 1\cdot t_2, 1\cdot t_3, 1\cdot t_4$, i.e., when all four transitions have fired, the initial marking is reset.

For the net 6.2, the properties CPI, CTI, SB, and B can be deduced from the invariant analysis.

Fast non-reachability test

If the computation of P-invariants has led to a result, a fast non-reachability test is offered. With the computed invariants, INA can easily check this, because of the following equation: For the initial marking m₀, an invariant x, and a marking m reachable from m₀, it always holds that $m_0\cdot x = m\cdot x$. For a specified marking, this equation is tested with all basis invariants computed, and, if existent, the numbers of the P-invariants which do not satisfy the equation are displayed.

Within the context of net 6.2, such a non-reachability is shown in the following, based on the previously computed P-invariants:

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

The marking is not reachable from m0.
invariant nr.  3
invariant nr.  2
invariant nr.  1

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

No conclusions possible.

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

The marking is not reachable from m0.
invariant nr.  3

As you can see, the state ``both traffic lights are green'' is not reachable. It violates all three P-invariants computed. Furthermore, it can not be decided whether the marking ``traffic light 1 is simultaneously green and red'' is reachable. The marking ``both traffic lights are yellow'' violates the invariant number three, which states that exactly one traffic light must indicate red; that marking is therefore not reachable.