# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix B Soundness, Completeness, and Complexity of Algorithm 3
### Soundness
Thus, in either case, we reach \(R\). Since in the last iteration of loop on Lines 6-43, we do not change the set of transitions for states in \(R\) of the previous iteration, based on the induction hypothesis, the lemma is proved. The following lemma states that when the repaired program starts at its invariant \(S^{\prime}\), if it reaches a state in \(R_{p}-R\), in the rest of the its computation it will reach a state in \(S^{\prime}\). Specifically,  
**Lemma A7**. : _For every \(\delta^{\prime}_{p}[]_{2}\delta_{e}[]f\) computation \(\langle s_{0},s_{1},\ldots\rangle\) such that \(s_{0}\in S^{\prime}\), for \(S^{\prime}\), \(R_{p}\) and \(R\) in the last iteration of loop on Lines 6-43, we have: \(\forall s_{i}:s_{i}\in R_{p}-R:(\exists j:j\geq i:s_{j}\in S^{\prime})\)._  
Proof. : Let \(s_{i}\in(R_{p}-R)\). Any state that is not in \(R\) is in \(ms_{2}\). Thus, \((s_{i-1},s_{i})\in mt\). By construction, the program does not have any transition in \(mt\). Thus, \((s_{i-1},s_{i})\in f\cup\delta_{e}\). If \((s_{i-1},s_{i})\in f\), then \(s_{i-1}\in ms_{1}\) that is a contradiction to Lemma A5. Thus, \((s_{i-1},s_{i})\in\delta_{e}\). Since we have reached \(s_{i}\) by an environment transition and \(s_{i}\in R_{p}\), the computation will reach \(R\) and according to Lemma A6, the computation will reach \(S^{\prime}\). Based on Lemmas A6 and A7, we have the following corollary that guarantees recovery to the invariant from \(R\cup R_{p}\). :  
**Corollary A2**. : _For every \(\delta^{\prime}_{p}[]_{2}\delta_{e}[]f\) computation \(\langle s_{0},s_{1},\ldots\rangle\) such that \(s_{0}\in S^{\prime}\), for \(S^{\prime}\), \(R_{p}\) and \(R\) in the last iteration of loop on Lines 6-43, we have: \(\forall s_{i}:s_{i}\in R\cup R_{p}:(\exists j:j\geq i:s_{j}\in S^{\prime})\)._  
**Theorem A4**. : _Algorithm 3 is sound._  
Proof. : In order to show the soundness of our algorithm, we need to show that the three conditions of the problem statement are satisfied. **C1**: Satisfaction of **C1** for Algorithm 3 is the same as that for Algorithm 2 stated in the proof of the Theorem A1. **C2**: We need to show that \(p^{\prime}\) is a masking fault-tolerant revision for \(p\). Thus, we need to show the constraints of Definition 16 are satisfied. From **C1**, \(S^{\prime}\subseteq S\), the assumption that \(p[]_{2}\delta_{e}\) satisfies _spec_ from \(S\), \(S^{\prime}\
eq\emptyset\) and \(S^{\prime}\) is closed in \(p^{\prime}\cup\delta_{e}\), all constraints of Definition 10 are satisfied. Thus, \(p^{\prime}[]_{2}\delta_{e}\) 2-satisfies _spec_ from \(S^{\prime}\). Let \(spec=\langle Sf,Lv\rangle\). Consider prefix \(c\) of \(p^{\prime}[]_{2}\delta_{e}[]f\) such that \(c\) starts from a state in \(S^{\prime}\). If \(c\) does not satisfy \(Sf\), there exists a prefix of \(c\), say \(\langle s_{0},s_{1},\ldots,s_{n}\rangle\), such that it has a transition in \(\delta_{b}\). W.l.o.g., let \(\langle s_{0},s_{1},\cdots,s_{n}\rangle\) be the smallest such prefix. It follows that \((s_{n-1},s_{n})\in\delta_{b}\). Hence, \((s_{n-1},s_{n})\in mt\). By construction, \(p^{\prime}\) does not contain any transition in \(mt\). Thus, \((s_{n-1},s_{n})\) is a transition of \(f\) or \(\delta_{e}\). If it is in \(f\) then \(s_{n-1}\in ms_{1}\) which is a contradiction to Lemma A5. If it is in \(\delta_{e}\) then \(s_{n-1}\in ms_{2}\) and \((s_{n-2},s_{n-1})\in mt\). Again, by construction, we know that \(\delta^{\prime}_{p}\) does not contain any transition in \(mt\), so \((s_{n-2},s_{n-1})\) is either in \(f\) or \(\delta_{e}\). If it is in \(f\) then \(s_{n-2}\in ms_{1}\) (contradiction to Lemma A5). If it is in \(\delta_{e}\), as both \((s_{n-2},s_{n-1})\) and \((s_{n-1},s_{n})\) are in \(\delta_{e}\), according to the fairness assumption, there does not exist a transition of \(\delta^{\prime}_{p}\) starting from \(s_{n-1}\) and it means that \(s_{n-1}\in ms_{1}\), which is again a contradiction to Lemma A5. Thus, each prefix of \(c\) does not have a transition in \(\delta_{b}\).