# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 5 Addition of Fault-Tolerance
### Algorithm to Add Failsafe Fault-Tolerance  
The procedure for adding failsafe fault-tolerance for \(k=2\) is shown in Algorithm 2. In this algorithm, set \(ms_{1}\) is the set of states from which there exists a computation suffix that violates the safety of \(spec\). \(ms_{2}\) is the set of states such that, if they are reached by a program or fault transition, or starting from them, there exists a computation suffix that violates safety. Note that \(ms_{2}\) always includes \(ms_{1}\). First, \(ms_{1}\) is initialized to \(\{s_{0}|(s_{0},s_{1})\in f\cap\delta_{b}\}\) and \(ms_{2}\) is initialized to \(ms_{1}\cup\{s_{0}|\exists s_{1}::(s_{0},s_{1})\in\delta_{e}\cap\delta_{b}\}\) by Lines 1 and 2, respectively. Set \(mt\) is the set of transitions that the final program cannot have, as they are in \(\delta_{b}\cup\delta_{r}\), or reach a state in \(ms_{2}\). ```
0:\(S_{p},\delta_{p},\delta_{e},S_{b},\delta_{r}\) and \(f\)
0:\((S^{\prime},\delta^{\prime}_{p})\) or Not-Possible
1:\(ms_{1}=\{s_{0}|\exists s_{1}::(s_{0},s_{1})\in f\cap\delta_{b}\}\);
2:\(ms_{2}=ms_{1}\cup\{s_{0}|\exists s_{1}::(s_{0},s_{1})\in\delta_{e}\cap\delta_{ b}\}\);
3:\(mt=\{(s_{0},s_{1})|\;(s_{0},s_{1})\in(\delta_{b}\cup\delta_{r})\lor s_{1}\in ms _{2}\}\);
4:repeat
5:\(ms^{\prime}_{1}=ms_{1}\);
6:\(ms^{\prime}_{2}=ms_{2}\);
7:\(ms_{1}=ms_{1}\cup\{s_{0}|\;\exists s_{1}::s_{1}\in ms_{2}:(s_{0},s_{1})\in f\} \cup\{s_{0}|(\exists s_{1}::(s_{1}\in ms_{1}\wedge(s_{0},s_{1})\in\delta_{e}) \lor(s_{0},s_{1})\in\delta_{e}\cap\delta_{b})\}\land(\forall s_{2}::(s_{0},s_{ 2})\in mt)\}\);
8:\(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})\}\);
9:\(mt=\{(s_{0},s_{1})|\;(s_{0},s_{1})\in(\delta_{b}\cup\delta_{r})\lor s_{1}\in ms _{2}\}\);
10:until\((ms^{\prime}_{1}=ms_{1}\wedge ms^{\prime}_{2}=ms_{2})\)
11:\(\delta^{\prime}_{p}=\delta_{p}|S-mt\);
12:\(S^{\prime},\delta^{\prime}_{p}=ClosureAndeadlocks(S-ms_{2},\delta^{\prime}_{p}, \delta_{e})\);
13:repeat
14:if\(S^{\prime}=\emptyset\)then
15:return Not-Possible;
16:endif
17:\(S^{\prime\prime}=S^{\prime}\);
18:\(ms_{3}=\{s_{0}|\;\big{(}\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{)}\}\);
19:\(ms_{4}=\{s_{0}|\exists s_{1}::(s_{1}\in ms_{3}\land(s_{0},s_{1})\in\delta_{e})\}\)
20:\(S^{\prime},\delta^{\prime}_{p}=ClosureAndeadlocks(S-ms_{4},\delta^{\prime}_{p},\delta_{e})\);
21:until\((S^{\prime\prime}=S^{\prime})\)
22:\(\delta^{\prime}_{p}=\Big{(}\delta^{\prime}_{p}\cup((S_{p}-S^{\prime})\times S _{p})\big{)}\Big{)}-mt\);
23:return\((S^{\prime},\delta^{\prime}_{p})\);
24:\(ClosureAndeadlocks(S,\delta_{p},\delta_{e})\)
25:repeat
26:\(S^{\prime}=S\);
27:\(\delta^{\prime}_{p}=\delta_{p}\);
28:\(S=S-\{s_{0}|\;(\forall s_{1}::s_{1}\in S:(s_{0},s_{1})\
otin\delta_{p}\cup \delta_{e})\}\);
29:\(S=S-\{s_{0}|\;\exists s_{1}::(s_{0},s_{1})\in\delta_{e}\wedge s_{0}\in S\wedge s _{1}\
otin S\}\);
30:\(\delta_{p}=\delta_{p}-\{(s_{0},s_{1})::s_{0}\in S\wedge s_{1}\
otin S\}\);
31:until\((S^{\prime}=S)\land(\delta^{\prime}_{p}=\delta_{p})\)
32:return\(S,\delta_{p}\);
```  
**Algorithm 2** Adding Failsafe Fault-Tolerance  
In the loop on Lines 4-10, more states are added to \(ms_{1}\) and \(ms_{2}\). Consequently, we update \(mt\). Any state \(s_{0}\) is added to \(ms_{1}\) by Line 7 in two cases: (1) if there exists a fault transition starting from \(s_{0}\) that reaches a state in \(ms_{2}\), or (2) there exists an environment transition \((s_{0},s_{1})\) such that \((s_{0},s_{1})\) is a bad transition or \(s_{1}\in ms_{1}\) and any other transition starting from \(ms_{1}\) reaches a state in \(ms_{2}\) (i.e., any transition \((s_{0},s_{2})\in mt\)). A state is added to \(ms_{2}\) by Line 8 if it is added to \(ms_{1}\) or if there exists an environment transition to a state in \(ms_{1}\). We update \(mt\) by Line 9 to include transitions to new states added to \(ms_{2}\). The loop on Lines 4-10 terminates if no state is added to \(ms_{1}\) or \(ms_{2}\) in an iteration.