For the graph computation, INA offers the following functions:
This command constructs the state graph, which can be computed using symmetrical and/or stubborn reduction. Subsequently, different graph analyses can be executed, CTL-formulae and predicates can be created or checked, and certain results can be written either into separate files or in the session report.
This command constructs the coverability graph, which can be computed using symmetrical reduction and/or according to FINKEL'S method. A further analysis of the coverability graph is not possible.
Current analysis options are:
no symmetrical reduction ........................................Y
no stubborn reduction ...........................................U
no depth restriction ............................................D
do not use a 'bad' predicate ....................................B
The following settings can be made:
![[*]](cross_ref_motif.gif)
in chapter 6.5.1.
For a coverability graph, you can additionally choose a reduction by FINKEL'S method with <R> .
With the option <D> , you can set the depth level to which the state graph is to be computed. By entering depth 0, the depth restriction is cancelled.
).
On entering predicates, see the
description on page
in chapter 6.5.2.
For coverability graphs, the use of such a predicate is not
possible.
.
The progress of the graph computation is visualized by the number of states created.
The computation can be cancelled at any time by entering <Q> . In case the construction of the graph cannot be completed because of memory restrictions, INA cancels with the message Nodeoverflow. The computation of a state graph is interrupted, if INA discovers that the current net is unbounded (and no depth restriction was set). In both cases, the computed graph is not complete: computed graph is not complete.
At the end of the graph computation, an overview of the states and arcs generated, as well as the capacities needed is written into the session report: for each place, it is shown how many tokens where maximally contained in it during the computation. For an incomplete state graph computation, only the computed markings will thus be considered. Thereafter, any dead or ``bad'' states which were found can be outputted (e.g. write the state numbers of the dead states?).
For the net 2.2 of the dining philosophers, the first results look like the following:
States generated: 393
Arcs generated: 1420
Capacities needed:
Place 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
Cap: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
Dead states:
6, 322,
Number of dead states found: 2
The computation of the coverability graph is not cancelled if the net
is unbounded; rather, the marking is set to
oo (
)
at the corresponding places.
At the beginning, INA states the largest amount of tokens allowed
on a bounded place:
It is assumed that all bounded places are 4294836224-bounded.
This constant is dependent on the implementation, and is in any
case smaller
than the internal value of oo (
-- the given value --
corresponds to the one in the UNIX implementation).
If, on the other hand, the net is bounded, the computed graphs are identical. The algorithm of KARP and MILLER then computes the state graph (which, however, cannot be further analyzed; therefore, please use the function <R> in this case).
If you have selected FINKEL'S method for the computation of the coverability graph, then the screen output during the computation is different: INA counts the number of arcs computed, and displays the number of nodes generated only at the end. For a coverability graph, a test for reachability or coverability of a marking can be executed (see the description below). No further analysis of the coverability graph is possible.
Graph analysis menu
Do You want to
quit analysis of the computed graph ................. Q
test the reachability/coverability of a marking ..... R
convert a set of states to a predicate .............. C
define an enabledness predicate ..................... E
check a CTL-formula ................................. F
compute distances ................................... A
compute circuits .................................... K
check liveness properties ........................... L
compute strongly connected components ............... V
check dynamic conflicts ............................. Y
write the computed graph (states and arcs) .......... W
write all arcs ...................................... X
write all states .................................... M
write all states satisfying a predicate ............. P
write the dead states ............................... D
write the bad states ................................ B
write a trace to a state ............................ T
write the list of executed steps .................... S
inspect a result file ................................I
choice>
The individual functions will be explained in the following. With <Q> , you can quit the graph analysis and return to the main menu.
With this function, you can execute reachability or coverability tests, and find (not necessarily minimal) paths from the initial marking to a target marking.
For coverability graphs, this function is selectable as a graph
computation option (by entering <T> , see page
).
INA first requests the number that the marking obtained during the construction of the state graph. By entering <N> , you can, of course, read a marking from a file, or enter it directly. Please note: under time allocation, transient states are not considered.
If the marking is not reachable, INA states this, and offers a coverability test. If this test also fails, the marking is reported as not coverable. Otherwise, a covering marking is displayed. By answering the question next? with <Y> , you can display further covering markings , until INA reports that no more exist: no more covering marking found. Under time allocation, the marking is presented as a component of a state when displayed.
If symmetrical reduction of the graph is selected as an option, you have to take into consideration that the results obtained may be less conclusive; it may happen that only an equivalent marking is found: by symmetry the marking is reachable. If the initial marking is not symmetrical, reachability is, in general, not decidable: no conclusion on reachability possible. For the coverability test, similar considerations apply; then only an equivalent covering marking can be found: no conclusion, but equivalent covering marking found.
Should a marking be reachable or coverable, you can calculate a path
to this marking,
(backtracking)
and, if desired, write it into a separate file with the extension
.tra. If you answer the question exit? negatively, you can
display further paths.
If you want to test another marking, answer the question once more? with <Y> , otherwise the graph analysis menu appears on the screen.
ff in chapter 6.5.2), the following
functions for defining predicates are available:
With this command, a predicate for a set of states is defined which is satisfied exactly by these given states. You can construct the predicate with respect to either the dead states (answer the question convert the set of all dead states? with <Y> ), or a set to be specified (answer with <N> ). In the latter case, states are requested at the state nr-prompt, until you enter <Q> . The predicate defined can be saved in a file with the extension .pdc.
With this function, a predicate is defined based on a transition set to be specified; this predicate is satisfied exactly by those states in which at least one transition of the set is enabled:We define a predicate satisfied by all states which enable at least one of the transitions to be given.Transitions are requested at the transition nr prompt, until you enter <Q> . The predicate defined can be saved in a file with the extension .pdc.
Formulae of the Computational Tree Logic (CTL) can be checked based
on (previoulsy defined) predicates (see page
ff in chapter 6.5.2):
With this function, you can check CTL-formulae, i.e. determine their validity and generate proofs.
First you have to decide, if you want to work in the atomic mode: Use the atomic mode? At the formula input file prompt, you can then read a .ctl file, or, by pressing <esc> , enter a formula directly. Please only use formulae files created by INA ; the syntax is displayed when entering manually:
<formula> ::= 'T' | 'P'<number> | '-'<formula> |
'('<formula>'&'<formula>')' | '('<formula>'V'<formula>')' |
'E''X'<formula> | 'E''F'<formula> | 'E''G'<formula> |
'A''X'<formula> | 'A''F'<formula> | 'A''G'<formula> |
'E''['<formula>'U'<formula>']' | 'A''['<formula>'U'<formula>']'
'E''['<formula>'B'<formula>']' | 'A''['<formula>'B'<formula>']'
<number> ::= <nonempty sequence of digits followed by a blank>
In the atomic mode, 'P'<number> holds iff the place <number> is marked.
T stands for the truth value ``true'', predicates are
referred to with P<number>, in the atomic mode P<number>
denotes the criterion whether the place with the internal number
<number> is marked or not, - stands for the logical ``not'',
& and V stand for the logical connectors
``and'' and ``or'', respectively, and
EX, EF, EG, AX, AF, AG,
E U, E B, A U, and A B stand for the
corresponding temporal-logical quantors (see chapter
6.5.2 on page ff).
Please note the different bracketings with
( ) or
[ ], as well as the entering of a blank
at the end of a predicate number. For faulty entries, a list of
expected symbols appears:
expected.
INA inserts any missing closing bracket automatically.
In some cases, corrections
may be impossible; in case of mistakes, still enter all required symbols,
and answer the question ok with <N> . Larger formulae can be
formatted by using <cr> and <space> .
After entering <Y> , you can write the formula into a file with the extension .ctl. Thereafter, the predicates whose numbers were stated in the formula are requested. You can either read previously defined predicates from a file, or, by pressing <esc> , enter predicates directly. Predicates are not considered in the atomic mode.
If the reachability graph contains dead or ``bad'' states, or if it
was not completely computed due to a depth restriction or
insufficient memory, you can
insert a loop at each leaf of the graph tree by answering the question
consider the structure as total with <Y> .
In this way, statements about infinite paths are obtained, even if the
graph contains end vertices.
Should INA discover end vertices without the graph structure declared total,
then no statements can be made: No decision because dead graph
nodes exist (see also page in chapter 6.5.2).
You can have a proof constructed by INA which contains either only witnesses and counter examples, or yet additional information. You can write this proof into a file with the extension .prf. In proofs you find information on predicates which are satisfied (sat) or not, and on possible states which are already on the path (is on path), or have already been visited.
At the end of a test, INA gives an answer which, for symmetrical and/or stubborn reduction as well as for depth restrictions, is obviously restricted to the subgraph computed: The formula is TRUE/FALSE (in the computed subgraph).
With this command, minimal and maximal distances between nodes of the state graph can be computed. The results are written into the session report.
If you answered the inquiry compute minimal distances with <Y> , the minimal distances of the graph node entered at the source node prompt are computed. The maximal distance found in this way is displayed, as well as a list of non-reachable nodes. All distances from the given node to any other node can be listed following print all the distances. E.g., for the net 2.2, the minimal distance from the initial state to the state 322 (all philosophers have their right fork) is shown to be distance(1,322)=5. The maximal distance from the initial state which has been found is seven: maximal computed distance = 7 to node nr. 33. It is possible that only upper bounds are found.
If you answer the inquiry mentioned above with N, INA computes the maximal distances. At the beginning, the following warning is issued:
Computation of a maximal (loop-free) distance is very hard, if the graph is
not circuit-free. If a graph with circuits is assumed to be circuit-free, then
only a lower bound for the maximal distance is (faster) computed.
If, in a graph which is not circuit-free, you are only interested in a lower bound, then answer the question assume the graph to be circuit-free with <Y> . The computation can otherwise be very expensive, and may not come to a result within a reasonable time. You can enter the numbers of two nodes of the state graph between which the maximal (ciruit-free) distance is to be computed. During the search, the amount of paths currently found is displayed; at any time, the running computation can be aborted with <Q> . At the end, either a lower bound or the maximal distance is displayed as the result, depending on whether the latter was found.
Please note: without time allocation, in both procedures the number of fired transitions (or steps) is counted. With time allocation, you have the possibility, by answering the question count times with <Y> , to consider the time passed meanwhile, instead.
With this command, circuits in the state graph can be computed and evaluated.
At the beginning of the circuit computation, the following options appear:
Work with transition values ..................................V
Print only selected circuits .................................A
Print circuits with minimal length ...........................B
Print circuits with maximal length ...........................C
Print circuits with minimal value ............................D
Print circuits with maximal value ............................E
Print circuits with best efficiency ..........................F
Print circuits with least efficiency .........................G
Print only circuits containing state nr. 0 ...............H
Print not only the first circuit of the selected type ........I
With <A> you can determine whether all circuits should be displayed. If you select this option, the only other option available is <V> . Otherwise, you can display the circuits with minimal or maximal lengths with <B> or <C> , respectively. The length is given by the number of fired transitions (or steps).
With <V> you can request to work with evaluation of transitions. Afterwards, there are further options available: with <D> or <E> you can display circuits with minimal or maximal values, respectively. The value of a circuit is the sum of the values of the transitions in the circuit. The efficiency is defined as the quotient of the value and the length of the circuit. You can select circuits with minimal or maximal efficiency with <F> or <G> , respectively.
With <H> you can select circuits which contain a certain state. By entering the number of a state of the graph, only those circuits which contain this state are displayed. The state O is never contained in the graph, and serves to display all circuits while considering the remaining options.
By selecting <I> , only the first circuit of each selected type is displayed.
After the options have been set, the computation starts. If you have chosen to work with evaluation of transitions, a file with the extension .val is requested at the values input file prompt. By pressing <esc> , you can also enter the transition values directly at the terminal: after entering a transition number, its name is indicated, and the corresponding value (cost) is requested. When you have quit the entering of a number with <Q> , the values of the transitions not yet specified are set to zero. You have the possibility to write the entered values into a file.
The progress of the computation is indicated by a counter of computed circuits. You can, of course, abort the running computation at any time with <Q> .
The circuits are written into the session report, or, upon request, into a file with the extension .cir. Every circuit is outputted in reversed orientation. Nx<-ty-Nz means that the transition with the number y is part of the circuit, and that firing transition y leads from the state z to the state x. The number of the states are referred to the previously computed list of states.
The following is an example for the net 6.2:
Circuit nr. 1:
N1<-t4--N4<-t3--N3<-t2--N2<-t1--N1
Corresponding T-invariant:
TR: 1 2 3 4
: 1 1 1 1
Livelocked transitions: none
Circuit length = 4
The circuit consists of the transitions t1, t2, t3, and t4, and leads from the initial state back to itself.
In addition, the respective transition invariants are displayed. These
invariants correspond to realizable T-invariants (see page
in chapter 6.6).
Furthermore, transitions are displayed which are in a livelock. A transition t is in livelock, if there exists a circuit in the state graph in which t does not fire [Sta90, chapter 12 (123-133)]. The corresponding net can then fire continuously, without the live transition t being fired; t ``starves''. This becomes particularly clear examining the circuits in the reachability graph of the net 2.2 of the dining philosphers, in which there are a lot of transitions which can be in a livelock.
With this command, a liveness analysis can be executed. This works only for completely computed state graphs without stubborn reduction.For nets executed using the maximal step firing rule, the liveness of steps can be investigated: Test liveness of steps?.
If the net contains transitions which are dead in the initial state (see page
removed (considered as facts). The net can be live if all dead transitions are considered as facts; the property LV (Liveness when ignoring dead transitions) is then set accordingly (see also page
Further weaker notions of liveness are explained on the screen, if
necessary:
on the one hand, weak liveness
and on the other hand, collective liveness
A transition is weakly live IFF it has a live colour.
On this see also the
explanations for WL and CL on page
A net is collectively live IFF every transition is collectively live at the
initial state.
A transition t is collectively live IFF for every reachable state m there
exists a colour c of t and a state m' reachable from m such that t has
concession in colour c at m'.
in chapter 6.2.2.
Possibly, transition sets are displayed which are not weakly live, or which are collectively live:
the following transitions are not weakly liveor
the set of collectively live transitions,respectively.
With this function, the strongly connected components are computed, and, upon request, written into a file with the extension .res.
An overview of the strongly connected components in the state graph is displayed. All nodes of the graph which are in the same component are reachable from each other along directed paths. Following the component number, the contained states are listed. Afterwards, the reachable components are shown (reachable scc's).
Terminal connected components, i.e. components from which no arcs are starting, are indicated with term. Dead states always form a terminal component with exactly one state.
For the net 2.2, three components are displayed. The first one consists of a total of 391 states. Two other components are reachable from this first component (Reachable scc's: 2, 3). They are both terminal and singleton components: 2: 322, term and 3: 6, term. These are exactly the components of the dead states.
If the entire graph is strongly connected, the computation has
not been aborted beforehand, and you have not requested stubborn
reduction, then INA is able to deduce that the graph is reversible (see in
chapter 6.2.2 on page ).
For nets under time allocation, a list of time deadlocks is displayed, if necessary.
With this function, you can search the set of reachable states for transitions in dynamic conflict (see in chapter 6.2.2 on page
If, in a given state i, two transitions j and k are in a dynamic conflict,
the following entry is created in the session report:
i : j # k.
For the net 2.1, only two lines are outputted:
1: 1.login_prog1 # 2.login_prog2 and
1: 1.login_prog1 # 3.login_prog3,
i.e. in the initial state, the transitions 1 and 2, and 1 and
3, repectively,
are in a dynamic conflict.
Please note: when using state graph reduction, a computation of dynamic conflicts is not possible. For nets which are analyzed using the step firing rule, each two steps enabled in a state are in conflict with each other. Hence, the search is also impossible in this case. However, examining the graph matrix, you can discover which steps are in conflict with each other.
With this command, the computed graph, i.e. all states and arcs, is written into the session report, or, upon request, into a file with the default extension .gra. By entering <esc> , you can redirect the output to the screen. Furthermore, a selection of states can be defined.See <X> and <M> for an example of the output.
With this command, all computed arcs are written into the session report, or, upon request, into a file with the default extension .res.For the net 2.1, the complete arc list looks like the following:
State nr. 1 ==t1=> s2 ==t2=> s3 ==t3=> s5 State nr. 2 ==t4=> s1 State nr. 3 ==t3=> s4 ==t5=> s1 State nr. 4 ==t5=> s5 ==t6=> s3 State nr. 5
With this command, all computed states are written into the session report, or, upon request, into a file with the default extension .sta.For the net 2.1, the complete state list looks like the following:
State nr. 1 P.nr: 0 1 2 3 4 5 6 toks: 2 0 0 0 1 1 1 State nr. 2 P.nr: 0 1 2 3 4 5 6 toks: 0 1 0 0 0 1 1 State nr. 3 P.nr: 0 1 2 3 4 5 6 toks: 1 0 1 0 1 0 1 State nr. 4 P.nr: 0 1 2 3 4 5 6 toks: 0 0 1 1 1 0 0 State nr. 5 P.nr: 0 1 2 3 4 5 6 toks: 1 0 0 1 1 1 0
Following the entering of a predicate, only those states are outputted which satisfy this predicate.
Only the dead states are outputted.
Only those states are outputted in which a ``bad'' predicate (which was entered before the computation) is satisfied.
Similar to backtracking during a search for a reachable marking with the command <R> , a path to a computed state can be outputted with this function.
For the maximal steps firing strategy, a list of steps can be outputted. All transitional numbers displayed by other functions are related to steps instead of transitions with that firing strategy; the transitions contained in any step are visible in the list displayed.
With this command, you can inspect different files created during the analysis.
The following submenu appears:
Thus, you can examine SESSION.ina with
<R> , a proof file (.prf) with <P> , a file
with computed circuits (.cir) with <C> , a states list
(.sta) with <S> , a trace (path) to a state (.tra) with
<T> , and a general result file (.res) with <F> .
See the session report ......R
See a proof .................P
See a circuits list .........C
See a states list ...........S
See a trace .................T
See a result file ...........F
© 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)