Pre-Condition: AOPLa has been produced by Algorithm 9, op∈AOPLa Operation Set CDBO {
01: DB4op = Ø;
02: for( i = |OPLop| to 1 ) {
For the input artifact operation op, Algorithm 11 calculates DB4op from its corresponding artifact operation list. Algorithm 11 checks the operations in OPLop with reverse order.
According to Lemma 1 and Definition 10, the processes in an LRTS workflow are either before, after, concurrent or exclusive to each other, and so are the operations. The operations concurrent or exclusive to op are excluded at line 3. With Lemma 4, the first operation found passing the checking at line 3 is directly before op. According to Definition 26, if op’ and op” are both directly before op, op’ can not be before op” and vice versa. Therefore, the algorithm continues gathering the other directly before operations with the statement at line 6 after the first one is found.
To show Algorithm 11 is correct, the following lemma is depicted and proved.
Lemma 8
For any artifact operation op and op’, op’ is directly before op if and only if op’∈CDBO(op)
Proof:
We first show the if-part is correct. B.W.O.C, it is assumed that op’∈CDBO(op), but is not directly before op. According to the algorithm, the result set of Algorithm 11 is a sub-set of OPLop. Therefore, op’∈OPLop, op’.let < op.let, and op’ can not be after op on the basis of Lemma 7. Besides, op’ must pass the checking at line 3, op’ is not concurrent or exclusive to op. Based on Lemma 4 and Definition 24, op’ is before op. Since op’ is not directly before op, according to Definition 26, there must exist another operation op” which is after op’ and before op. Because op’∈CDBO(op), op’ must be collected in the result set at line 4 or line 6 in Algorithm 11. Since op” is after op’, op’.let < op”.let. op” has a larger index than op’ in OPLop, and is touched by Algorithm 11 earlier than op’ does. Therefore, either op” is directly
before op or not, op’ can not be collected in the result set at line 4 or line 6. op’∉CDBO(op) which is a contradiction, and the if-part of Lemma 8 is shown correct.
As for the only-if-part, B.W.O.C, we assume that op’ is directly before op and op’∉CDBO(op). The assumption indicates that op’ is before op. According to Lemma 7, op’.let < op.let, and thus op’ belongs to OPLop. op’ also passes the checking at line 3 based on Lemma 4 and Definition 24. If the result set is empty when Algorithm 11 touches op’, op’ is inserted into the result set at line 4 because op’ is before op. Otherwise, op’ is added into the result set at line 6 because op’ is directly before op and there exist no other operations after op’ in OPLop. Therefore, op’∈CDBO(op) which is a contradiction, and the only-if-part of Lemma 8 is shown correct. With the proofs of the both direction, Lemma 8 is proved. □
For an artifact operation op, multiple operations directly before it might exist. According to Definition 26, the operations are not before or after each other. On the basis of Lemma 1 and Definition 10, the operations are mutually concurrent or exclusive, and are possibly organized as the following cases:
(1) All the operations are concurrent to each other.
(2) All the operations are exclusive to each other.
(3) The operations can be divided into several distinct groups where the operations in the same group are concurrent to each other, and the operations belonging to different groups are all mutually exclusive.
(4) The operations can be organized into several varied groups where the operations in the same group are concurrent to each other, and the operations belonging to different groups are either identical or mutually exclusive.
The operations in case (1) compose a racing operation. In case (2), each operation is considered separately during analysis because only one of the operations is executed during run-time. Case (3) and (4) happen when the operations are made by processes reside in nestedly organized decision and parallel structures. Since only one of the branches in a decision structure is taken during run-time, the operations reside in different branches of a decision structure are
separately analyzed with the operations concurrent to them. Figure 14 illustrates two partial LRTS workflow schemas as the examples of case (3) and (4).
Figure 14 Examples for Nestedly Organized Decision and Parallel Structures
In Figure 14, we assume that the EAIs of the activity processes with footnotes are all overlapped, and all the operations made by them are thus directly before op. Figure 14(a) illustrates an example of case (3) mentioned above. In Figure 14(a), the operations directly before op can be divided into two distinct groups {op1, op2, op3} and {op4, op5, op6}. The operations are concurrent to the ones within the same group and are exclusive to the ones belonging to different groups. Figure 14(b) illustrates an example of the case (4). op1, op2, and op3 are mutually exclusive and should be separately considered when analysis. However, each of them is concurrent to op4 and op5. Therefore, the operations are organized with three groups, {op1, op4, op5}, {op2, op4, op5}, and {op3, op4, op5}. The operations in the same group are concurrent to each other, and the exclusive operations are distributed among different groups.
Definition 28 (Set of Operation Sets derived from DB4op)
∀op∈AOPLa,
DB4OPSop = {OPS | OPS⊆DB4op, ∀op’, op”∈OPS, Concurrent(op’, op”) ==
true, and ∀op3∈DB4op\OPS, ∃op4∈OPS that Exclusive(op3, op4) == true }
Each of the groups, the operation sets, in which all the operations are mutually concurrent represents an execution case during run-time. With Definition 26, the set of the operation sets
derived from DB4op is defined as above.
However, to retrieve all such operation sets from DB4op is equivalent to solve the well-known NP-hard problem “Maximal Clique Enumeration Problem [52].” Although many studies and efficient algorithms like [53] and [54] has been developed for this problem, to discuss the solution for maximal clique enumeration problem is beyond the scope of this dissertation. To illustrate our methodology, we describe a polynomial algorithm to manufacture DB4OPSop satisfying the cases (1), (2), (3) completely and case (4) partially from DB4op. The algorithm is described as following.
Algorithm 12 Collecting Directly Before Operation Sets - CDBOPS