# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## Appendix A Soundness, Completeness and Complexity of Algorithm 2
### Soundness
Regarding the third requirement of Lemma A.1, suppose that there exists \(s_{1}\) in \(S^{\prime}\) such that \(\big{(}\exists s_{0},s_{2},s_{3}:s_{0}\in S^{\prime}\wedge(s_{0},s_{1}),(s_{1},s_{2})\in\delta_{e}\wedge(s_{1},s_{3})\in\delta_{p}\big{)}\) but \(\
exists_{4}::(s_{1},s_{4})\in\delta^{\prime}_{p}\). From \(\exists s_{2},s_{3}::(s_{1},s_{2})\in\delta_{e}\wedge(s_{1},s_{3})\in\delta_{p}\) and \(\
exists_{4}::(s_{1},s_{4})\in\delta^{\prime}_{p}\) we can conclude that \(s_{1}\) is in \(ms_{3}\). Then, from \((s_{0},s_{1})\in\delta_{e}\), we know that \(s_{0}\) is in \(ms_{4}\), which is contradiction as \(s_{0}\) is in \(S\). Finally, the fourth condition is satisfied by the fact that \(S^{\prime}\) does not include any deadlock state. Since all conditions of Lemma A.1 are satisfied, condition \(C1\) holds. **C2**: We need to show that \(p^{\prime}\) is a failsafe fault-tolerant revision for \(p\). Thus, we need to show constraints of Definition 15 are satisfied. From \(C1\), \(S^{\prime}\subseteq S\), the assumption that \(p\big{[}\!\big{]}_{2}\delta_{e}\) satisfies _spec_ from \(S\), \(S^{\prime}\
eq\emptyset\) and \(S^{\prime}\) is closed in \(p^{\prime}\cup\delta_{e}\), all constrains of Definition 10 are satisfied. Thus, \(p^{\prime}\big{[}\!\big{]}_{2}\delta_{e}\) 2-satisfies _spec_ from \(S^{\prime}\). Let _spec_ be \(\langle Sf,Lv\rangle\). Consider prefix \(c\) of \(p^{\prime}\big{[}\!\big{]}_{2}\delta_{e}\big{[}\!\big{]}f\) such that \(c\) starts from a state in \(S^{\prime}\). If \(c\) does not satisfy \(Sf\) then 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},\ldots,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\). Byconstruction, \(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}\) (i.e., \(s_{n-1}\in ms_{2}\)). If it is in \(\delta_{e}\) then \(s_{n-1}\in ms_{2}\). Therefore, in both cases, \(s_{n-1}\in ms_{2}\) and \((s_{n-2},s_{n-1})\in mt\). Again, by construction, we know that \(\delta_{p}^{\prime}\) 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}\) (i.e., \(s_{n-2}\in ms_{2}\)). If it is in \(\delta_{e}\) two cases are possible:  
(1) \((s_{n-1},s_{n})\in f\). In this case, as stated before, \(s_{n-1}\in ms_{1}\), so \(s_{n-2}\in ms_{2}\). (2) \((s_{n-1},s_{n})\in\delta_{e}\). Since \((s_{n-1},s_{n})\in\delta_{e}\cap\delta_{b}\), from the fact the original program satisfies \(spec\) from \(S\), we conclude that \(s_{n-1}\
otin S\) (i.e., \(s_{n-1}\
otin S^{\prime}\)). In this case, all transitions starting from \(s_{n-1}\) should be in \(mt\). If this is not the case then this implies that there exists a state \(s\) such that \((s_{n-1},s)\) is not in \(mt\) and we would have added it to \(\delta_{p}^{\prime}\) by Line 22, as \(S_{n-1}\) is outside \(S^{\prime}\). Since all transitions from \(s_{n-1}\) are in \(mt\), \(s_{n-1}\) is in \(ms_{1}\) (by Line 7). Hence, \(s_{n-2}\) is in \(ms_{2}\). Continuing this argument further leads to the conclusion that \(s_{0}\in ms_{2}\). This is a contradiction, as we know \(S^{\prime}\) does not include any state in \(ms_{2}\). Thus, any prefix of \(p^{\prime}[]2\delta_{e}[]f\) satisfies \(Sf\). Thus, \(C2\) holds. **C3**: Any \((s_{0},s_{1})\in\delta_{r}\), is in \(mt\). By construction, \(\delta_{p}^{\prime}\) does not have any transition in \(mt\). Hence, \(C3\) holds.