Stategraph

This section describes the implementation of the tool pbesstategraph.

Definitions

We denote the number of predicate variable instances occurring in a predicate formula \varphi by \mathrm{npred}(\varphi). We assume that predicate variable instances in \varphi are assigned a unique natural number between

and \mathrm{npred}(\varphi).

Definition

Let \varphi be a predicate formula and let i be between 1 and \mathrm{npred}(\varphi). The functions \mathrm{pred}(\varphi,i),

and \mathrm{PVI}(\varphi,i) are such that the predicate variable instance \mathrm{PVI}(\varphi,i) is the i-th predicate variable instance in \varphi, syntactically present as \mathrm{pred}(\varphi,i)(\mathrm{data}(\varphi,i)). Let \psi be a predicate formula. We write \varphi[i \rightarrow \psi] to indicate that the predicate variable instance at position i is replaced syntactically by \psi in \varphi.

Definition

Let \varphi be a predicate formula. We define the guard of predicate variable instantiation \mathrm{PVI}(\varphi,i) for

inductively as follows:

\begin{array}{lll} guard^i(c) &=& \mathit{false} \\ guard^i(Y) &=& \mathit{true} \\ guard^i(\forall d{:}D.\,\varphi) &=& guard^i(\varphi) \\ guard^i(\exists d{:}D.\,\varphi) &=& guard^i(\varphi) \\[4pt] guard^i(\varphi \wedge \psi) &=& \left\{\begin{array}{lll} s(\varphi) \wedge guard^{i - \mathrm{npred}(\varphi)}(\psi) && \text{if } i > \mathrm{npred}(\varphi) \\ s(\psi) \wedge guard^i(\varphi) && \text{if } i \leq \mathrm{npred}(\varphi) \end{array}\right. \\[4pt] guard^i(\varphi \vee \psi) &=& \left\{\begin{array}{lll} n(\varphi) \wedge guard^i(\psi) && \text{if } i > \mathrm{npred}(\varphi) \\ ns(\psi) \wedge guard^i(\varphi) && \text{if } i \leq \mathrm{npred}(\varphi) \end{array}\right. \end{array}

where

\begin{array}{lll} s(\varphi) &=& \left\{\begin{array}{lll} \varphi && \text{if } \mathrm{npred}(\varphi) = 0 \\ \mathit{true} && \text{otherwise} \end{array}\right. \\[8pt] ns(\varphi) &=& \left\{\begin{array}{lll} \lnot\varphi && \text{if } \mathrm{npred}(\varphi) = 0 \\ \mathit{true} && \text{otherwise} \end{array}\right. \end{array}

We define the function sig for computing significant variables recursively as follows:

\begin{array}{lll} sig(b) &=& FV(b) \\ sig(\varphi \wedge \psi) &=& sig(\varphi) \cup sig(\psi) \\ sig(\varphi \vee \psi) &=& sig(\varphi) \cup sig(\psi) \\ sig(X(e)) &=& \emptyset \\ sig(\exists d{:}D.\,\varphi) &=& sig(\varphi) \setminus \{d\} \\ sig(\forall d{:}D.\,\varphi) &=& sig(\varphi) \setminus \{d\} \\ sig(\varphi \Rightarrow \psi) &=& sig(\varphi) \cup sig(\psi) \\ sig(\lnot\varphi) &=& sig(\varphi) \end{array}

The functions source, target and copy

Let X(d{:}D) = \varphi be a PBES equation. Let \mathrm{source} be a function with the property that

\mathrm{source}(X,i,j) = \left\{\begin{array}{lll} e && \text{if } guard^i(\mathrm{PVI}(\varphi_X,i)) \Rightarrow d[j] \approx e \\ \bot && \text{otherwise} \end{array}\right.

A possible heuristic for obtaining a source function is to look for positive occurrences of constraints of the form d[j] \approx e in the guards; these can be used to define the source function. Let \mathrm{sigma}(X,i) be the substitution defined as

\mathrm{sigma}(X,i)(v) = \left\{\begin{array}{lll} e && \text{if } \mathrm{source}(X,i,j) = e \text{ for some } j \\ v && \text{otherwise} \end{array}\right.

We define the function \mathrm{target} as follows:

\mathrm{target}(X,i,j) = \left\{\begin{array}{lll} c && \text{if } rewrite(\mathrm{sigma}(X,i)(\mathrm{PVI}(\varphi,i))[j]) = c \\ \bot && \text{otherwise} \end{array}\right.

with c a constant. We define the function \mathrm{copy} as follows:

\mathrm{copy}(X,i,j) = \left\{\begin{array}{lll} k && \text{if } \mathrm{PVI}(\varphi,i)[k] = d[j] \\ \bot && \text{otherwise} \end{array}\right.

We define the function \mathrm{used} as follows:

\mathrm{used}(X,i,j) = d_X[j] \in FV(guard^i(\mathrm{PVI}(\varphi_X,i)))

We define the function

as follows:

Let par(X) be the set of parameters of the equation corresponding to X. Let pos(X,i) denote the i-th parameter of the equation corresponding to X.

Control flow parameters

Control flow parameters are computed in phases. First the function LCFP is computed, then the function GCFP, and finally they are related using \sim.

LCFP computation

There are two versions of the computation of LCFP.

\begin{array}{l} \operatorname{ComputeLocalControlflowParametersDefault}(\mathcal{E}) \\ \mathbf{for}\ X \in bnd(\mathcal{E})\ \mathbf{do} \\ \quad \mathbf{for}\ n = 1, \ldots, |par(X)|\ \mathbf{do} \\ \quad\quad LCFP(X,n) := \mathbf{true} \\ \mathbf{for}\ X \in bnd(\mathcal{E})\ \mathbf{do} \\ \quad \mathbf{for}\ i = 1, \ldots, npred(\varphi_X)\ \mathbf{do} \\ \quad\quad \mathbf{if}\ pred(\varphi_X,i) = X\ \mathbf{then} \\ \quad\quad\quad \mathbf{for}\ n = 1, \ldots, |par(X)|\ \mathbf{do} \\ \quad\quad\quad\quad \mathbf{if}\ source(X,i,n) = \bot\ \wedge \mathrm{target}(X,i,n) = \bot \wedge \mathrm{copy}(X,i,n) \neq n\ \mathbf{then} \\ \quad\quad\quad\quad\quad LCFP(X,n) := \mathbf{false} \\ \mathbf{return}\ LCFP \end{array}

\begin{array}{l} \operatorname{ComputeLocalControlflowParametersAlternative}(\mathcal{E}) \\ \mathbf{for}\ X \in bnd(\mathcal{E})\ \mathbf{do} \\ \quad \mathbf{for}\ n = 1, \ldots, |par(X)|\ \mathbf{do} \\ \quad\quad LCFP(X,n) := \mathbf{true} \\ \mathbf{for}\ X \in bnd(\mathcal{E})\ \mathbf{do} \\ \quad \mathbf{for}\ i = 1, \ldots, npred(\varphi_X)\ \mathbf{do} \\ \quad\quad \mathbf{if}\ pred(\varphi_X,i) = X\ \mathbf{then} \\ \quad\quad\quad \mathbf{for}\ n = 1, \ldots, |par(X)|\ \mathbf{do} \\ \quad\quad\quad\quad \mathbf{if}\ (\mathrm{source}(X,i,n) = \bot\ \wedge \mathrm{target}(X,i,n) = \bot \wedge \mathrm{copy}(X,i,n) \neq \bot) \\ \quad\quad\quad\quad \mathbf{or}\ (\mathrm{source}(X,i,n) \neq \bot\ \wedge \mathrm{target}(X,i,n) \neq \bot \wedge \mathrm{copy}(X,i,n) = \bot) \\ \quad\quad\quad\quad \mathbf{then} \\ \quad\quad\quad\quad\quad LCFP(X,n) := \mathbf{false} \\ \mathbf{return}\ LCFP \end{array}

GCFP computation

\begin{array}{l} \operatorname{ComputeGlobalControlflowParameters}(\mathcal{E},\, LCFP) \\ \mathbf{for}\ X \in bnd(\mathcal{E})\ \mathbf{do} \\ \quad \mathbf{for}\ n = 1, \ldots, |par(X)|\ \mathbf{do} \\ \quad\quad GCFP(X,n) := LCFP(X,n) \\ \mathbf{for}\ X \in bnd(\mathcal{E})\ \mathbf{do} \\ \quad \mathbf{for}\ i = 1, \ldots, npred(\varphi_X)\ \mathbf{do} \\ \quad\quad \mathbf{let}\ Y = pred(\varphi_X,i) \\ \quad\quad \mathbf{if}\ Y \neq X\ \mathbf{then} \\ \quad\quad\quad \mathbf{for}\ n = 1, \ldots, |par(X)|\ \mathbf{do} \\ \quad\quad\quad\quad \mathbf{if}\ \mathrm{target}(X,i,n) = \bot \wedge \forall m{:}\, \mathrm{copy}(X,i,m) \neq n\ \mathbf{then} \\ \quad\quad\quad\quad\quad GCFP(X,n) := \mathbf{false} \\ \mathbf{return}\ GCFP \end{array}

Control flow graphs

The symmetric closure {\sim}_S of the relation \sim defines an undirected graph (V, {\sim}_S) on the set of vertices V = \{(X,i) \mid X \in bnd(\mathcal{E}) \wedge 1 \leq i \leq |d_X|\}. This graph is called the global control flow graph. The connected components in this graph are the local control flow graphs. A local control flow graph is called invalid if it contains two vertices (X,i) and (X,j) with i \neq j.

Global algorithm

Global control flow graph

The following algorithm computes the global control flow graph.

\begin{array}{l} \operatorname{ComputeGlobalControlflowGraph}(\mathcal{E},\; X_{init}(e_{init})) \\ V := \emptyset \\ E := \emptyset \\ \mathit{todo} := \{(X_{init}, e) \mid \forall k \leq |c_X|{:}\; e[k] = e_{init}[{\downarrow_X k}]\} \\ \mathbf{while}\ \mathit{todo} \neq \emptyset\ \mathbf{do} \\ \quad \mathbf{choose}\ u \in \mathit{todo} \\ \quad \mathit{todo} := \mathit{todo} \setminus \{u\} \\ \quad V := V \cup \{u\} \\ \quad \mathbf{for}\ i = 1 \cdots \mathrm{npred}(\varphi)\ \mathbf{do} \\ \quad\quad \mathbf{if}\ \operatorname{EnabledEdge}(u,i) \\ \quad\quad\quad v := \operatorname{ComputeVertex}(u, i, \mathrm{PVI}(\varphi_X, i)) \\ \quad\quad\quad \mathbf{if}\ v \notin V \\ \quad\quad\quad\quad V := V \cup \{v\} \\ \quad\quad\quad\quad \mathit{todo} := \mathit{todo} \cup \{v\} \\ \quad\quad\quad E := E \cup \{(u, i, v)\} \\ \mathbf{return}\ (V, E) \end{array}

\begin{array}{l} \operatorname{EnabledEdge}(u, i) \\ \mathbf{let}\ u = (X, e) \\ \mathbf{for}\ k = 1 \cdots |c_X|\ \mathbf{do} \\ \quad \mathbf{if}\ \mathrm{source}(X, i, {\downarrow_X k}) \neq \bot \wedge \mathrm{source}(X, i, {\downarrow_X k}) \neq e_k\ \mathbf{then} \\ \quad\quad \mathbf{return}\ \mathbf{false} \\ \mathbf{return}\ \mathbf{true} \end{array}

\begin{array}{l} \operatorname{ComputeVertex}(u, i, Y(f)) \\ \mathbf{let}\ u = (X, e) \\ \mathbf{for}\ l = 1 \cdots |c_Y|\ \mathbf{do} \\ \quad q := \mathrm{target}(X, i, {\downarrow_Y l}) \\ \quad \mathbf{if}\ q = \bot\ \mathbf{then} \\ \quad\quad \mathbf{choose}\ k\ \mathbf{such\ that}\ \mathrm{copy}(X, i, {\downarrow_X k}) = {\downarrow_Y l} \\ \quad\quad v_l := e_k \\ \quad \mathbf{else} \\ \quad\quad v_l := q \\ \mathbf{return}\ (Y, v) \end{array}

Note that \mathrm{copy}(X,i,{\downarrow_X k}) = {\downarrow_Y l} implies that parameters (X, {\downarrow_X k}) and

are related.

Remark

In the code {\downarrow_X k} is represented by cfp_X[k].

Remark

In the code \mathrm{copy}(X,i,{\downarrow_X k}) is represented by Yf.copy(k), where Yf = \mathrm{PVI}(\varphi_X, i).

Global control flow marking

The following algorithm computes the function marking that denotes which parameters are marked in a vertex of the control flow graph (V, E).

\begin{array}{l} \operatorname{ComputeMarkingGlobal}(\mathcal{E},\; X_{init}(e_{init}),\; V,\; E) \\ \mathbf{for}\ u = X(e) \in V\ \mathbf{do}\quad marking(u) := sig(u) \cap par(X) \\ \mathit{todo} := V \\ \mathbf{while}\ \mathit{todo} \neq \emptyset\ \mathbf{do} \\ \quad \mathbf{choose}\ v = X(e) \in \mathit{todo} \\ \quad \mathit{todo} := \mathit{todo} \setminus \{v\} \\ \quad \mathbf{for}\ (u,v) \in E\ \mathbf{do} \\ \quad\quad \mathbf{let}\ X(f) = label(u,v) \\ \quad\quad \mathbf{for}\ d_X[j] \in marking(v) \\ \quad\quad\quad M := (FV(f[j]) \setminus marking(u)) \cap par(X) \\ \quad\quad\quad \mathbf{if}\ M \neq \emptyset \\ \quad\quad\quad\quad marking(u) := marking(u) \cup M \\ \quad\quad\quad\quad \mathit{todo} := \mathit{todo} \cup \{u\} \end{array}

Global reset variables

Let

and let V be the global control flow graph. Then we define

\begin{array}{l} \operatorname{ResetVariableGlobal}(Y(e),\; i,\; V) \\ \varphi := \mathbf{true} \\ \mathbf{for}\ u = Y(f) \in V\ \mathbf{do} \\ \quad c := \mathbf{true} \\ \quad k := 1 \\ \quad \mathbf{for}\ j = 1 \cdots |par(Y)|\ \mathbf{do} \\ \quad\quad r := [] \\ \quad\quad \mathbf{if}\ CFP(Y,j)\ \mathbf{then} \\ \quad\quad\quad \mathbf{if}\ \mathrm{target}(X,i,j) = \bot \\ \quad\quad\quad\quad c := c \wedge (e[j] = f[k]) \\ \quad\quad\quad r := r \mathbin{\vartriangleleft} f[k] \\ \quad\quad \mathbf{else\ if}\ e[j] \in marking(u)\ \mathbf{then} \\ \quad\quad\quad r := r \mathbin{\vartriangleleft} e[j] \\ \quad\quad \mathbf{else} \\ \quad\quad\quad r := r \mathbin{\vartriangleleft} default\_value(e[j]) \\ \quad\quad k := k + 1 \\ \quad \varphi := \varphi \wedge (c \Rightarrow Y(r)) \\ \mathbf{return}\ \varphi \end{array}

Compute values

Let C be a component containing related CFPs.

\begin{array}{l} \operatorname{ComputeValues}(\mathcal{E},\; X_{init}(e_{init}),\; C) \\ \mathit{result} := \emptyset \\ \mathbf{for}\ (X,j) \in C\ \mathbf{do} \\ \quad \mathbf{if}\ X = X_{init}\ \mathbf{then}\quad \mathit{result} := \mathit{result} \cup \{e_{init}[j]\} \\ \mathbf{for}\ (X,k) \in C\ \mathbf{do} \\ \quad \mathbf{for}\ i = 1 \cdots \mathrm{npred}(\varphi_X)\ \mathbf{do} \\ \quad\quad \mathbf{if}\ \mathrm{source}(X,i,k) = v\ \mathbf{then}\quad \mathit{result} := \mathit{result} \cup \{v\} \\ \mathbf{for}\ (Y,k) \in C\ \mathbf{do} \\ \quad \mathbf{for}\ i = 1 \cdots \mathrm{npred}(\varphi_Y)\ \mathbf{do} \\ \quad\quad \mathbf{if}\ \mathrm{pred}(\varphi_Y,i) = Y \wedge \mathrm{target}(Y,i,k) = v\ \mathbf{then}\quad \mathit{result} := \mathit{result} \cup \{v\} \\ \mathbf{return}\ \mathit{result} \end{array}

Local algorithm

Local control flow graph

Given a GCFG (W, \sim) and a component

, then we define U as \{(X,i,d=e) \mid (X,i,d) \in C \wedge e \in \operatorname{ComputeValues}(C)\} \cup \{(X_{init},?,?=?) \mid \forall i{:}\,(X_{init},i) \notin C\}. Note that this algorithm potentially extends the graph with ‘undefined’ nodes in a lazy fashion.

\begin{array}{l} \operatorname{ComputeLocalControlFlowGraph}(U, C) \\ V, E := U, \emptyset \\ \mathit{todo} := U \\ \mathbf{while}\ \mathit{todo} \neq \emptyset\ \mathbf{do} \\ \quad \mathbf{choose}\ u = (X,k,d=e) \in \mathit{todo} \\ \quad \mathit{todo} := \mathit{todo} \setminus \{u\} \\ \quad \mathbf{for}\ i = 1 \cdots \mathrm{npred}(\varphi_X)\ \mathbf{do} \\ \quad\quad \mathbf{let}\ Y = \mathrm{pred}(\varphi_X, i) \\ \quad\quad \mathbf{if}\ d = ?\ \mathbf{then} \\ \quad\quad\quad \mathbf{if}\ (Y,k') \in C\ \text{for some}\ k'\ \mathbf{then} \\ \quad\quad\quad\quad \mathbf{if}\ \mathrm{target}(X,i,k') = e'\ \mathbf{then} \\ \quad\quad\quad\quad\quad v := (Y,k',d_Y[k']=e') \\ \quad\quad\quad\quad\quad insert(V,E,\mathit{todo},u,i,v) \\ \quad\quad\quad \mathbf{else} \\ \quad\quad\quad\quad \mathbf{if}\ X \neq Y\ \mathbf{then} \\ \quad\quad\quad\quad\quad v := (Y,?,?=?) \\ \quad\quad\quad\quad\quad insert(V,E,\mathit{todo},u,i,v) \\ \quad\quad \mathbf{else} \\ \quad\quad\quad \mathbf{if}\ (Y,k') \in C\ \text{for some}\ k'\ \mathbf{then} \\ \quad\quad\quad\quad \mathbf{if}\ (\mathrm{source}(X,i,k)=e \wedge \mathrm{target}(X,i,k')=e')\ \mathbf{then} \\ \quad\quad\quad\quad\quad insert(V,E,\mathit{todo},u,i,(Y,k',d_Y[k']=e')) \\ \quad\quad\quad\quad \mathbf{else\ if}\ (Y \neq X \wedge \mathrm{source}(X,i,k)=\bot \wedge \mathrm{target}(X,i,k')=e')\ \mathbf{then} \\ \quad\quad\quad\quad\quad insert(V,E,\mathit{todo},u,i,(Y,k',d_Y[k']=e')) \\ \quad\quad\quad\quad \mathbf{else\ if}\ (Y \neq X \wedge \mathrm{source}(X,i,k)=\bot \wedge \mathrm{copy}(X,i,k)=k')\ \mathbf{then} \\ \quad\quad\quad\quad\quad insert(V,E,\mathit{todo},u,i,(Y,k',d_Y[k']=e)) \\ \quad\quad\quad \mathbf{else} \\ \quad\quad\quad\quad v := (Y,?,?=?) \\ \quad\quad\quad\quad insert(V,E,\mathit{todo},u,i,v) \\ \mathbf{return}\ (V,E) \end{array}

where insert(V,E,\mathit{todo},u,i,v) is shorthand for the statements

\begin{array}{l} \mathbf{if}\ v \notin \mathit{todo} \wedge v \notin V\ \mathbf{then}\quad \mathit{todo} := \mathit{todo} \cup \{v\} \\ V := V \cup \{v\} \\ E := E \cup \{(u,i,v)\} \end{array}

Local belongs relation

Let (V, \longrightarrow) be a local control flow graph, and \mathrm{rules} be a predicate defined as

\mathrm{rules}(V,X,i) = \exists_{(X,j,e) \in V}{:}\; (X,j,e) \overset{i}{\longrightarrow}.

Local control flow marking

Let (V, E) be a local control flow graph, and B the corresponding belongs relation.

\begin{array}{l} \operatorname{UpdateMarkingRule1}(B,\; u,\; i,\; v) \\ \mathbf{let}\ u = (X,n,d_X[n]=z) \\ \mathbf{let}\ v = (Y,m,d_Y[m]=w) \\ \mathbf{let}\ Y(e) = \mathrm{PVI}(\varphi_X, i) \\ M := \emptyset \\ \mathbf{for}\ d_Y[l] \in marking(v)\ \mathbf{do} \\ \quad M := M \cup \bigl(\mathrm{FV}(\mathrm{rewr}(e[l],[d_X[n]{:=}z])) \cap \{d \mid (X,d) \in B\}\bigr) \\ \mathbf{return}\ marking(u) \cup M \end{array}

\begin{array}{l} \operatorname{UpdateMarkingRule2}(B,\; u,\; i,\; v) \\ \mathbf{let}\ u = (X,n,d_X[n]=z) \\ \mathbf{let}\ v = (Y,m,d_Y[m]=w) \\ \mathbf{let}\ Y(e) = \mathrm{PVI}(\varphi_X, i) \\ M := \emptyset \\ \mathbf{for}\ d_Y[l] \in marking(v)\ \mathbf{do} \\ \quad \mathbf{if}\ (Y,d_Y[l]) \notin B\ \mathbf{then} \\ \quad\quad M := M \cup \bigl(\mathrm{FV}(\mathrm{rewr}(e[l],[d_X[n]{:=}z])) \cap \{d \mid (X,d) \in B\}\bigr) \\ \mathbf{return}\ marking(u) \cup M \end{array}

\begin{array}{l} \operatorname{ComputeMarkingLocal}(\mathcal{E},\; (V_1,E_1,B_1), \ldots, (V_J,E_J,B_J)) \\ \mathbf{for}\ j = 1 \cdots J\ \mathbf{do} \\ \quad \mathbf{for}\ u=(X,n,d_X[n]=z) \in V_j\ \mathbf{do} \\ \quad\quad marking(u) := significant(u) \cap \{d \mid (X,d) \in B_j\} \\ \mathit{stable} := \mathbf{false} \\ \mathbf{while}\ \lnot\,\mathit{stable}\ \mathbf{do} \\ \quad \mathit{stableint} := \mathbf{false} \\ \quad \mathbf{while}\ \lnot\,\mathit{stableint}\ \mathbf{do} \\ \quad\quad \mathit{stableint} := \mathbf{true} \\ \quad\quad \mathbf{for}\ j = 1 \cdots J\ \mathbf{do} \\ \quad\quad\quad \mathit{todo} := V_j \\ \quad\quad\quad \mathbf{while}\ \mathit{todo} \neq \emptyset\ \mathbf{do} \\ \quad\quad\quad\quad \mathbf{choose}\ u=(X,n,d_X[n]=z) \in \mathit{todo} \\ \quad\quad\quad\quad \mathit{todo} := \mathit{todo} \setminus \{u\} \\ \quad\quad\quad\quad \mathbf{if}\ marking(u) = \{d \mid (X,d) \in B_j\}\ \mathbf{then\ continue} \\ \quad\quad\quad\quad \mathbf{for}\ (u,i,v) \in E_j\ \mathbf{do} \\ \quad\quad\quad\quad\quad m := marking(u) \\ \quad\quad\quad\quad\quad marking(u) := \operatorname{UpdateMarkingRule1}(B_j,\, u,\, i,\, v) \\ \quad\quad\quad\quad\quad \mathbf{if}\ m \neq marking(u)\ \mathbf{then} \\ \quad\quad\quad\quad\quad\quad \mathit{todo} := \mathit{todo} \cup \{v' \mid \exists i'{:}\,(v',i',u) \in E_j\} \\ \quad\quad\quad\quad\quad\quad \mathit{stableint} := \mathbf{false} \\ \quad \mathit{stableext} := \mathbf{false} \\ \quad \mathbf{while}\ \lnot\,\mathit{stableext}\ \mathbf{do} \\ \quad\quad \mathit{stableext} := \mathbf{true} \\ \quad\quad \mathbf{for}\ j = 1 \cdots J\ \mathbf{do} \\ \quad\quad\quad \mathbf{for}\ u=(X,n,d_X[n]=z) \in V_j\ \mathbf{do} \\ \quad\quad\quad\quad \mathbf{if}\ marking(u) = \{d \mid (X,d) \in B_j\}\ \mathbf{then\ continue} \\ \quad\quad\quad\quad \mathbf{for}\ (u,i,w) \in E_j\ \mathbf{do} \\ \quad\quad\quad\quad\quad \mathbf{let}\ Y(e) = \mathrm{PVI}(\varphi_X, i) \\ \quad\quad\quad\quad\quad \mathbf{for}\ k = 1 \cdots J\ \mathbf{do} \\ \quad\quad\quad\quad\quad\quad \mathbf{if}\ k \neq j\ \mathbf{then} \\ \quad\quad\quad\quad\quad\quad\quad \mathbf{for}\ v=(Y,m,d_Y[m]=w) \in V_k\ \mathbf{do} \\ \quad\quad\quad\quad\quad\quad\quad\quad \mathbf{if}\ \exists v'=(X,m',D_X[m']) \in V_k\ \text{s.t.}\ (v',i,v) \in E_k\ \mathbf{then} \\ \quad\quad\quad\quad\quad\quad\quad\quad\quad m := marking(u) \\ \quad\quad\quad\quad\quad\quad\quad\quad\quad marking(u) := \operatorname{UpdateMarkingRule2}(B_j,\, u,\, i,\, v) \\ \quad\quad\quad\quad\quad\quad\quad\quad\quad \mathbf{if}\ m \neq marking(u)\ \mathbf{then} \\ \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad \mathit{stableint} := \mathbf{false} \\ \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad \mathit{stableext} := \mathbf{false} \\ \quad \mathit{stable} := \mathit{stableint} \wedge \mathit{stableext} \end{array}

Local reset variables

\begin{array}{l} \operatorname{ResetVariableLocal}(i,\; \sigma X(d_X)=\varphi_X,\; V_1,\ldots,V_J,\; B_1,\ldots,B_J,\; \mathrm{rules}) \\ \mathbf{let}\ Y(e) = \mathrm{PVI}(\varphi_X, i) \\ e' := e \\ \mathbf{for}\ k = 1 \cdots |e|\ \mathbf{do} \\ \quad \mathbf{if}\ \mathrm{CFP}(Y,k)\ \mathbf{then\ continue} \\ \quad \mathit{relevant} := \mathbf{true} \\ \quad \mathit{condition} := \{\} \\ \quad \mathbf{for}\ j = 1 \cdots J\ \mathbf{do} \\ \quad\quad \mathbf{if}\ \mathrm{rules}(V_j,X,i)\ \mathbf{then} \\ \quad\quad\quad \mathbf{let}\ p,q\ \text{be such that}\ (Y,p,q) \in V_j \\ \quad\quad\quad \mathbf{if}\ \mathrm{target}(X,i,p) \neq \bot\ \mathbf{then} \\ \quad\quad\quad\quad \mathbf{let}\ q' = \mathrm{target}(X,i,p) \\ \quad\quad\quad\quad \mathit{relevant} := \mathit{relevant} \wedge \bigl((Y,d_Y[k]) \in B_j \Rightarrow d_Y[k] \in marking(Y,p,q')\bigr) \\ \quad\quad\quad \mathbf{else} \\ \quad\quad\quad\quad \mathit{relevant} := \mathit{relevant} \wedge \bigl((Y,d_Y[k]) \in B_j \Rightarrow \exists r{:}\,d_Y[k] \in marking(Y,p,r)\bigr) \\ \quad\quad\quad\quad \mathit{condition} \mathrel{{+}{=}} \{e[p]=r \mid (Y,d_Y[k]) \in B_j \wedge (Y,p,r) \in V_j \wedge d_Y[k] \notin marking(Y,p,r)\} \\ \quad \mathbf{if}\ \lnot\,\mathit{relevant}\ \mathbf{then} \\ \quad\quad e'[k] := default\_value(d_Y[k]) \\ \quad \mathbf{else\ if}\ \mathit{condition} \neq \{\}\ \mathbf{then} \\ \quad\quad e'[k] := \mathit{if}(join\_or(\mathit{condition}),\, default\_value(d_Y[k]),\, e[k]) \\ \mathbf{return}\ Y(e') \end{array}