## 2 WFT-Net Model
### The Firing Rule of WFT-Nets
A new configuration \(c^{\prime}\) is generated after firing \(t\) at \(c\), denoted as \(c[t)c^{\prime}\), where \(c^{\prime}=(m^{\prime}\), \(\theta^{\prime}\), \(\omega^{\prime}\), \(\delta^{\prime}\)) holds for \(m[t)m^{\prime}\) \(\wedge(\forall d\in\mathcal{D}(\mathcal{D}_{t}^{wt}\cup\mathcal{D}_{t}^{dt}) :\theta^{\prime}(d)=\theta(d))\) \(\wedge(\forall d\in\mathcal{D}_{t}^{wt}:\theta^{\prime}(d)=\top)\) \(\wedge(\forall d\in\mathcal{D}_{t}^{dt}:\theta^{\prime}(d)=\bot)\) \(\wedge(\forall R\in\mathcal{R}_{t}^{ins},\forall R_{t}^{ins}\cap R=\emptyset\): \(\omega^{\prime}(R)=\omega(R)\cup R_{t}^{ins})\) \(\wedge(\forall R\in\mathcal{R}_{t}^{upd},\forall R_{t}^{upd}\subseteq R: \omega^{\prime}(R)=\omega(R)\backslash(R_{t}^{upd}\cup\overline{R}_{t}^{upd}))\) \(\wedge(\forall R\in\mathcal{R}_{t}^{del},\forall R_{t}^{del}\subseteq R: \omega^{\prime}(R)=\omega(R)\backslash R_{t}^{del})\) \(\wedge(\forall\pi\in\Pi:(\mathcal{D}_{t}^{G}\cap(\mathcal{D}_{t}^{dt}\backslash \mathcal{D}_{t}^{pt})\
eq\emptyset\vee(\forall R\in\mathcal{R}_{t}^{G}:\omega^ {\prime}(R)=\bot\) \(\vee R_{t}^{G}\
ot\subseteq R))\Rightarrow\delta^{\prime}(\pi)=\bot)\) \(\wedge(\forall\pi\in\Pi:((\forall d\in\mathcal{D}_{t}^{G}:\theta^{\prime}(d)= \top)\wedge(\forall R\in\mathcal{R}_{t}^{G}:\omega^{\prime}(R)=\top\) \(\wedge R_{t}^{G}\subseteq R))\Rightarrow\delta^{\prime}(\pi)\in\{true,false\})\) \(\wedge(\forall\pi\in\Pi:(\mathcal{D}_{t}^{G}\cup\mathcal{R}_{t}^{G})\cap( \mathcal{D}_{t}^{wt}\cup\mathcal{D}_{t}^{dt}\cup\mathcal{R}_{t}^{ins}\cup \mathcal{R}_{t}^{upd}\cup\) \(\mathcal{R}_{t}^{del})=\emptyset\Rightarrow\delta^{\prime}(\pi)=\delta(\pi))\). For the WFT-net in Figure 2 with \(c_{0}=([start]\), \(\{\)_aid\(\rightarrow\bot\), ac\(\rightarrow\bot\), bid\(\rightarrow\bot\)_\(\}\), \(\{R_{1}=\{(\)_aid_\(1\), \(ac_{1})\}\), \(R_{2}=\{(\)_bid_\(1\), _aid_\(1\), _ac_\(1)\}\)}, \(\{\)_\(\pi_{1}\)\(\mapsto\)\(\bot\), \(\pi_{2}\)\(\mapsto\)\(\bot\)_\(\}\)), only \(t_{1}\) is enabled at \(c_{0}\). After firing \(t_{1}\), the token in \(start\) is moved into \(p_{1}\), and all data elements except \(ac\) are undefined since only \(ac\) is written by \(t_{1}\). The states of all tables have no changes, since \(its(t_{1})=\emptyset\), \(upd(t_{1})=\emptyset\), \(del(t_{1})=\emptyset\), as well as the predicates \(\pi_{1}\) and \(\pi_{2}\). According to Definition 3, a new configuration \(c^{\prime}\) is generated after firing \(t_{1}\). Then, \(t_{2}\) is enabled at \(c_{1}\), and a new configuration \(c^{\prime\prime}\) is generated after firing \(t_{2}\). And the _defined_ aid can make \(\pi_{1}\)_defined_. Obviously, the enabled transition at \(c^{\prime\prime}\) is determined by the value of \(\pi_{1}\), i.e., the exact value of _aid_. \(c^{\prime}=([p_{1}]\), \(\{\)_aid\(\rightarrow\bot\), ac\(\rightarrow\top\), bid\(\rightarrow\bot\)_\(\}\), \(\{R_{1}=\{\)_aid_\(1\), _ac_\(1)\}\), \(R_{2}=\{(\)_bid_\(1\), _aid_\(1\), _ac_\(1)\}\)}, \(\{\)_\(\{\pi_{1}\)\(\mapsto\)\(\bot\), _\(\pi_{2}\)\(\mapsto\)\(\bot\}\)_, \(\{\)_\(\pi_{1}\)\(\mapsto\)\(\top\), _\(\pi_{2}\)\(\mapsto\)\(\bot\)_\(\}\)_). Note that for each data element, its values assigned by the function \(\theta\) are abstract (i.e., _defined_ and _undefined_), as well as the state of data tables and predicates. In order to clearly express the specific information of the data flow, the concept of _data refinement_ is employed to display the concrete values of data elements, and the corresponding refining strategy is introduced in Section 4. Considering that the abstract value of each data element can be refined into several concrete values, several new configurations can be generated after firing a transition. Given a configuration set \(C\) and two configurations \(c\) and \(c^{\prime}\), \(c^{\prime}\) is a successor of \(c\) if \(c[t)C\) and \(c^{\prime}\in C\). And then the reachability of a WFT-net is as follows.