Edit Operations for LRTS workflow

To trace resource conflicts generated in an LRTS workflow during design-time, the edit operations designers may adopt to develop the LRTS workflow are first addressed. Since an

LRTS workflow is structured [8], the construction of an LRTS workflow follows the constraints described in chapter 2. Therefore, the edit operations are restricted as following:

(1) Only an activity process can be directly inserted/removed into/from an LRTS workflow.

Control processes must be inserted/removed into/from an LRTS workflow in pairs.

(2) Designers can only alter the working durations or resource references of activity processes.

(3) The design of an LRTS workflow is started from a basic LRTS workflow, and designers edit the LRTS workflow until all the design works are completed. The definition of basic LRTS workflow is described in Definition 33.

Definition 33 (Basic LRTS workflow)

A basic LRTS workflow w = ( {s, e}, {(s, e)}, s, e ) D(s) = d(s) = D(e) = d(e) = 0

EAI(s) = EAI(e) = [0, 0]

In order to keep the control processes inserted/removed into/from an LRTS workflow in pairs, additional records for control blocks are introduced. A control block is composed of a split process starting a decision/parallel structure and a join process converging the structure.

Besides, the record also marks a natural number counter to provide distinct ID for each branch in the corresponding decision/parallel structure. The record for a control block is modeled as following.

Definition 34 (Control Blocks)

For an LRTS workflow w, CBw records all the control blocks in w.

∀cb∈CBw,

∀sp∈Pw, sp.type∈{AS, XS}, ∃cb∈CBw that sp == cb.st

(Reachable(cb.end, cb’.st)⊕Reachable(cb’.end, cb.end)) == true.

Starting from a basic LRTS workflow w, the edit operations discussed in this dissertation are listed as following:

(1) Inserting activity process p into an existent flow f Pre-Condition: f = (p’, p”)∈F_w, BM(p’, p”) == bm connected to the source process of f and the out-flow of p which is connected to the sink process of f. The minimum and maximum working durations of p are both assumed to be zero. The branch mark of the in-flow of p is given as the replaced one, and the branch mark of the out-flow of p is set as Ø because p is an activity process.

(2) Inserting a new decision structure quoted by sp and jn into an existent flow f Pre-Condition: f = (p’, p”)∈Fw, BM(p’, p”) == bm

Post-Condition: (p’, p”)∉Fw, (p’, sp), (sp, jn), (jn, p”)∈Fw, sp.type == XS, jn.type == XJ, (sp, jn, 1)∈CBw

BM( (p’, sp) ) == bm, BM( (sp, jn) ) == 0, BM( (jn, p”) ) == -1

Comments: Designers use this operation to inset a decision structure quoted by sp, an XOR-split process, and jn, an XOR-join process, into an existent flow f in w. f is replaced similarly as in operation (1). A control block record is generated with this operation. Both sp and jn are recorded, and the corresponding courter for the branches in the decision structure is initialized as 1. Besides, the branch mark of (sp, jn), the flow of the first branch split from sp, is initialized as 0.

(3) Inserting a new parallel structure quoted by sp and jn into an existent flow f structure. The only difference between them is that sp is an AND-split process, and jn is typed AND-join.

(4) Inserting a new branch to a decision/parallel structure Pre-Condition: (sp, jn, br_count)_∈CB_w, (sp, jn)_∉F_w

Post-Condition: (sp, jn)_∈F_w, BM( (sp, jn) ) == br_count++

Comments: To simplify our discussion, a flow between a pair of split and join processes is allowed being inserted only when no such flow exists in w. The flow (sp, jn) is added to F_w. and its branch mark is set to the current value of the corresponding branch counter. The counter is added by 1 after the insertion.

(5) Adding a resource reference to an activity process

Pre-Condition: r∈Rw, p∈Pw, p.type == ACT, Ref(r, p) == false Post-Condition: Ref(r, p) == true

Comments: Designers use this operation to indicate that access of the resource r is necessary for activity process p.

(6) Removing a resource reference from an activity process Pre-Condition: r_∈R_w, p_∈P_w, p.type == ACT, Ref(r, p) == true Post-Condition: Ref(r, p) == false

Comments: Designers use this operation to remove the resource reference of resource r from activity process p.

(7) Setting minimal working duration of an activity process Pre-Action: var = in_value - d(p)

Pre-Condition: p∈Pw, 0≤in_value≤D(p), var ≠ 0 Post-Condition: d(p) == in_value

Comments: Designers use this operation to designate the minimal working duration of an activity process in w to the specific input value, in_value. To simplify our discussion, in_value must be a non-negative integer is equal or smaller than

the maximal working duration of the target activity process. To facilitate our detection of resource conflicts, the variation of d(p) is recorded as var before the operation is invoked.

(8) Setting maximal working duration of an activity process Pre-Action: var = in_value - D(p)

Pre-Condition: p_∈P_w, d(p)≤in_value, var ≠ 0 Post-Condition: D(p) == in_value

Comments: Designers use this operation to designate the maximal working duration of an activity process in w to the specific input value, in_value. in_value must be a non-negative integer which is equal to or larger than the maximal working duration of the target activity process. To facilitate our detection of resource conflicts, the variation of D(p) is recorded as var before the operation is invoked.

(9) Removing the activity process p from w

Pre-Condition: (p’, p), (p, p”)∈Fw, p.type == ACT, d(p) == 0, D(p) == 0,

∀r∈Rw, Ref(r, p) == false Post-Condition: p∉Pw, (p, p”)∈Fw

Comments: Designers use this operation to remove an activity process from w. To simplify our discussion, it is assumed that before the removal of the activity process, the resource references of the activity process are first removed, and the corresponding minimum and maximal working durations are set to be 0.

(10) Removing the empty branch from w

Pre-Condition: (sp, jn, br_count)_∈CB_w, (sp, jn)_∈F_w, and a path <sp, p₁, …, p_k, jn> exists.

Post-Condition: (sp, jn)_∉F_w

Comments: Designers use this operation to remove the empty branch in a control block from w. In order to keep the integrity of w, the removal which disconnects w is forbidden.

(11) Removing the empty control block quoted by sp and jn from w Pre-Condition: (sp, jn, br_count)∈CBw, (p’, sp), (sp, jn), (jn, p”)∈Fw,

∃ no p∈Pw that (Reachable(sp, p)∧Reachable(p, jn)) == true Post-Condition: (p’, p”)∈Fw, sp, jn∉Pw,

∀cb∈CBw, cb.st ≠ sp, cb.end ≠ jn

Comments: Designers use this operation to remove a control block from w. To simplify

our discussion, only the control block containing no processes inside is allowed being removed from w.