# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix B Soundness, Completeness, and Complexity of Algorithm 3
### Completeness
**Line 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} \big{)}\vee(s_{0},s_{1})\in(\delta_{e}\cap\delta_{b})\}\wedge\big{(}\
exists _{2}::(s_{0},s_{2})\in\delta^{\prime}_{p}\big{)}\}\)  
We add state \(s_{0}\) to \(ms_{1}\) in three cases in this line:  
**Case 1**\(\exists s_{1}:s_{1}\in ms_{2}:(s_{0},s_{1})\in f\)  
In this case according to Lemma A9, a transition in \(\delta_{b}\) may occur, or there is a suffix that never reach \(S^{\prime}\), or a state in \(ms_{1}\) can be reached. Thus, according to the induction hypothesis, the theorem is proved. **Case 2**\(\exists s_{1}::(s_{1}\in ms_{1}\wedge(s_{0},s_{1})\in\delta_{e})\wedge( \
exists_{2}::(s_{0},s_{2})\in\delta^{\prime}_{p})\)  
In this case, if according to fairness, \((s_{0},s_{1})\) can occur, state \(s_{1}\in ms_{1}\) can be reached by \((s_{0},s_{1})\) and according to the induction hypothesis, the theorem is proved. However, if \((s_{0},s_{1})\) cannot occur, some other transition \(t\in\delta^{\prime\prime}_{p}\cup f\) occurs. Since \(\exists s_{1}:s_{1}\in ms_{1}:(s_{0},s_{1})\in\delta_{e}\), we know that \(s_{0}\
otin R\). By construction, \(\delta^{\prime}_{p}\) contains any transition from states \(\
eg R\) to \(R\). Since \(\
exists_{2}::(s_{0},s_{2})\in\delta^{\prime}_{p}\), we conclude \(t\) goes to a state in \(\
eg R\) (i.e., \(ms_{2}\)). Thus, according to Lemma A9 either a transition in \(\delta_{b}\) can occur, or there is a suffix that never reaches \(S^{\prime}\), or a state in \(ms_{1}\) can be reached. Thus, according to the induction hypothesis, the theorem is proved. **Case 3**\(\exists s_{1}::((s_{0},s_{1})\in\delta_{e}\cap\delta_{b})\wedge(\
exists_{2}:: (s_{0},s_{2})\in\delta^{\prime}_{p})\)  
In this case, if according to fairness, \((s_{0},s_{1})\) can occur, by its occurrence a transition in \(\delta_{b}\) has occurred. However, if \((s_{0},s_{1})\) cannot occur, some other transition in \(\delta^{\prime\prime}_{p}\) should occur. Since \(\exists s_{1}::((s_{0},s_{1})\in\delta_{e}\cap\delta_{b})\), \(s_{0}\
otin R\). Our algorithm add any possible program transition that is not \(mt\) and goes to a state in \(R\) to \(s_{0}\) in Line 17. Since there is no such transition, any transition in \(\delta^{\prime\prime}_{p}\) either is in \(mt\) or goes to \(\
eg R\). In either case, we have a computation that reaches a state in \(ms_{2}\) starting from \(s_{0}\). Thus, according to Lemma A9, either a transition in \(\delta_{b}\) can occur, or there is suffix that never reaches \(S^{\prime}\), or a state in \(ms_{1}\) can be reached. Thus, according to the induction hypothesis, the theorem is proved. Like Lemma A4 for Algorithm 2, we have following lemma for \(ms_{4}\) for Algorithm 3. **Lemma A11**. : _If \(S^{\prime\prime}\) includes any state in \(ms_{4}\) in any iteration of the loop on Lines 13-21, then there is a \(p^{\prime\prime}[]_{2}\delta_{e}\) computation that starts from \(S^{\prime\prime}\) that is not a \(p^{\prime\prime}[]_{2}\delta_{e}\)._  
Proof. : The proof of this lemma is very similar to that of Lemma A4. **Theorem A5**. : _Algorithm 3 is complete._  
Proof. : Suppose program \(p^{\prime\prime}\) and invariant \(S^{\prime\prime}\) solve transformation problem. We show that at any point of Algorithm 3, \(S^{\prime\prime}\) must always be a subset of \(S^{\prime}\). We prove this by looking at lines where we set \(S^{\prime}\). In the first iteration of the loop on Lines 6-43, \(S^{\prime}=S\). According to constraint **C1** of the problem definition in Section 5.1, \(S^{\prime\prime}\subseteq S\). Thus, \(S^{\prime\prime}\subseteq S^{\prime}\) for the \(S^{\prime}\) at the beginning of the first iteration of the loop on Lines 6-43.