6.7 Structural analysis

The functions for structural analysis are only offered in cases where the Petri net theory allows to draw conclusions about dynamic properties of the net from structures discovered. As a fundamental prerequisite, the options have to be set as follows: no time allocation, normal firing mode, no priorities, and firing of single transitions. Further conditions for the availability of the commands result from the previously executed pre-analysis of the current net.

The net 6.2, which models the control of two traffic lights, is the reference for all examples in this section.

It has the following strongly connected components, which are state machines:

Figure 6.4: Three strongly connected state machines components of the net 6.2

The places of the components also correspond to the minimal deadlocks and the related maximal traps. Hence, the deadlock-trap-property is satisfied.

The net is not state machine allocatable, since a pre-place allocation exists [Sta90, Definition 16.3 (182)] which does not select a strongly connected state machine component. The components illustrated above, $K_1=\{\textrm{green}_\textrm{\footnotesize one}, \textrm{green}_\textrm{\footnotesize two},\textrm{yellow}_\textrm {\footnotesize one}\}$, $K_2=\{\textrm{green}_\textrm{\footnotesize one}, \textrm{green}_\textrm {\footnotesize two},\textrm{yellow}_\textrm{\footnotesize two}\}$, and $K_3=\{\textrm{red}_\textrm{\footnotesize one},\textrm{red}_\textrm {\footnotesize two}\}$ have the post-transitions $T_1=\{t_1,t_2,t_3,t_4\}$, $T_2=\{t_1,t_2,t_3,t_4\}$, and $T_3=\{t_2,t_4\}$, respectively. The pre-place allocation $\alpha$ with $\alpha(t_1)=\textrm{green}_\textrm {\footnotesize one}$, $\alpha(t_2)=\textrm{yellow}_\textrm{\footnotesize two}$, $\alpha(t_3)=\textrm {green}_\textrm{\footnotesize two}$, and $\alpha(t_4)=\textrm{yellow}_\textrm{\footnotesize one}$ does not select any components, since $t_2\in T_1$, but $\alpha(t_2)=\textrm{yellow}_\textrm{\footnotesize two}\notin K_1$; also, $t_4\in T_2$, but $\alpha(t_4)=\textrm{yellow}_\textrm{\footnotesize one}\notin K_2$, and $t_2\in T_3$, but $\alpha(t_2)=\textrm{yellow}_\textrm{\footnotesize two}\notin K_3$.

The notions and abbreviations used here, can be found in the index or in the chapter 6.2 on page ff.

In the following excerpts from the session report, you can also view, besides the actual computation, the net properties thereby deduced.

<D> Check the deadlock-trap-, SMD-, SMA-properties

This command decides the deadlock-trap-property (DTP), and also, for ordinary nets, the state machine decomposability (SMD), and the state machine allocatability (SMA).

After the writing options have been set, INA computes the list of all deadlocks which are minimal with respect to set inclusion. Deadlocks which are not sufficiently marked in the initial marking are reported as clean or not sufficiently marked. The maximal trap in such a deadlock can not be sufficiently marked; transitions which have pre-places in that deadlock are dead.

Afterwards, the related maximal traps are computed, where the trap with the number i is the maximal trap in the deadlock number i. Here as well, traps, in particular empty sets, which have no or not enough tokens, are reported as clean or not sufficiently marked, respectively.

If this is not true for all traps, the deadlock-trap-property is satisfied, and therefore, no dead marking is reachable. [Sta90, Satz 15.5 (165)].

When the net has non-blocking multiplicity (NBM), is homogeneous (HOM), and extended simple (ES), then it is live [Sta90, Satz 15.6 (165)].

If one of the traps is not sufficiently marked, then the deadlock-trap-property is not satisfied. For an extended free choice net (EFC), the non-liveness can be deduced [Sta90, Satz 15.10 (173)].

For an ordinary net (ORD), INA subsequently computes all minimal strongly connected state machine components, as well as other minimal components, in order to test for state machine decomposability (SMD). In this case, the net would be structurally bounded (SB). Components which are clean in the initial marking are reported.

If the net is SMD and connected (CON), then INA tests for state machine allocatability (SMA). If this property is not fulfilled, then you find a pre-place allocation in the session report as a list of the form <transnr> ==> <preplacenr> , which does not select any SCSM-components.

For the net of the example 6.2, the following computation results:

Structural liveness properties of net nr. 14.Two_Traffic_Lights     :
processed candidates: 13
There are  3 minimal deadlocks:
-------------------------------
   1: 5.rot_eins, 6.rot_zwei,
   2: 1.gruen_eins, 2.gruen_zwei, 4.gelb_zwei,
   3: 1.gruen_eins, 2.gruen_zwei, 3.gelb_eins,

Corresponding maximal traps:
----------------------------
   1: 5.rot_eins, 6.rot_zwei,
   2: 1.gruen_eins, 2.gruen_zwei, 4.gelb_zwei,
   3: 1.gruen_eins, 2.gruen_zwei, 3.gelb_eins,
The deadlock-trap-property is valid.
The net has no dead reachable states.
The net is live.
The net has no dead transitions at the initial marking.
The net is live, if dead transitions are ignored.

SM-allocatability of net nr.  0:
********************************
Some minimal place sets Q with QF=FQ, but all SCSM's:

   1: 5.rot_eins, 6.rot_zwei, SCSM 
   2: 1.gruen_eins, 2.gruen_zwei, 4.gelb_zwei, SCSM 
   3: 1.gruen_eins, 2.gruen_zwei, 3.gelb_eins, SCSM 
 3 minimal component(s) found.

