# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix A Soundness, Completeness and Complexity of Algorithm 2
### Completeness  
Now, we focus on showing that Algorithm 2 is complete, that is, if there is a solution that satisfies the problem statement for adding failsafe fault-tolerance, Algorithm 2 finds one. The proof of completeness is based on the analysis of states that were removed from \(S\). First, we note the following observation:  
**Observation 4**. : _For every state \(s_{0}\) in \(ms_{2}\) one of three cases below is true:_  
1. \(s_{0}\in ms_{1}\)__
2. \(\exists_{\mathrm{S}1}::(s_{0},s_{1})\in\delta_{e}\wedge s_{1}\in ms_{1}\)__
3. \(\exists_{\mathrm{S}1}::(s_{0},s_{1})\in\delta_{e}\cap\delta_{b}\)__  
Now, for the rest of our discussion in this section, we assume that Algorithm 2 has declared failure for finding a failsafe fault-tolerant revision of program \(p=\langle S_{p},\delta_{p}\rangle\) with invariant \(S\). Let \(p^{\prime\prime}=\langle S_{p},\delta_{p}^{\prime\prime}\rangle\) with invariant \(S^{\prime\prime}\) be any revision for program \(p\). Also, let \(f\) and \(\delta_{e}\) be a set of fault transitions and a set of environment transitions for \(p\) (i.e., \(p^{\prime\prime}\)), respectively. If there exists a computation prefix that reaches a state in \(ms_{2}\), there exists a computation with that prefix that either reaches a state in \(ms_{1}\), or executes a transition in \(\delta_{b}\) (i.e., violates safety). Specifically, we have the following lemma. **Lemma A2**. : _If \(\alpha\) is a prefix of a \(p^{\prime\prime}[]2\delta_{e}[]f\) computation and \(\alpha=\langle s_{i},\ldots,s_{m}\rangle\) such that \(s_{i}\in ms_{2}\), or \(\alpha=\langle s_{0}\ldots,s_{i-1},s_{i}\rangle\) such that \(s_{i}\in ms_{2}\) and \((s_{i-1},s_{i})\in f\cup\delta_{p}^{\prime\prime}\), then, there exists a suffix \(\beta\) such that \(\alpha\beta\) is a \(p^{\prime\prime}[]2\delta_{e}[]f\) computation and_  
* \(\exists j:j\geq i:((s_{j-1},s_{j})\in\delta_{b})\)_, or_
* \(\exists j:j\geq i:(s_{j}\in ms_{1})\)_._  
Proof. : From Observation 4, we know there are three cases for \(s_{i}\). The first case is \(s_{i}\in ms_{1}\). The theorem trivially holds for this case. In the second and the third case, there is an environment transition that either is a bad transition, or reaches a state in \(ms_{1}\). This transition can occur even with the fairness assumption, as the computation has started in \(s_{j}\), or we have reached \(s_{j}\) with a fault or program transition. For states in \(ms_{1}\) we have the following lemma that says in any given revision \(p^{\prime\prime}\) for \(p\), if there exists a computation prefix that reaches a state in \(ms_{1}\), then there exists a computation with that prefix that executes a transition in \(\delta_{b}\). **Lemma A3**. : _If \(\alpha=\langle s_{0},\ldots,s_{i-1},s_{i}\rangle\) where \(s_{i}\in ms_{1}\) is a prefix of a \(p^{\prime\prime}[|2\delta_{e}|]f\) computation, then, there exists a suffix \(\beta=\langle s_{i+1},s_{i+2},\ldots\rangle\) such that \(\alpha\beta\) is a \(p^{\prime\prime}[|2\delta_{e}|]f\) computation and \(\exists j:j\geq i:(s_{j},s_{j+1})\in\delta_{b}\)._  
Proof. : We prove this inductively as we expand \(ms_{1}\):  
**Base case**: \(ms_{1}=\{s_{0}|\exists s_{1}::(s_{0},s_{1})\in f\cap\delta_{b}\}\)  
Let \(\beta\) be any \(p^{\prime\prime}[|2\delta_{e}|]f\) computation starting from \(s_{1}\). Since fault transitions can execute in any state, \(\alpha\beta\) is a \(p^{\prime\prime}[|2\delta_{e}|]f\) computation such that \((s_{0},s_{1})\in\delta_{b}\). **Induction hypothesis**: Theorem holds for current \(ms_{1}\). **Induction step**: We show when we add a state to \(ms_{1}\), the theorem still holds for \(ms_{1}\). A state \(s_{0}\) is added into \(ms_{1}\) in three cases:  
**Case 1**\(\exists s_{1}:s_{1}\in ms_{2}:(s_{0},s_{1})\in f\)  
In this case according to Lemma A2, a transition in \(\delta_{b}\) may occur, or a state in \(ms_{1}\) can be reached. Hence, according to the induction hypothesis, a transition in \(\delta_{b}\) can occur in both cases.