After inquiring whether P- or T-invariants should be tested, INA computes the (transposed) incidence matrix of the net. The following menu subsequently appears:Please, select a sequence of functions (files: o, o1, o2, o3, o4, c, c1, c2) (read/write: r, r1, w, k) (results: p, b, b1, q, q1) (special: f, m, s) (exit: e ) --- h for help --- <del> = <?> :You can now enter a sequence of operations ending with <cr> , which INA will then perform. Of course, only a single command can also be executed; you just have to press <cr> after entering the corresponding letters. After succesfully completing its task, INA returns to the menu above. A description of the individual subcommands can be found in the following parts.
Within a sequence of operations, you can repeat the operations so far performed using the subcommand <S> (see page
), and, e.g., thus test several vectors subsequently in the same way.
With this subcommand, you determine the input and output files.The files with the extension .inv, in which invariants, computed with the analysis menu commands <I> or <S> , have been written in the format complete table (see page
When opening a file, a consistency test is executed: INA checks whether the vectors saved in the opened file are consistent with the net in the internal memory. This is achieved by use of the headlines which were written automatically when saving vector files in the format complete table (see page
All information computed is normally written into the session report. By specifying a separate file with the extension .res, you can redirect this output. Of course, you can also direct the output onto the screen by pressing <esc> .
Like <O> , but only the input file is opened.
Like <O> , but only the output file is opened.
This subcommand opens only the input file, and the consistency test is thereby restricted so that only the number of places or transitions is compared with the length of the headlines.
With this subcommand, you can open a file without headlines. Use it, if INA produces related warnings when attempting to open a file with one of the other commands.
With this subcommand, you can close the input and output files by hand.
Like <C> , but only the input file is closed.
Like <C> , but only the output file is closed.
If you opened an input file with a <O> -subcommand before, this subcommand will read a vector from that file; otherwise, you can enter one directly: Please, give a vector. For the terminal entering, two modes exist: jump to next non-zero component with <J> , and sequential mode with <S> . In the sequential mode, INA requests the components of the vector sequentially. In the jump mode, you can first enter a node number, and then the value of the correpsonding component. All components skipped are set to zero; a reset is not possible. The dialogue starts in the sequential mode, and can at any time be continued in the repective other mode by entering <J> or <S> instead of the expected number. With <N> , you can set all remaining components to zero at the end: set remaining components to zero. With <Q> , you can cancel the entering; the vector may then be incomplete.
When reading files with <R> , the current vector is recorded on the screen. With the subcommmand <R> <1> , this protocol remains inactive. When entering components at the terminal, there are no changes.
If you opened an output file with a <O> -subcommand, this subcommand writes a vector. Please note: do not attempt to later reread a vector saved; INA cancels in this case.
With this subcommand, you can write a headline into an opened output file. Use this command once, before you start writing vectors.
With this subcommand, you change the output format of the invariants: the same formats are available that were already described in the sections 6.6.1 and 6.6.2 on pages
As an example for the testing of an invariant, the invariant ``a
traffic light
is yellow, if and only if the other traffic light is red-yellow'',
already
introduced in section 6.6.1 on page
, will be referred to. A corresponding vector
is 0 0 1 -1 1 1; it is tested in the following.
This subcommand checks the just entered (or most recently read) vector, whether it is semipositive, and whether it is invariant, sub-invariant, or sur-invariant. The symbol + stands for yes, - for no.The vector 0 0 1 -1 1 1 has the following properties:
The place vector under test is not semipositive. It has the following properties: place invariant: + place subinvariant: + place surinvariant: +
With this subcommand, the equation results for the vector are displayed.
equation for transition 1. gives result: 0 equation for transition 2. gives result: 0 equation for transition 3. gives result: 0 equation for transition 4. gives result: 0
This subcommand gives an overview of the transitions (in the case of P-vectors) or places (in the case of T-vectors), whose respective equations are not satisfied by the current vector, i.e., do not equal zero.
This subcommand works exactly like the subcommand <B> , except that the details of the computation are displayed in addition.The following example shows part of the output:
equation for transition 4. : place equation * vector sum 1 | 1 * 0 = 0 ==> 0 2 | 0 * 0 = 0 ==> 0 3 | -1 * 1 = -1 ==> -1 4 | -1 * -1 = 1 ==> 0 5 | -1 * 1 = -1 ==> -1 6 | 1 * 1 = 1 ==> 0
With this subcommand, you can display an individual equation. You will be asked for a transition (in the case of P-vectors) or a place (in the case of T-vectors). The corresponding equation is displayed in a similar way to the previous command.
This subcommand displays the (transposed) incidence matrix.
With this subcommand, you can repeat the operations so far performed within a sequence of operations. If <S> is reached in the current sequence, INA asks: Repeat the function sequence?. If you answer with <Y> , the sequence is executed again from the beginning.In this way, you can test several vectors subsequently in the same way: First, open the input and output files with <O> , thereafter enter, as a sequence, <R> , followed by the corresponding test commands, then the repetition command <S> , and finally <C> to close the files. The testing commands are executed on the vectors, which are read one after the other, until you enter <N> . Afterwards, the files are closed.
With this subcommand, you obtain a short overview of all available functions.
This subcommand ends the invariant test. INA returns to the analysis menu. Any open files are closed first.
© 1996-99 Prof. Peter H. Starke (starke@informatik.hu-berlin.de) und Stephan Roch (roch@...)
INA Manual Version 2.2 (last changed 1999-04-19)