The net is state machine decomposable (SMD).
The net is coverable by state machines (SMC).
The net is covered by semipositive P-invariants.
The net is structurally bounded.
The net is bounded.
The net is covered by semipositive T-invariants.
There are no proper semipositive T-surinvariants.

The net is not state machine allocatable (SMA).
A pre-place allocation allocating no SCSM:
   1==>   1,   2==>   4,   3==>   2,   4==>   3,
The net is covered by 1-token SCSM's.

ORD HOM NBM PUR CSV SCF CON SC  Ft0 tF0 Fp0 pF0 MG  SM  FC  EFC ES 
 Y   Y   Y   Y   N   N   Y   Y   N   N   N   N   N   N   N   N   Y  
DTP SMC SMD SMA CPI CTI  B  SB  REV DSt BSt DTr DCF  L   LV L&S 
 Y   Y   Y   N   Y   Y   Y   Y   ?   N   N   N   ?   Y   Y   ?

The line 1==> 1, 2==> 4, 3==> 2, 4==> 3 describes the pre-place allocation $\alpha$ defined above.

Since the search for minimal deadlocks requires a considerable amount of computation, you can cancel it at any time by pressing <Q> .

Possible symmetries computed beforehand help to reduce the search: for the net 6.2, only 7 instead of 13 candidates have to be examined, due to its symmetry group computed in 6.5.1.

<C> Compute all components

With this command, all components of the current net are computed. After you have set the writing options, the computation starts. The number of components so far computed is thereby displayed. Each component is tested whether it is a state machine (SM) and strongly connected (SC). At the end, the properties SMD and SMA are checked, and appropriate deductions are made.

For the net of the example 6.2, you find the following examination results in the session report:

candidates: 117
 All components of net nr. 14.Zwei_Ampeln     :

   1:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,  5.rot_eins,
       6.rot_zwei,
   2:  5.rot_eins,  6.rot_zwei, SM SC 
   3:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei,  5.rot_eins,  6.rot_zwei,
   4:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei,  6.rot_zwei,
   5:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei, SM SC 
   6:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei,  5.rot_eins,
   7:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  5.rot_eins,  6.rot_zwei,
   8:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  6.rot_zwei,
   9:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins, SM SC 
  10:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  5.rot_eins,
  11:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,  6.rot_zwei,
  12:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,
  13:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins,  4.gelb_zwei,  5.rot_eins,

The net is state machine decomposable (SMD).
The net is coverable by state machines (SMC).
The net is covered by semipositive P-invariants.
The net is structurally bounded.
The net is bounded.
There are no proper semipositive T-surinvariants.

The net is not state machine allocatable (SMA).
A pre-place allocation allocating no SCSM:
   1==>   1,   2==>   4,   3==>   2,   4==>   3,

ORD HOM NBM PUR CSV SCF CON SC  Ft0 tF0 Fp0 pF0 MG  SM  FC  EFC ES 
 Y   Y   Y   Y   N   N   Y   Y   N   N   N   N   N   N   N   N   Y  
DTP SMC SMD SMA CPI CTI  B  SB  REV DSt BSt DTr DCF  L   LV L&S 
 ?   Y   Y   N   Y   ?   Y   Y   ?   ?   N   ?   ?   ?   ?   ?

Since the computation is very time-consuming, it can be cancelled at any time by pressing <Q> .

<M> Decide state machine coverability

This command decides for ordinary nets whether they can be covered by (not necessarily strongly connected) components which are state machines.

First, you can set the writing options. Thereafter, INA computes all minimal components [Sta90, Definition 16.1 (177)]; the number of components so far computed is thereby displayed. You can cancel the examination at any time by pressing <Q> .

All computed components are examined in order to determine whether they are state machines [Sta90, Definition 14.3 (152)]. In the session report, these are marked as SM. Components which are not marked in the initial marking are reported as clean.

If the place set of the net is the union of place sets of minimal state machine components, then the net is SMC and hence bounded [Sta90, Folgerung 16.4].

For the net of the example 6.2, the output looks like the following:

SM-coverability of net nr. 14.Zwei_Ampeln     :

Minimal place sets Q with QF=FQ:

   1:  5.rot_eins,  6.rot_zwei, SM 
   2:  1.gruen_eins,  2.gruen_zwei,  3.gelb_eins, SM 
   3:  1.gruen_eins,  2.gruen_zwei,  4.gelb_zwei, SM 
 3 minimal component(s) found.

candidates created: 29
The net is coverable by state machines (SMC).
The net is covered by semipositive P-invariants.
The net is structurally bounded.
The net is bounded.
There are no proper semipositive T-surinvariants.

ORD HOM NBM PUR CSV SCF CON SC  Ft0 tF0 Fp0 pF0 MG  SM  FC  EFC ES 
 Y   Y   Y   Y   N   N   Y   Y   N   N   N   N   N   N   N   N   Y  
DTP SMC SMD SMA CPI CTI  B  SB  REV DSt BSt DTr DCF  L   LV L&S 
 ?   Y   ?   ?   Y   ?   Y   Y   ?   ?   N   ?   ?   ?   ?   ?

If the net cannot be covered with state machines, then you find an overview of the places in the session report which lie in state machine components, and which are therefore bounded.

If INA already knows that the net is coverable by state machines (the net is known to be state machine coverable), the first question is: Compute the SM-components? If you answer this question with <Y> , INA executes the computation regardless of the previous knowledge.

This computation can also be cancelled at any time by pressing <Q> .