6.5.3 Computation of paths

The computation of paths is based on the partial computation of the state graph, and therefore belongs to the reachability analysis.

For nets with time allocation, note that transient states are not considered. If your marking appears only in a transient state, INA will not find it and will regard it as non-reachable, provided the entire state graph can be constructed.

<P> Compute a shortest path from the initial state to a target marking

A marking is tested for reachability, and, if possible, a path is displayed. The path is shortest with respect to the number of firing procedures. Here, a partial marking is sufficient. The marking of the remaining places is considered as not defined, i.e., treated as don't care conditions.

The marking to be examined can be read from a file or, by pressing <esc> , entered directly.

For a net with time allocation, in addition to the computation of a shortest path, it is also possible to compute a path which is minimal with respect to time (i.e. a fastest one) (compute a minimal time path). Time allocation will be inquired anyway.

After entering (or reading) the target marking, INA starts to construct the state graph of the net breadth first. The number of states so far computed is displayed: States generated.

If INA encounters a marking that agrees with the target marking on the places defined, the examination is cancelled. The target marking is reported on the screen as reachable. The path can be written into a separate file with the extension .tra or in the session report.

If the target marking is not reachable, there are two cases: if the entire state graph can be constructed and saved, the marking will be regarded as unreachable (The marking is not reachable); otherwise (always in unbounded nets), INA cancels with the message Node overflow and states that no decision can be made: No decision possible.

By pressing <Q> , the computation process can be cancelled at any time.

Any dead states which may have been found are taken into account in the further analysis.

If the method of stubborn reduction can be used (see page in chapter 6.5.1), a net construction is used to construct the state graph stubbornly reduced in such a way that a minimal path to the partial target marking will be nonetheless found.

Display of results

Using the example of net 2.1, the computation of a path is shown. The partial marking thereby used here means that the programmers two and three are working at the terminal.

Computation of a shortest path.
target submarking:
   2:1;   3:1;

The marking is reachable.

Trace of length 2
State nr.    1
P.nr: 0 1 2 3 4 5 6
toks: 2 0 0 0 1 1 1
   n1====2.login_prog2     ==> n3
State nr.    3
P.nr: 0 1 2 3 4 5 6
toks: 1 0 1 0 1 0 1
   n3====3.login_prog3     ==> n5
State nr.    5
P.nr: 0 1 2 3 4 5 6
toks: 0 0 1 1 1 0 0

States generated: 6

In this example, two firing procedures are necessary in order to get from the initial marking to the target marking. In the initial marking n1, the state n3 is reached by firing transition 2, and in that state, the target marking in state n5 is reached by firing transition 3. Or simpler: if, in the initial situation, both programmers two and three log in, the given target marking is reached.

Further path computations

In addition to the path computation described above, there are further possibilities:

<O> Compute a minimal path from the initial state to satisfy a predicate

This function computes a minimal path to a state which satisfies a previously specified state predicate (on the definition and entering see page ff in chapter 6.5.2).

In contrast to the path computation with <P> , the following minimality criteria are available:

Computation of a minimal path to a state satisfying a predicate:
'minimal' to be understood as minimal length........L
'minimal' to be understood as minimal time..........T
'minimal' to be understood as minimal value.........V

Miminal length and minimal time are defined in an analogous way to the functionality described for <P> . When computing a path with minimal value, to each transition a value is assigned, first. These values can be read from a file with the extensions .val, or, upon pressing <esc> , entered directly at the values input file prompt. The value of a path is the sum of the values of the fired transitions (on the use of evaluations see also page ff in chapter 6.5.4).

After reading a predicate, you can restrict the search by specifying a so-called ``bad'' predicate: if the predicate is satisfied by a state, the state will not be further developed (see also page in chapter 6.5.4).

Otherwise, the running and result display of this function is similar to the one with <P> .