Integrated Net Analyzer [v2.2final-Jul 31 2003-win32] session report: Current net options are: token type: black (for Place/Transition nets) time option: no times firing rule: normal priorities : not to be used strategy : single transitions line length: 80 Net read from levchenko_N1.pnt Information on elementary structural properties: Current name options are: transition names to be written place names to be written The net is not statically conflict-free. The net is pure. The net is ordinary. The net is homogenous. 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 not extended simple. The net is marked. The net is not marked with exactly one token. The net is not a marked graph. The net has 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: 6 The net is connected. The net is strongly connected. 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 N DTP SMC SMD SMA CPI CTI B SB REV DSt BSt DTr DCF L LV L&S ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? Current name options are: transition names to be written place names to be written Structural liveness properties of net nr. 0.t : processed candidates: 124 There are 7 minimal deadlocks: ------------------------------- 1: 14.ERKPP_Phase3, 15.ERKP_Phase3, 19.Phase3, 2: 9.ERK, 10.ERK_MEKPP, 11.ERKP_MEKPP, 12.ERKP, 14.ERKPP_Phase3, 15.ERKP_Phase3, 17.ERKPP, 3: 7.MEKP_Phase2, 8.MEKPP_Phase2, 18.Phase2, 4: 5.MEK_RafP, 6.MEKP_RafP, 7.MEKP_Phase2, 8.MEKPP_Phase2, 10.ERK_MEKPP, 11.ERKP_MEKPP, 13.MEKPP, 16.MEKP, 20.MEK, 5: 1.RasGTP, 2.Raf_RasGTP, 6: 4.RafP_Phase1, 21.Phase1, 7: 0.Raf, 2.Raf_RasGTP, 3.RafP, 4.RafP_Phase1, 5.MEK_RafP, 6.MEKP_RafP, Corresponding maximal traps: ---------------------------- 1: 14.ERKPP_Phase3, 15.ERKP_Phase3, 19.Phase3, 2: 9.ERK, 10.ERK_MEKPP, 11.ERKP_MEKPP, 12.ERKP, 14.ERKPP_Phase3, 15.ERKP_Phase3, 17.ERKPP, 3: 7.MEKP_Phase2, 8.MEKPP_Phase2, 18.Phase2, 4: 5.MEK_RafP, 6.MEKP_RafP, 7.MEKP_Phase2, 8.MEKPP_Phase2, 10.ERK_MEKPP, 11.ERKP_MEKPP, 13.MEKPP, 16.MEKP, 20.MEK, 5: 1.RasGTP, 2.Raf_RasGTP, 6: 4.RafP_Phase1, 21.Phase1, 7: 0.Raf, 2.Raf_RasGTP, 3.RafP, 4.RafP_Phase1, 5.MEK_RafP, 6.MEKP_RafP, The deadlock-trap-property is valid. The net has no dead reachable states. SM-allocatability of net nr. 0: ******************************** Some minimal place sets Q with QF=FQ, but all SCSM's: 1: 14.ERKPP_Phase3, 15.ERKP_Phase3, 19.Phase3, SCSM 2: 9.ERK, 10.ERK_MEKPP, 11.ERKP_MEKPP, 12.ERKP, 14.ERKPP_Phase3, 15.ERKP_Phase3, 17.ERKPP, SCSM 3: 7.MEKP_Phase2, 8.MEKPP_Phase2, 18.Phase2, SCSM 4: 5.MEK_RafP, 6.MEKP_RafP, 7.MEKP_Phase2, 8.MEKPP_Phase2, 10.ERK_MEKPP, 11.ERKP_MEKPP, 13.MEKPP, 16.MEKP, 20.MEK, SCSM 5: 1.RasGTP, 2.Raf_RasGTP, SCSM 6: 4.RafP_Phase1, 21.Phase1, SCSM 7: 0.Raf, 2.Raf_RasGTP, 3.RafP, 4.RafP_Phase1, 5.MEK_RafP, 6.MEKP_RafP, SCSM 7 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. There are no proper semipositive T-surinvariants. The net is not state machine allocatable (SMA). A pre-place allocation allocating no SCSM: 0==> 2, 1==> 4, 2==> 10, 3==> 7, 4==> 5, 5==> 6, 6==> 8, 7==> 11, 8==> 0, 9==> 2, 10==> 14, 11==> 15, 12==> 16, 13==> 7, 14==> 15, 15==> 19, 16==> 8, 17==> 13, 18==> 4, 19==> 3, 20==> 14, 21==> 17, 22==> 6, 23==> 5, 24==> 11, 25==> 10, 26==> 20, 27==> 3, 28==> 9, 29==> 12, 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 N DTP SMC SMD SMA CPI CTI B SB REV DSt BSt DTr DCF L LV L&S Y Y Y N Y ? Y Y ? N ? ? ? ? ? ? Current options are: computation of place-invariants no computation of subinvariants no computation of surinvariants run automatically output format = print non-zero entries with names For net nr. 0.t : 7 place-invariants written to INVARI.HLP 0 rows lost! Formatting lines from INVARI.HLP Current reduction options are: Delete repeated occurrences of the same support Do not delete covered sub/sur/invariants Delete strict invariants covering sub/sur/invariants place sub/sur/invariants for net 0.t : semipositive place invariants = 1 | 1.RasGTP : 1, | 2.Raf_RasGTP : 1 2 | 4.RafP_Phase1 : 1, | 21.Phase1 : 1 3 | 7.MEKP_Phase2 : 1, | 8.MEKPP_Phase2 : 1, | 18.Phase2 : 1 4 | 0.Raf : 1, | 2.Raf_RasGTP : 1, | 3.RafP : 1, | 4.RafP_Phase1 : 1, | 5.MEK_RafP : 1, | 6.MEKP_RafP : 1 5 | 14.ERKPP_Phase3 : 1, | 15.ERKP_Phase3 : 1, | 19.Phase3 : 1 6 | 5.MEK_RafP : 1, | 6.MEKP_RafP : 1, | 7.MEKP_Phase2 : 1, | 8.MEKPP_Phase2 : 1, | 10.ERK_MEKPP : 1, | 11.ERKP_MEKPP : 1, | 13.MEKPP : 1, | 16.MEKP : 1, | 20.MEK : 1 7 | 9.ERK : 1, | 10.ERK_MEKPP : 1, | 11.ERKP_MEKPP : 1, | 12.ERKP : 1, | 14.ERKPP_Phase3 : 1, | 15.ERKP_Phase3 : 1, | 17.ERKPP : 1 The net is safe. 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 N DTP SMC SMD SMA CPI CTI B SB REV DSt BSt DTr DCF L LV L&S Y Y Y N Y ? Y Y ? N ? ? ? ? ? ? Current options are: computation of transition-invariants no computation of subinvariants no computation of surinvariants run automatically output format = print non-zero entries with names For net nr. 0.t : 15 transition-invariants written to INVARI.HLP 0 rows lost! Formatting lines from INVARI.HLP Current reduction options are: Delete repeated occurrences of the same support Do not delete covered sub/sur/invariants Delete strict invariants covering sub/sur/invariants transition sub/sur/invariants for net 0.t : The net is covered by semipositive T-invariants. semipositive transition invariants = 1 | 8.k1 : 1, | 9.k2 : 1 2 | 18.k5 : 1, | 19.k4 : 1 3 | 0.k3 : 1, | 1.k6 : 1, | 8.k1 : 1, | 19.k4 : 1 4 | 23.k8 : 1, | 26.k7 : 1 5 | 22.k11 : 1, | 27.k10 : 1 6 | 12.k16 : 1, | 13.k17 : 1 7 | 16.k14 : 1, | 17.k13 : 1 8 | 25.k20 : 1, | 28.k19 : 1 9 | 24.k23 : 1, | 29.k22 : 1 10 | 5.k12 : 1, | 6.k15 : 1, | 17.k13 : 1, | 27.k10 : 1 11 | 20.k26 : 1, | 21.k25 : 1 12 | 2.k21 : 1, | 11.k30 : 1, | 15.k28 : 1, | 28.k19 : 1 13 | 14.k29 : 1, | 15.k28 : 1 14 | 7.k24 : 1, | 10.k27 : 1, | 21.k25 : 1, | 29.k22 : 1 15 | 3.k18 : 1, | 4.k9 : 1, | 12.k16 : 1, | 26.k7 : 1 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 N 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 ? ? ? ? ? ? Current analysis options are: no symmetrical reduction no stubborn reduction no depth restriction do not use a 'bad' predicate Computation of the reachability graph States generated: 118 Arcs generated: 468 Capacities needed: Place 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 Cap: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 The net has no dead transitions at the initial marking. Searching for dynamic conflicts: State Conflict 2: 0.k3 # 9.k2 The net is not dynamically conflict-free. Computing the strongly connected components The computed graph is strongly connected. The net is reversible (resetable). The net is live. The net is live, if dead transitions are ignored. The net is live and safe. 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 N 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 Y N ? N N Y Y Y Current options written to options.ina End of Analyzer session.