6.6.2 Semipositive invariants

In this subsection, you find a description of the computation of a basis of semipositive invariants using the analysis command <S> , and the formatting of the computed basis using <F> . Please note the remarks on the complexity, and the output formats additionally available.

Subsections

• Semipositive (sub/sur)-invariants
• Notes on complexity
• Interactive computation
• Output formats
• <S> print supports
• <N> print supports with names
• Basis computation for semipositive (sub/sur)-invariants
• <S> Compute a basis for all semipositive P/T-[sub/sur]-invariants
• Formatting invariants
• <F> Format lines written to INVARI.hlp earlier

Semipositive (sub/sur)-invariants

For many applications of invariants, only the semipositive (real) ones [Sta90, Definition 11.3/4 (112,114)] are of interest, i.e., those which are $\geq 0$ in all components. For example, a place is bounded iff its weight is positive (i.e. >0) in some semipositive P-invariant [Sta90, Satz 11.9.1 (116)].

In addition to semipositive invariants, semipositive sub- or sur-invariants can also be computed: For example, a vector y is a semipositive sur-T-invariant if $C\cdot y \geq 0$. A net which possesses a non-trivial (properly semipositive) invariant cannot be bounded for every initial marking (structurally bounded - see chapter 6.2.2), because y is the counting vector of a word which, when being fired, creates a marking $m'=m+C\cdot y$ (out of a marking m), which is greater than m.

Notes on complexity

The problem of computing a basis or a generating system for the semi-space of all semipositive invariants is substantially more complex as the problem of determining a basis for all invariants. There exist nets which possess an exponential number of minimal invariants. For that reason, it is recommendable - even if you are only interested in semipositive invariants - to compute a basis for all invariants with <I> , first. When outputted, the semipositive invariants in the basis are marked with +. Under certain circumstances, the semipositive invariants found in this way are already sufficient to draw the intended conclusions.

Interactive computation

Because of the complexity of the problem, it is in many cases impossible for INA to compute a complete generating system in a reasonable time and with the memory available. In the ``interactive'' mode, you can direct the the computation process by entering the next column to be worked on, and thus obtain partial solutions. Should you be interested in specific places in computing P-invariants, you can achieve this by preferring the numbers of the pre- and post- transitions of these places. In this way, you may obtain at least a part of the place invariants related to these places, before you cancel the computation with <Q> for reasons of time.

Output formats

Also for the output of semipositive invariants, different formats are available. In addition to the formats already introduced in 6.6.1, these are the following (as example, P-invariants of the net 6.2 again):

<S> print supports

This format displays the invariants in the form of their support, i.e. by the numbers of the positive components of the vector [Sta90, Definition 11.5 (119)].

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

<N> print supports with names

The invariants are likewise displayed by their support, but with the names of the components included.

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

Basis computation for semipositive (sub/sur)-invariants

This command computes the unformatted invariant basis.

<S> Compute a basis for all semipositive P/T-[sub/sur]-invariants

First, you can change the displayed options:

     computation of place-invariants..................................P
     no computation of subinvariants..................................B
     no computation of surinvariants..................................R
     covered sub/surinvariants not to be deleted......................D
     run automatically................................................I
     output format = complete table...................................F

With the option <P> , you choose between the computation of place or transition invariants; with <I> , you opt for the interactive or the automatic mode, and with <F> , you again determine the form in which invariants should be displayed. Additionally, you can determine whether sub- or sur-invariants should be computed by entering <B> or <R> , respectively. They cannot both be selected at the same time. With the option <D> , you can further decide whether covered sur-/sub-invariants should be deleted.

After setting the options, the computation starts. In the interactive mode, you obtain an overview of the positive and negative entries in the columns of the current matrix and of the alteration to be expected. When computing T-invariants, the columns correspond to the places, whereas for P-invariants, they correspond to the transitions. INA awaits the entering of a column number. With <P> or <cr> , the proposed column can be (proposal for next to process) selected, with <A> , INA can be switched into the automatic mode, and with <Q> , the computation can be interrupted. In the automatic mode, you can return to the interactive mode at any time by pressing <I> .

The computed invariants, which in general do not form a minimal system, are automatically written into the file INVARI.hlp. It is assumed that sufficient memory space is available on the output medium.

The computation of a minimal generating system and the formatting of the invariants is performed with the function <F> which is executed automatically after finishing the computation. The description of the invariants computation is therefore continued in the next part.

Formatting invariants

This procedure is used to format the output, in particular, it reduces the system of vectors previously computed with <S> .

<F> Format lines written to INVARI.hlp earlier

This procedure has to be executed using the same options as in the creation of the file INVARI.hlp. INA automatically opens and reads this file; initial reduction options are automatically set according to the type of vectors.

At the beginning, INA asks if a certain number of vectors should be skipped: skip a certain number of lines?. This can be useful, if the file contains more vectors than can be loaded into the internal memory. In this case, the formatting can be performed sectionwise. After entering <Y> , you can determine the number of lines to be skipped.

If the file INVARI.hlp does not exist, INA returns not found and requests a file with the extension .hlp: lines input file. This file can be a INVARI.hlp file that you have renamed, and which contains the unformatted invariants of the current net. You cannot enter this file directly at the terminal.

Should the opened file not correspond to the current net, INA states: INVARI.hlp and current net do not match. In this case, INA returns to the analysis menu. The same happens, if the opened file is not an invariant file at all: wrong file.

You can set the following options for formatting:

     Delete repeated occurrences of the same support.................O
     Do not delete covered sub/sur/invariants........................C
     Delete strict invariants covering sub/sur/invariants............I
     Reset to default reductions.....................................R

When opening the file, options are preset in such a way as to ensure that no information gets lost. INA therefore warns NOTE that information may be lost by non-default reductions. With <R> , you can restore the default settings. With <O> , you can determine whether or not repeated occurences of the same support should be deleted. With <C> , you decide on the deletion of covered sur-/sub-/invariants, and with <I> , you decide whether to delete strict invariants which cover sur-/sub-/invariants.

After setting the options, INA demonstrates the continuation of the formatting by counting the lines read: reading line. If a certain number of lines should be skipped, then these are not counted. By pressing <Q> , you can cancel the reading process at any time.

After possible warnings such as results may be incomplete or covered solutions may be lost (option "c"), first deductions are made, and the results are written into the session report: writing solutions. Again, you can cancel writing with <Q> . Thereafter, the following line reappears: results by other format (f) or exit (e). If you enter <E> , INA returns to the analysis menu; with <F> , you can format again using other options or change the output format. You can also determine an output file or, by pressing <esc> , redirect the output onto the screen. Vectors written into an .inv file using the complete table format, can later be tested with <T> (see page and ).