6.3 Analysis menu and pre-analysis

In the analysis menu, different analysis procedures are offered depending on the net type. Not for every type of net, all of the procedures are already theoretically justified, or even reasonable. Clocked nets, for example, are equivalent to the TURING MACHINE, which excludes the existence of algorithms to decide e.g. boundedness. For each type of net, only those procedures are offered which can lead to statements about the important dynamic properties. To return to the main menu, enter <Q> .

Analysis menu:
Decide structural boundedness...............................................B
Non-reachability test of a partial marking using the state equation.........N
Compute the symmetries of the net...........................................Y

Compute a shortest path from the initial state to a target marking..........P
Compute a minimal path from the initial state to satisfy a predicate........O
Compute a reachability graph................................................R
Compute a coverability graph to decide boundedness and coverability.........G

Compute a basis for all P/T-invariants [non-reachability test]..............I
Compute a basis for all semipositive P/T-[sub/sur]-invariants...............S
Format lines written to INVARI.HLP earlier..................................F
Test place- or transition-vectors for invariant properties..................T

Check the deadlock-trap-, SMD-, SMA-properties [boundedness, liveness]......D
Compute all components [check SMD-,SMA-properties]..........................C
Decide state machine coverability [for boundedness].........................M

choice >

Pre-analysis

Before the analysis menu is displayed, INA executes a pre-analysis of the net, which investigates structural properties (see page to ), and also checks which functions are available for the given net.

At the beginning, you can set writing options. These include, for example, the output option for static conflicts: Print the static conflicts? With <Y> , they will be displayed.

Example

For the net 2.1 of the three programmers sharing two terminals, the pre-analysis provides the following results:

Information on elementary structural properties:
The net is not statically conflict-free.
The net is pure.
The net is not ordinary.
The net is not conservative.
The net is not subconservative.
The net is not a state machine.
The net is not free choice.
The net is not extended free choice.
The net is extended simple.
The net is not safe.
The net is not live and safe.
The net is marked.
The net is not marked with exactly one token.
The net is not a marked graph.
The net is not homogenous.
The net has not a non-blocking multiplicity.
The net has no nonempty clean trap.
The net has no transitions without pre-place.
The net has no transitions without post-place.
The net has no places without pre-transition.
The net has no places without post-transition.
Maximal in/out-degree:  3
The net is connected.
The net is strongly connected.

From that, INA can already conclude some properties:

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

The static conflicts of the net are:

Static conflicts:
transition 1.login_Prog1 is in conflict with:
       2.login_Prog2,  3.login_Prog3,
transition 2.login_Prog2 is in conflict with:
       1.login_Prog1,  3.login_Prog3,
transition 3.login_Prog3 is in conflict with:
       1.login_Prog1,  2.login_Prog2,