# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 3 Addition of Stabilization
### Algorithm to Add Stabilization  
The algorithm proposed here adds stabilization for the case where \(k=2\). When \(k=2\), environment transitions can execute immediately after any program transition. By contrast, for larger \(k\), the environment transitions may have to wait until the program has executed \(k-1\) transitions.  
The procedure for adding stabilization is as shown in Algorithm 1. In this algorithm, \(\delta_{p}^{\prime}\) is the set of transitions of the final stabilizing program. Inside the invariant, the transitions must be equal to the original program (Constraint **C1**). Therefore, in the first line, we set \(\delta_{p}^{\prime}\) to \(\delta_{p}|S\). Next, the algorithm expands set \(R\) that includes states from which all computations reach a state in \(S\). Initially, \(R\) is set to \(S\) at (Line 2).  
State predicate \(R_{p}\) is the set of states that can reach a state in \(R\) using an unrestricted program transition, that is, a transition not in \(\delta_{r}\). In each iteration, \(R_{p}^{\prime}\) is the set of new states that we add to \(R_{p}\). In Line 9, we add program transitions from states in \(R_{p}^{\prime}\) to states in \(R\) to \(\delta_{p}^{\prime}\).  
```
0:\(S_{p},\delta_{p},\delta_{e},S\), and \(\delta_{r}\)
0:\(\delta_{p}^{\prime}\) or Not-Possible
1:\(\delta_{p}^{\prime}:=(\delta_{p}|S)\);
2:\(R=S\);
3:\(R_{p}=\{\}\)
4:repeat
5:\(R^{\prime}=R\);
6:\(R_{p}^{\prime}=\{s_{0}|s_{0}\
otin(R\cup R_{p})\wedge\exists s_{1}:s_{1}\in R :(s_{0},s_{1})\
otin\delta_{r}\}\);
7:\(R_{p}=R_{p}\cup R_{p}^{\prime}\);
8:for each \(s_{0}\in R_{p}^{\prime}\)do
9:\(\delta_{p}^{\prime}=\delta_{p}^{\prime}\cup\{(s_{0},s_{1})|(s_{0},s_{1})\
otin \delta_{r}\wedge s_{1}\in R\}\);
10:endfor
11:for each \(s_{0}\
otin R:\
exists s_{2}\in-(R\cup R_{p}):(s_{0},s_{2})\in\delta_{e}\wedge (\exists s_{1}:s_{1}\in(R\cup R_{p}):(s_{0},s_{1})\in\delta_{e}\lor s_{0}\in R _{p})\)do
12:\(R=R\cup s_{0}\);
13:endfor
14:until (\(R^{\prime}=R\));
15:if\(\exists s_{0}\
otin R\)then
16:return Not-Possible;
17:else
18:return \(\delta_{p}^{\prime}\);
19:endif
```  
**Algorithm 1** Addition of stabilization  
In the loop on Lines 11-13, we add more states to \(R\). We add \(s_{0}\) to \(R\) (Line 12), whenever every computation starting from \(s_{0}\) has a state in \(S\). A state \(s_{0}\) can be added to \(R\) only when there is no environment transition starting from \(s_{0}\) going to a state outside \(R\cup R_{p}\). In addition to this condition, there must be at least one transition from \(s_{0}\) that reaches \(R\). The loop on Lines 4-14 terminates if no state is added to \(R\) in an iteration. Upon termination of the loop, the algorithm declares failure to add stabilization if there exists a state outside \(R\). Otherwise, it returns \(\delta_{p}^{\prime}\) as the set of transitions of the stabilizing program.  
We use Figure 3 as an example to illustrate Algorithm 1. Figure 3 depicts the status of the state space in a hypothetical \(i\)th iteration of the loop on Lines 4-14. In this iteration, state \(\mathbf{A}\) is added to \(R\). This is due to the fact that (1) there is at least one transition from \(\mathbf{A}\) (namely \((\mathbf{A},\mathbf{F})\)) that reaches \(R\) and (2) there is no environment transition from \(\mathbf{A}\) that reaches outside \(R\cup R_{p}\). Likewise, state \(\mathbf{C}\) is also added to \(R\). State \(\mathbf{B}\) is not added to \(R\) due to environment transition \((\mathbf{B},\mathbf{E})\). Likewise, state \(\mathbf{D}\) is not added to \(R\). State \(\mathbf{E}\) is not added to \(R\) since there is no transition from \(\mathbf{E}\) to a state in \(R\).  
In the next, that is, \((i+1)\)th iteration, \(\mathbf{E}\) is added to \(R\) due to transition \((\mathbf{E},\mathbf{A})\) that goes to \(\mathbf{A}\) that was added to \(R\) in the \(i\)th iteration. Continuing this, \(\mathbf{B}\) and \(\mathbf{D}\) will be added in the \((i+2)\)th iteration.