Chapter 4. Maintaining the O-graph for Item Insertion
4.1 Arc Insertion
4.1.1 TtoP arc insertion
4.1.1.1 Scenario of TtoP arc insertions
Let a relation which belongs to T×P be named as a TPR relation. The addTtoParc example in section 3.2 can be translated into: PN is transformed into PN’ by applying addTtoParc with a TPR relation (t2, p4). A formal definition of a TPR addition is described in Definition 4.1.
Definition 4.1 (TPR addition)
Let PN = (P, T, F, m0) be a Petri net. A Petri net PN’ = (P’, T’, F’, m’0) constructed by adding a TPR relation tpr into PN has the following properties:
(1) P’ = P;
(2) T’ = T;
(3) F’ = F ∪ { tpr }.
In a TPR addition, both the original net PN and the refined net PN’ have the same transitions, places, and tokens in the places, but PN‟ has one more arc representing the TPR relation added. Therefore, the initial markings of PN and PN’ are equivalent, i.e. m0 = 𝑚0′.
Definition 4.2 (Canonical Transition Firing Count Vector 𝜎 𝑗∗)
Let a Petri net be PN = (P, T, F, m0) and the O-graphs OG = (V, A) belong to PN.
The canonical transition firing count vector 𝝈 𝒋∗ at vertex vj is defined as ∀ vj ∈ V:
𝜎 𝑗∗ = 0 , if 𝑗 = 0;
∃ 𝑚𝑖, 𝑡𝑛, 𝑚𝑗 ∈ 𝐴: 𝜎 𝑗∗ = 𝜎 𝑖∗+ 𝑇𝐶𝑉. 𝑡𝑛 , otherwise
, where 0 denotes a vector of appropriate size |T| and all entries are zero.
There might be many distinct firing count vector 𝜎 𝑖 at the vertex vi. Ensuring that each vertex vi has identical structure, we choose only one arc in the O-graph to construct the canonical transition firing count vector 𝜎 𝑖∗ at vi. Thus, the canonical transition firing count vector 𝜎 𝑖∗ at vi is unique.
Definition 4.3 (another firing arc set ATF)
Let a Petri net PN = (P, T, F, m0) have the O-graph OG = (V, A). OG might have an another firing arc set ATF ⊆ A,
ATF = { ak=(mi, tn, mj) ∈ A| 𝜎 𝑗∗ ≠ 𝜎 𝑖∗ + TCV.tn }.
There are two firing count vectors 𝜎 5 at v5:
(0,0,1,0,0,1,0,0,0,0) = 𝜎 1∗ + TCV.t5 = (0,0,1,0,0,0,0,0,0,0) + (0,0,0,0,0,1,0,0,0,0) and (0,1,0,0,1,0,0,0,0,0) = 𝜎 2∗ + TCV.t4 = (0,1,0,0,0,0,0,0,0,0) + (0,0,0,0,1,0,0,0,0,0).
However, Table A3.1(a) shows a4 = (m1,t5,m5) and 𝜎 5∗ = 𝜎 1∗ + TCV.t5. Then, a5 = (m2,t4,m5) is put in ATF and atf5 is true.
There are two firing count vectors 𝜎 7 at v7:
(0,0,1,0,0,1,0,0,1,0) = 𝜎 5∗ + TCV.t8 = (0,0,1,0,0,1,0,0,0,0) + (0,0,0,0,0,0,0,0,1,0) and (0,0,1,0,0,0,1,0,0,1) = 𝜎 4∗ + TCV.t9 = (0,0,1,0,0,0,1,0,0,0) + (0,0,0,0,0,0,0,0,0,1).
However, Table A3.1(a) shows a8 = (m5,t8,m7) and 𝜎 7∗ = 𝜎 5∗ + TCV.t8. Then, a7 = (m4,t9,m7) is put in ATF and atf7 is true.
Obviously, the set ATF of Figure 3.5 is {a5, a7}.
Definition 4.4 (state space mapping function for addTtoParc SSME)
Let a Petri net PN = (P, T, F, m0) have the O-graph OG = (V, A), and M be the marking set. Assume that PN is changed into another Petri net PN’ by applying the basic editing action E = addTtoParc as described in section 3.1 according to a TPR relation tpr. M‟ is the set of all markings of PN’. The state space mapping function SSME is a function defined from M into M’, and tpr = (tsrc, pdst):
∀ mi ∈ M: SSME(mi) = mi + 𝜎 𝑖∗[tsrc] * PCV.pdst
SSME is a function which maps the reachable markings of PN to the reachable markings of PN’. For example, while using marking m1=(0,0,0,1,0,0,0,0,0) in Table A3.1(a) as input, SSME outputs marking 𝑚1′ = (0,0,0,1,1,0,0,0,0) = m1 + 𝜎 1∗[t2] * PCV.p4 = (0,0,0,1,0,0,0,0,0) + 1 * (0,0,0,0,1,0,0,0,0), as shown in Table A3.2(a).
Definition 4.5 (arc mapping function for addTtoParc RE)
Let E = addTtoParc be defined as in Definition 4.4, and M‟ be the set of all
markings of PN’. The arc mapping function RE is a function defined from A into M‟
× T’ × M‟,
and tpr = (tsrc, pdst):
∀ak = (mi, tn, mj) ∈ A: RE(ak) = (SSME(mi), tn, SSME(mj));
For example, both marking m6 and m8 can enable the firing of transition t7, i.e. a10 = (m6, t7, m9) and a11 = (m8, t7, m10) in Table A3.1(b). After arc mapping function RE is applied with inputs a10 and a11, RE(a10) = (𝑚6′,t7,𝑚9′) and RE(a11) = (𝑚8′,t7,𝑚10′ ), as shown in Table A3.2(b).
Definition 4.6 (temporal occurrence graph for addTtoParc OGE)
Let E = addTtoParc be defined as in Definition 4.4, and M be the set of all markings generated from SSME. The temporal occurrence graph OGE is the directed graph OGE = (V, A) with tpr = (tsrc, pdst), where
(1) ∀ vi ∈ V, vi ∈ V: mi = SSME(mi)
(2) A = { (mi, tn, mj) ∈ M×T×M | mi [ tn > mj } (3) ∀ak ∈ A\ATF, ak ∈ A: ak = RE(ak)
For example, Figure 4.1 is the OGE after SSME and RE are applied with input OG shown in Figure 3.5.
Figure 4.1 The temporal occurrence graph OGE modified from Figure 3.5.
v0
v8
v1 v3 v2
v4 v5 v6
v7 v9
v10
a0 a2 a1
a3
a4 a6
a7
a8 a10
a9
a12
a11
a5
According to Definition 4.6, the following properties ensure that OG‟ can be constructed by extending OGE.
Proposition 4.1
Let E = addTtoParc be defined as in Definition 4.4, C be the incidence matrix of PN, C’ be the incidence matrix of PN’, and a temporal occurrence graph OGE be defined as in Definition 4.6. Then,
(1) v0 = 𝑣0′, (2) V ⊆ V’, and (3) A ⊆ A’.
Proof:
(1) Since the initial markings of PN and PN’ are the same, v0 = 𝑣0′. (2) For each node vi in V,
mi = mi + 𝜎 𝑖∗[tsrc] * PCV.pdst.
Since the firing sequence of 𝜎 𝑖∗ can be fired in PN’, there is a marking 𝑚𝑖′ = 𝑚0′ + 𝐶′ ∗ 𝜎 𝑖∗.
Because there might be some token(s) generated from the arc (tsrc, pdst), the difference between mi[pdst] and 𝑚𝑖′[pdst] is 𝜎 𝑖∗[tsrc]. Besides, the rest of mi are equivalent to those of 𝑚𝑖′, i.e.
𝑚𝑖′ = mi + 𝜎 𝑖∗[tsrc] * PCV.pdst. According to Definition 4.4,
mi = SSM(mi) is 𝑚𝑖′.
From Definition 4.6 and 𝜎 𝑖∗ = 𝜎 𝑖∗′, vi = 𝑣𝑖′. Thus, and V is the subset of V’.
(3) For each arc ak = (mi, tn, mj) in A, there is a node 𝑣𝑖′∈ V’ and a marking 𝑚𝑖′= mi based on the discussions in (2). Since 𝑚𝑖′[pdst] ≧ mi[pdst] and the token numbers in the rest places do not change, transition tn enabled at mi can also be fired at 𝑚𝑖′. From Definition
4.6(1), another marking mj ∈ M can be modified as mj = mj + 𝜎 𝑗∗[tsrc] * PCV.pdst.
From Definition 2.4,
mj = mi + C * TCV.tn. From Definition 4.2,
𝜎 𝑗∗ = 𝜎 𝑖∗+ TCV.tn.
Therefore, mj = mi + 𝜎 𝑖∗[tsrc] * PCV.pdst + C * TCV.tn + TCV.tn[tsrc] * PCV.pdst. Because TCV.tn[tsrc] * PCV.pdst is the number of new tokens in the place pdst,
C’ * TCV.tn = C * TCV.tn + TCV.tn[tsrc] * PCV.pdst.
Thus, there exists an arc 𝑎𝑘′ =(𝑚𝑖′, tn,𝑚𝑗′) ∈ A’ and mj = 𝑚𝑖′ + C’ * TCV.tn = 𝑚𝑗′. Hence, ak = 𝑎𝑘′ and A is the subset of A’.
Proposition 4.2
Let E = addTtoParc be defined as in Proposition 4.1. Then,
∀ ak = (mi, tn, mj) ∈ A:
(1) if ak∈ ATF and (𝜎 𝑖∗+ TCV.tn)[tsrc] = 𝜎 𝑗∗[tsrc], then RE(ak) ∈ A’.
(2) if ak∈ ATF and (𝜎 𝑖∗+ TCV.tn)[tsrc] ≠ 𝜎 𝑗∗[tsrc], then RE(ak) ∉ A’ and
(SSME(mi), tn, mj+(𝜎 𝑖∗+ TCV.tn)[tsrc] * PCV.pdst ) ∈ A’.
(3) if ak∉ ATF, then RE(ak) ∈ A’.
Proof:
(1) From Definition 4.6(1), mj = mj + 𝜎 𝑗∗[tsrc] * PCV.pdst.
From Definition 2.4 and (𝜎 𝑖∗+ TCV.tn)[tsrc] = 𝜎 𝑗∗[tsrc], mj + 𝜎 𝑗∗[tsrc] * PCV.pdst = mi + 𝜎 𝑖∗[tsrc] * PCV.pdst + C * TCV.tn + TCV.tn [tsrc] * PCV.pdst.
From Proposition 4.1(2), there is a marking 𝑚𝑖′= SSME(mi).
Thus, mi + 𝜎 𝑖∗[tsrc] * PCV.pdst = 𝑚𝑖′. TCV.tn [tsrc] * PCV.pdst represents the tokens in place
pdst generated from arc (tsrc, pdst) after firing tn. The difference between C * TCV.tn and C’
* TCV.tn is the tokens generated from arc (tsrc, pdst).
Hence, mi + 𝜎 𝑖∗[tsrc] * PCV.pdst + C * TCV.tn + TCV.tn [tsrc] * PCV.pdst = 𝑚𝑖′ + C’ * TCV.tn. Because 𝑚𝑖′ + C’ * TCV.tn = 𝑚𝑗′, RE(ak) = ( SSME(mi) , tn , SSME(mj) ) = (mi, tn, mj) = (𝑚𝑖′, tn, 𝑚𝑗′) ∈ A’.
(2) From Proposition 4.1(2), there is a marking 𝑚𝑖′= SSME(mi). Since mi enable tn, 𝑚𝑖′ enable tn. mj + (𝜎 𝑖∗+ TCV.tn)[tsrc] * PCV.pdst = mi + C * TCV.tn + 𝜎 𝑖∗[tsrc] * PCV.pdst + TCV.tn[tsrc] * PCV.pdst = 𝑚𝑖′ + C’ * TCV.tn = 𝑚𝑗′.
Because SSME(mj) = mj + 𝜎 𝑗∗[tsrc] * PCV.pdst and 𝜎 𝑖∗+ TCV.tn)[tsrc] ≠ 𝜎 𝑗∗[tsrc], RE(ak)≠mj + (𝜎 𝑖∗+ TCV.tn)[tsrc] * PCV.pdst. Thus, RE(ak) ∉ A’.
(3) From Definition 4.6 (3) and ak∈ A\ATF, RE(ak) ∈ A. From Proposition 4.1(3), RE(ak) ∈ A’.
We use the addTtoParc example in section 3.2 to explain Proposition 4.2. In the example:
(1) a7∈ ATF and (𝜎 4∗+ TCV.t9)[t2]=𝜎 7∗[t2] cause RE(a7) = 𝑎7′∈ A’.
(2) a5∈ ATF and (𝜎 2∗+ TCV.t4)[t2]≠𝜎 5∗[t2] cause RE(a5) = (𝑚2′,t4,𝑚5′) ∉ A’. Also, 𝑚12′ = 𝑚5′ + (𝜎 2∗ + TCV.t4)[t2] * PCV.p4 = (0,0,0,0,0,1,0,0,0) + 0*(0,0,0,0,1,0,0,0,0) is constructed by mj+(𝜎 𝑖∗+ TCV.tn)[tsrc] * PCV.pdst. Thus, (𝑚2′,t4,𝑚12′ ) = 𝑎14′ ∈ A’.
(3) Because a3 ∉ ATF, RE(a3) = 𝑎3′∈ A’.
Proposition 4.2(2) detects the arcs which do not belong to A’. Proposition 4.2 certifies that the detections are complete.
Definition 4.7 (must re-generated marking set for addTtoParc MRGE)
For a temporal occurrence graph OGE and M, the set of all markings in OGE. OGE might have a must re-generated marking set MRGE ⊆ M, tpr = (tsrc, pdst):
MRGE = { mi ∈ M| 𝜎 𝑖∗[tsrc]>0 }.
Since 𝜎 1∗[t2]=1, 𝜎 4∗[t2]=1, 𝜎 5∗[t2]=1, and 𝜎 7∗[t2]=1, MRGE in Figure 4.1 is {m1, m4, m5, m7}.
Proposition 4.3
Let E = addTtoParc be defined as in Proposition 4.1. Then, ∀ 𝑎𝑘′=(𝑚𝑖′, tn,𝑚𝑗′) ∈ A’ : (1) if 𝑚𝑖′ ∉ M, then 𝑎𝑘′∉ A.
(2) if 𝑚𝑖′ ∈ MRGE and ∄ (mi, tn, mj) ∈ A\ATF, then 𝑎𝑘′ ∉ A.
(3) if 𝑚𝑖′ ∈ MRGE and ∃ (mi, tn, mj) ∈ A\ATF, then 𝑎𝑘′∈A.
(4) if 𝑚𝑖′ ∈ M and 𝑚𝑖′∉ MRGE, then 𝑎𝑘′ ∈A or ∃ (mi, tn, mj) ∈ ATF.
Proof:
(1) If 𝑚𝑖′ does not exist in OGE, the arcs starting from it to 𝑚𝑗′ can not occur in OGE. (2) Because ∄ (mi, tn, mj) ∈ A\ATF and Definition 4.6(3), ∄ (mi, tn, mj) ∈ A. Thus, 𝑎𝑘′ ∉ A.
(3) Since ∃ (mi, tn, mj) ∈ A\ATF and Definition 4.6(3), ∃ (mi, tn, mj) ∈ A. From Proposition 4.1(3), 𝑎𝑘′∈A.
(4) Because 𝑚𝑖′ ∉ MRGE, 𝜎 𝑖∗[tsrc]=0. Hence, mi can enable all transitions which 𝑚𝑖′ can enable. Since mi can enable all transitions which 𝑚𝑖′ can enable, each arc from 𝑚𝑖′ belongs to A or ∃ (mi, tn, mj) ∈ ATF.
We use the addTtoParc example in section 3.2 to explain Proposition 4.3. In the example:
(1) Because 𝑎16′ =(𝑚11′ ,t5,𝑚9′) and 𝑚11′ ∉ M, 𝑎16′ ∉ A.
(2) 𝑚1′∈ MRGE, a3=(m1,t6,m4), and a4=(m1,t5,m5) cause 𝑎13′ =(𝑚1′,t7,𝑚11′ )∉ A.
(3) 𝑚1′∈ MRGE and a3=(m1,t6,m4) cause 𝑎3′=(𝑚1′,t6,𝑚4′)∈ A.
(4) Since 𝑚3′∈ M and 𝑚3′ ∉ MRGE\MS, 𝑎6′=(𝑚3′,t3,𝑚6′) ∈ A.
Proposition 4.3(1) and (2) detect the arcs which do not belong to A. Proposition 4.3
certifies that the detections are complete.
Proposition 4.4
Let E = addTtoParc be defined as in Proposition 4.1. Then, (1) ∀𝑣𝑗′∈ V’ : if ∄ (𝑚𝑖′, tn,𝑚𝑗′) ∈ A and 𝑣𝑗′≠𝑣0′,
then 𝑣𝑗′∉ V.
(2) 𝑣0′∈ V
Proof:
(1) Since there is no arc pointing to the vertex 𝑣𝑗′ in OGE, such marking do not exist in OGE
but the initial vertex.
(2) Since 𝑚0′= m0 and 𝜎 0∗′= 𝜎 0∗, 𝑣0′= v0 belongs to V.
We use the addTtoParc example in section 3.2 to explain Proposition 4.4. In the example:
(1) Because 𝑣11′ ≠𝑣0′ and 𝑎13′ =(𝑚1′,t7,𝑚11′ ) ∉ A, 𝑣11′ ∉ V.
Proposition 4.5
Let E = addTtoParc be defined as in Proposition 4.1.
∀ mx, my∈ M: if SSME(mx) = SSME(my) and 𝜎 𝑦∗[tsrc]>𝜎 𝑥∗[tsrc], then ∀ (mx, tn, mxj) ∈ A,
∃ (my, tn, myj) ∈ A.
Proof:
Because SSME(my) = my + 𝜎 𝑦∗[tsrc] * PCV.pdst, SSME[mx] = mx + 𝜎 𝑥∗[tsrc] * PCV.pdst,
𝜎 𝑦∗[tsrc]>𝜎 𝑥∗[tsrc], and SSME(my) = SSME(mx), my[pdst] < mx[pdst] and the rest of my and mx are equivalent. Thus, mx can enable the transitions which my enables.
We use the addTtoParc example in section 3.2 to explain Proposition 4.5. In the example, SSME(m6) = SSME(m5) and 𝜎 5∗[t2]>𝜎 6∗[t2]. Both a8=(m5,t8,m7) and a9=(m6,t8,m8) are
constructed by firing t8.
4.1.1.2 Updating an Occurrence graph
Let a Petri net be PN = (P, T, F, m0), the O-graph OG = (V, A) belong to PN, and M be the set of all markings of P. The following algorithm presents a method to update the corresponding O-graph OG’ when a TPR relation is added into a Petri net. Each arc ai ∈ A has the flag atfi = {true, false}. The flag atfi = true means ai ∈ ATF (Definition 4.3), whereas ai ∉ ATF. Assume that PN is transformed into another Petri net PN’ by applying basic editing action E = addTtoParc according to tpr=(tsrc, pdst), i.e. addTtoParc (PN, tsrc, pdst). Algorithm 4.1 firstly modifies OG for OGE as described in Definition 4.6, and then extends OGE for the O-graph OG’ = (V’, A’) which belongs to PN’. M is the set of all markings in OGE and M’ is the set of all markings of P’.
Algorithm 4.1 Main_ATP (PN, OG, tpr) → PN’ and OG’
// Input PN: the original net // OG: the O-graph of PN // tpr: a TPR relation
// Output PN’: the refined net with tpr // OG’: the O-graph of PN’
● Mnr ←∮: a set of markings. Mnr ⊆ M’ \ M. Mnr contains those markings for which we have not yet found the successors.
● MRGE ←∮: a set of markings as in Definition 4.7.
● OGE : a temporal occurrence graph. V ←∮and A ←∮.
● OG’ : an occurrence graph. V’ ←∮and A’ ←∮.
1 add an arc from tsrc to pdst // construct PN’
2 ModifyOG_ATP // modify OG for OGE 3 Findmarking
4 ExtendOG // extend OGE for OG‟
Line 1 in Algorithm 4.1 constructs the refined Petri net PN’. Line 2 calls the function ModifyOG_ATP (Algorithm 4.2) to modify the state space in OG and redirect the flow relations in ATF. For example, the redirection changes from a5 to 𝑎14′ and generates node 𝑣12′ . Then, 𝑣12′ is added to Mnr. The function Findmarking (Algorithm 4.4) in line 3 can generate the new node 𝑣𝑗′∈V’ \ V and arc 𝑎𝑘′ ∈ A’ \ A according to MRGE. For example, the new nodes in Figure 3.7 are 𝑣11′ and 𝑣13′ . The new arcs are 𝑎13′ and 𝑎15′ . The new nodes generated by Findmarking are put in Mnr. Line 4 calls the function ExtendOG (Algorithm 4.5) to generate the rest of new nodes and arcs whose ancestors are in Mnr, e.g., the node 𝑣14′ and the arcs 𝑎16′ , 𝑎17′ , 𝑎18′ , and 𝑎19′ in Figure 3.7. The details of each step will be presented below.
Algorithm 4.2 ModifyOG_ATP
1 ATF ← ATF 2 A ← A
3 for all vi ∈ TmapV (tsrc) do 4 begin
5 NewV(vi ,vi)
6 mi[pdst] ← mi[pdst] + 𝜎 𝑖∗[tsrc] 7 // SSME(mi) in Definition 4.4 8 if(∃mj∈ M and mi = mj) 9 if(𝜎 𝑖∗[tsrc] > 𝜎 𝑗∗[tsrc]) 10 Merge(vi, vj) 11 else
12 Merge(vj, vi) 13 endif
14 else // mi ∈ MRGE
15 MRGE ←MRGE∪{mi} 16 endif
17 endfor 18
19 for all ak = (mi, tn, mj) ∈ ATF do 20 begin
21 if( (𝜎 𝑖∗+TCV.tn)[tsrc] ≠ 𝜎 𝑗∗[tsrc] ) 22 A ← A \ { ak }
23 ATF ← ATF \ { ak }
24 𝑚𝑗′ is the marking produced after mi fires tn 25 𝑣𝑗′← Node (vi, tn, 𝑚𝑗′)
26 V’ ← V’∪{𝑣𝑗′} 27 𝑎𝑙′← Arc (mi, tn, 𝑚𝑗′) 28 A’ ← A’∪{𝑎𝑙′} 29 endif
30 endfor
In Algorithm 4.2, the loop from line 3 to 17 selects a node vi in TmapV (tsrc). In line 3, TmapV (tn) is a function that maps a transition tn to a set of vertexes. ∀ vi ∈ TmapV(tn):
𝜎 𝑖∗[tn]>0. In line 5, NewV (vi ,vi) is a function. The function creates a new vertex vi, sets its datum as the following, and adds vi to V.
- mi ← mi
- 𝜎 𝑖∗←𝜎 𝑖∗
In each turn, line 6 modifies the marking of vi as described in Definition 4.4. Some of the markings after modification would be duplicated and codes from line 9 to 13 deal with this situation by calling Merge as in Algorithm 4.3 with corresponding parameters. After Merge, the node represented by the first parameter and its connected arc(s) are deleted. Because the parameters of Merge in line 10 and 12 are different, the node to be deleted is vi or vj
respectively. Otherwise, mi is added to MRGE in line 15. The loop from line 19 to 30 deletes the arcs in ATF according to “if condition” in line 21. In line 25, Node (𝒗𝒊′, tn, m’) is a function. If there is already a node 𝑣𝑗′ whose marking is equal to m‟, the function has no effect and returns address 𝑣𝑗′. Otherwise, the function adds m‟ to Mnr, creates a new vertex 𝑣𝑗′, sets its datum as the following, and returns its address.
- 𝑚′ ← m’
- 𝜎 𝑗∗′←𝜎 𝑖∗′+ TCV.tn
In line 27, Arc (𝒎𝒊′, tn, 𝒎𝒋′) is a function that creates a new arc 𝑎𝑘′= (𝑚𝑖′, tn, 𝑚𝑗′) in A‟, sets its datum as the following, and returns its address.
- 𝑎𝑡𝑓𝑘′← true and ATF’ ← ATF’∪{𝑎𝑘′ } , if 𝜎 𝑗∗′ ≠ 𝜎 𝑖∗′+ TCV.tn - 𝑎𝑡𝑓𝑘′← false , otherwise
Then, line 25 generates the node with vi, tn, and 𝑚𝑗′. Line 27 generates the arc based on mi [tn
> 𝑚𝑗′.
For example, when the loop from line 3 to 17 selects v1, line 6 modifies m1 as m1 + 𝜎 1∗[t2]
* PCV.p4. Assume that m5 belongs to M. When v6 is selected, the marking m5 and m6 in Figure 4.1 are both (0,0,0,0,1,1,0,0,0) and 𝜎 5∗[t2] > 𝜎 6∗[t2] which satisfy the conditions in line 8 and 9.
Hence, Merge(v5, v6) is called in line 10. When the loop from line 19 to 30 selects a5, (𝜎 2∗+TCV.t4)[t2] ≠ 𝜎 5∗[t2] satisfy the conditions in line 21. Thus, arc a5 in Figure 4.1 is deleted.
𝑣12′ and 𝑎14′ in Figure 3.7 are generated based on m2 [t4 > 𝑚12′ .
Algorithm 4.3 Merge (vx, vy)
// Input vx: a vertex after SSME
// Vy: a vertex after SSME
1 for all ak = (mx, tn, mxj) ∈ A //outgoing arcs of vx
2 if(atfk = true)
3 ATF ← ATF \ { ak } 4 endif
5 A ← A \ { ak } 6 endfor
7
8 for all ak = (mxi, tn, mx) ∈ A //ingoing arcs of vx
9 change ak from (mxi, tn, mx) to (mxi, tn, my) 10 if(𝜎 𝑥𝑖∗+TCV.tn≠𝜎 𝑦∗)
11 atfk ← true
12 ATF ←ATF∪{ ak } 13 endif
14 endfor
15 V ← V \ { vx }
In Algorithm 4.3, the loop from line 1 to 6 deletes each outgoing arc of vx. The loop from line 8 to 14 redirects the ingoing arcs of vx. Line 15 merges node vx and vy by deleting vx in V.
For example, when vx=v5 and vy=v6, arc a8 = (m5, t8, m7) in Figure 4.1 is deleted. When vx=v7 and vy=v8, arc a7 is redirected from (m4, t9, m7) to (m4, t9, m8). v5 and v6 are merged by deleting v5.
Proposition 4.6
Assume that the markings of vx and vy are equivalent and 𝜎 𝑥∗[tsrc] > 𝜎 𝑦∗[tsrc].
Algorithm 4.3 merges vx and vy correctly, i.e., the arcs connected with vx are redirected to vy and vx is deleted in V
Proof:
The loop from line 1 to 6 deletes each outgoing arc of vx and Proposition 4.5 holds that the redirected arcs of the outgoing arcs of vx belong to A. The loop from line 8 to 14 redirects the ingoing arcs of vx. Line 15 merges node vx and vy by deleting vx in V. With above statements, the correctness of Algorithm 4.3 holds.
Proposition 4.7
Assume that the arc from tsrc to pdst is added into PN and Algorithm 4.3 merges vx
and vy correctly. Algorithm 4.2 modifies OG as OGE, generates MRGE, and redirects the arcs in ATF correctly, i.e., OGE as defined in Definition 4.6, MRGE as defined in Definition 4.7, and the arcs after redirections belong to OG’.
Proof:
The temporal occurrence graph defined in Definition 4.6 is calculated from line 3 to 17. For
∈ V, the conditions in line 8 and 9 equals to those in Proposition 4.5 and
Algorithm 4.3 merges vx and vy correctly. Otherwise, mi is added to MRGE. Line 19 to 30 deletes and generates the arcs according to the condition in Proposition 4.2(2). With above statements, the correctness of Algorithm 4.2 holds.
Algorithm 4.4 Findmarking
1 for all mi∈ MRGE
2 for (each transition tn can be enabled at mi and ∄(mi, tn, mj) ∈ A) 3 𝑚𝑗′ is the marking produced after mi fires tn
4 𝑣𝑗′← Node (vi, tn, 𝑚𝑗′) 5 V’ ← V’∪{𝑣𝑗′} 6 𝑎𝑘′← Arc (mi, tn, 𝑚𝑗′) 7 A’ ← A’∪{𝑎𝑘′ } 8 endfor
9 endfor
In Algorithm 4.4, for each marking mi in MRGE, the loop from line 2 to 8 generates the node 𝑣𝑗′ and the arc 𝑎𝑘′ =(mi, tn, 𝑚𝑗′) based on mi [ tn > 𝑚𝑗′. Line 4 adds the new marking 𝑚𝑗′ to Mnr if 𝑚𝑗′∉ V.
For example, when the loop from line 1 to 9 selects m1 and the loop from line 2 to 8 selects t7, 𝑣11′ is generated in line 4 and 𝑎13′ is generated in line 6.
Proposition 4.8
Given PN and PN‟ as in Definition 4.1 and MRGE generated by Algorithm 4.2 correctly. Algorithm 4.4 generates the nodes and arcs from MRGE correctly, i.e., the nodes and arcs generated by Algorithm 4.4 all belong to OG’ but not OGE.
Proof:
For each marking mi∈ MRGE, the conditions in line 2 equals to those in Proposition 4.3 (2) and codes from line 4 to 7 generate the nodes and arcs for OG’. Since ∄(mi, tn, mj) ∈ A, the
arc generated by Algorithm 4.4 do not belong to OGE. Thus, the correctness of Algorithm 4.4 holds.
Algorithm 4.5 ExtendOG
1 V’ ← V’∪V 2 A’ ← A’∪A
3 ATF’ ← ATF’∪ATF 4 repeat
5 select a markings 𝑚𝑖′∈Mnr
6 for (each transition tn enabled at 𝑚𝑖′ )
7 𝑚𝑗′ is the marking produced after firing tn 8 𝑣𝑗′ ← Node (𝑣𝑖′, tn, 𝑚𝑗′)
9 V’ ← V’∪{𝑣𝑗′} 10 𝑎𝑘′← Arc (𝑚𝑖′, tn, 𝑚𝑗′) 11 A’ ← A’∪{𝑎𝑘′ } 12 endfor
13 Mnr ← Mnr \ {𝑚𝑖′} 14 until Mnr =∮
In Algorithm 4.5, for each 𝑚𝑖′ in Mnr, the loop from line 4 to 12 generates the arcs 𝑎𝑘′ ∈ A’ and nodes 𝑣𝑗′∈V’ from 𝑣𝑖′. The nodes generated by function Node are added to Mnr.
For example, when the loop from line 4 to 12 selects m11, the node generated from 𝑣11′ is 𝑣13′ and the arcs generated from 𝑣11′ are 𝑎16′ and 𝑎17′ , as shown in Figure 3.7.
Proposition 4.9
Assume that Mnr is generated by Algorithm 4.2 and Algorithm 4.4 correctly.
Algorithm 4.5 generates the nodes and arcs whose ancestors are in Mnr correctly, i.e., the nodes and arcs generated by Algorithm 4.5 all belong to OG’ and the nodes and arcs belonging to OG’ but not generated by Algorithm 4.4 are all generated by Algorithm 4.5.
Proof:
For each marking 𝑚𝑖′∈Mnr, the loop from line 4 to 14 extends the graph from Mnr which has the properties discussed in Proposition 4.3(1) and Proposition 4.4(1). Codes from line 8 to 11 generate the nodes and arcs for OG’. Proposition 4.3 certifies that the detections corresponding to Proposition 4.3(1) are complete. Hence, the correctness of Algorithm 4.5 holds.
Theorem 4.1 (Correct O-graph Modification and Extension)
Algorithm 4.1 generates OG’ correctly when adding a TtoP arc, i.e. OG’ has the same characteristic as the one constructed from PN’ directly.
Proof:
From Proposition 4.7, Algorithm 4.2 modifies OG as OGE and redirects the arcs in ATF correctly. From Proposition 4.1, OGE is the subnet of OG’. From 4.8 and 4.9, the nodes and arcs generated by Algorithm 4.4 and 4.5 all belong to OG’ and the nodes and arcs belonging to OG’ but not OGE are all generated by Algorithm 4.4 and 4.5. Hence, the correctness of Algorithm 4.1 holds.
4.1.1.3 The time complexity
Let t be the number of transitions in the Petri net, n be the number of vertexes in the input O-graph, and n’ be the number of vertexes in the result O-graph. In algorithm 4.2, it is assumed that all markings in the O-graph of the original net should be modified one time.
Thus, the loop from line 3 to 17 will run n times. Line 8 checks if mi is already in the temporal occurrence graph and the complexity of the search is O(1). Because the loop from line 19 to 30 will run n times, the complexity of Algorithm 4.2 is O(n). In algorithm 4.5, each node contained in the result O-graph but not contained in OGE should be added into Mnr. The loop
from line 4 to 14 selects a marking in Mnr and generates the arcs and nodes correspondingly.
Hence, this loop repeats |n’- n| times. Since each transition in the result net must be examined whether it is enabled at 𝑚𝑖′ or not, the complexity of the examination is O(t). The procedure Node (𝑣𝑖′, tn, 𝑚𝑗′) checks if 𝑚𝑗′ is already in O-graph and the complexity of the search is O(1).
Thus, the complexity of Algorithm 4.5 is O(|n’- n|*t). The complexity of Algorithm 4.1 is O(n + |n’- n|*t). Since designers usually edit the Petri nets sequentially, the complexity of Algorithm 4.1 is O(n + t).