# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 5 Addition of Fault-Tolerance
### Algorithm to Add Masking Fault-Tolerance
```
0:\(S_{p},\delta_{p},\delta_{e},S,\delta_{b},\delta_{r}\), and \(f\)
0:\((S^{\prime},\delta^{\prime}_{p})\) or Not-Possible
1:\(S^{\prime}=S\);
2:\(\delta^{\prime}_{p}=(\delta_{p}|S)\);
3:\(ms_{1}=\{s_{0}|(s_{0},s_{1})\in f\cap\delta_{b}\}\);
4:\(ms_{2}=ms_{1}\cup\{s_{0}|\exists s_{1}:(s_{0},s_{1})\in\delta_{e}\cap\delta_{b}\}\);
5:\(mt=\{(s_{0},s_{1})|\ (s_{0},s_{1})\in(\delta_{b}\cup\delta_{r})\lor s_{1}\in ms_{2}\}\);
6:repeat
7:\(ms^{\prime}_{1}=ms_{1}\);
8:\(ms^{\prime}_{2}=ms_{2}\);
9:\(R=S^{\prime}\);
10:\(S^{\prime\prime}=S^{\prime}\);
11:\(R_{p}=\{\}\);
12:repeat
13:\(R^{\prime}=R\);
14:\(R^{\prime}_{p}=\{s_{0}|s_{0}\
otin R\land\exists s_{1}:s_{1}\in R:(s_{0},s_{ 1})\
otin mt\}\);
15:\(R^{\prime}_{p}=R^{\prime}_{p}\cup Rp\);
16:for each\(s_{0}\in R^{\prime}_{p}\)do
17:\(\delta^{\prime}_{p}=\delta^{\prime}_{p}\cup\{(s_{0},s_{1})|(s_{0},s_{1})\
otin mt \wedge s_{1}\in R\}\);
18:endfor
19:for each\(s_{0}\
otin R:\Big{(}\
exists_{2}:s_{2}\in(-(R\cup R_{p})\cup ms_{1}):(s_{0},s_{ 2})\in\delta_{e}\Big{)}\land\Big{(}\big{(}\exists s_{1}:s_{1}\in(R\cup R_{p})- ms_{1}:(s_{0},s_{1})\in\delta_{e})\land(\
exists_{2}::(s_{0},s_{2})\in(\delta_{e} \cap\delta_{b}))\big{)}\ \lor s_{0}\in R_{p}\Big{)}\)do
20:\(R=R\cup s_{0}\);
21:endfor
22:until\((R^{\prime}=R)\);
23:\(ms_{1}=ms_{1}\cup\
eg(R\cup R_{p})\);
24:\(ms_{2}=ms_{2}\cup\
eg R\);
25:repeat
26:\(ms^{\prime\prime}_{j}=ms_{1}\);
27:\(ms^{2}_{2}=ms_{2}\);
28:\(ms_{1}=ms_{1}\cup\{s_{0}|\ \exists s_{1}:s_{1}\in ms_{2}:(s_{0},s_{1})\in f\} \cup\{s_{0}|\big{(}\exists s_{1}:s_{1}\in ms_{1}:(s_{0},s_{1})\in\delta_{e} )\lor(s_{0},s_{1})\in(\delta_{e}\cap\delta_{b})\}\land\big{(}\
exists_{2}::(s_ {0},s_{2})\in\delta^{\prime}_{p}\big{)}\}\);
29:\(ms_{2}=ms_{2}\cup ms_{1}\cup\{s_{0}|\exists s_{1}:s_{1}\in ms_{1}:(s_{0},s_{ 1})\in\delta_{e}\}\));
30:\(mt=\{(s_{0},s_{1})|\ (s_{0},s_{1})\in(\delta_{b}\cup\delta_{r})\lor s_{1} \leq ms_{2}\}\);
31:until\(ms^{\prime}_{1}=ms_{1}\wedge ms^{\prime}_{2}=ms_{2}\)
32:\(\delta^{\prime}_{p}=\delta^{\prime}_{p}-mt\);
33:\(\delta^{\prime}_{p}=ClosureAndDeadlocks(S^{\prime}-ms_{2},\delta^{\prime}_{p}, \delta_{e})\);
34:repeat
35:if\(S^{\prime}=\phi\)then
36:return Not-Possible;
37:endif
38:\(S^{\prime\prime\prime}=S^{\prime}\);
39:\(ms_{3}=\{s_{0}|\ (\exists s_{1},s_{2}::(s_{0},s_{1})\in\delta_{e}\ \land(s_{0},s_{2})\in\delta_{p}\ \}\land\big{(}\
exists_{3}:(s_{0},s_{3})\in\delta^{ \prime}_{p}\big{)}\}\);
40:\(ms_{4}=\{s_{0}|\exists s_{1}::(s_{1}\in ms_{3}\land(s_{0},s_{1})\in\delta_{e} )\}\)
41:\(S^{\prime},\delta^{\prime}_{p}=ClosureAndDeadlocks(S-ms_{4},\delta^{\prime}_{p}, \delta_{e})\);
42:until\((S^{\prime\prime\prime}=S^{\prime})\)
43:until\((S^{\prime\prime}=S^{\prime}\land ms^{\prime}_{1}=ms_{1}\wedge ms^{\prime}_{2}= ms_{2})\)
44:return\((S^{\prime},\delta^{\prime}_{p})\) ;
```  
**Algorithm 3** Adding Masking Fault-Tolerance  
In the loop on Lines 11-11 we build set \(R\) which includes all states from which all computations reach a state in \(S^{\prime}\). In addition, all required program transitions are added to \(\delta^{\prime}_{p}\) by Line 11. When loop on Lines 11-11 terminates, we add all states in \(\
eg(R\cup R_{p})\) to \(ms_{1}\). We also set \(ms_{2}\) to \(\
eg R\). Then, in the loop on Lines 25-31 we expand \(ms_{1}\) and \(ms_{2}\) with the same procedure used in Algorithm 2. In Line 32, we remove any transition in \(mt\) from \(\delta_{p}^{\prime}\). In Line 33, we remove all states in \(ms_{2}\) from \(S^{\prime}\) and ensure closure and deadlock freedom. In the loop on Lines 34-42, we remove some states from \(S^{\prime}\) to avoid new behavior inside the invariant just like what we did in Algorithm 2. If any state \(s_{0}\) is removed from \(S^{\prime}\) in Lines 33 or 41, we need to repeat the loop on Lines 6-43, because it is possible that a state in \(R\) was dependent on \(s_{0}\) to reach \(S^{\prime}\) but \(s_{0}\) is not in \(S^{\prime}\) anymore. We also need to repeat this loop if the set of \(ms_{1}\) or \(m_{2}\) has changed.