# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 6 Experimental Results
### Addition of Stabilization
#### 6.1.1 One-Dimensional Stabilizing Shepherding Problem  
In this section, we focus on the shepherding problem introduced in Section 1. We first consider the one-dimensional version of the problem where both farmer and the sheep move in a line. Thus, we have a row of \(n\) cells that the sheep/farmer can be in. Thus, we have two variables \(c_{f}\) and \(c_{s}\) which represent the location of the farmer and the sheep, respectively (see Figure 5). The farmer and the sheep can change their location at most by one cell at a time.  
The rightmost cell is marked as the desired location. The farmer wants to steer the sheep to this cell. Thus, the invariant for the problem is \(\{s|c_{s}(s)=n-1\}\), where \(n\) is the number of cells in the row. The sheep always tries to increase its distance with the farmer. When the farmer and the sheep are in the same location, the sheep non-deterministically decides to go to the right or left, if it has space in  
Figure 5: An example state of an 1D shepherding problem with \(n=6\). In this example, \(c_{f}=1\) and \(c_{s}=n-2\).  
its both left and right. When the sheep is in the desired location, it stops moving further. With this explanation, the set of environment transitions is  
\[\delta_{e}=\Big{\{}(s_{0},s_{1})|c_{s}(s_{0})\
eq n-1\wedge c_{f}(s _{0})=c_{f}(s_{1})\wedge\] \[\Big{(}(c_{f}(s_{0})<c_{s}(s_{0})\wedge c_{s}(s_{0})<n-1\wedge c_{ s}(s_{1})=c_{s}(s_{0})+1)\vee\] \[\big{(}c_{f}(s_{0})>c_{s}(s_{0})\wedge c_{s}(s_{0})>0\wedge c_{s}( s_{1})=c_{s}(s_{0})-1\big{)}\vee\] \[\big{(}c_{f}(s_{0})=c_{s}(s_{0})\wedge c_{s}(s_{0})<n-1\wedge c_{ s}(s_{1})=c_{s}(s_{0})+1\big{)}\vee\] \[\big{(}c_{f}(s_{0})=c_{s}(s_{0})\wedge c_{s}(s_{0})>0\wedge c_{s}( s_{1})=c_{s}(s_{0})-1\big{)}\Big{)}\Big{\}}\]  
Also, since the farmer cannot move more than one cell in one step, the set of program restrictions is  
\[\delta_{r}=\{(s_{0},s_{1})|\ |c_{f}(s_{0})-c_{f}(s_{1})|>1\}.\]  
Because of the non-determinism in the movement of the sheep, a program for the farmer can go into an infinite loop such that it never reaches the goal state. To understand how that can happen, consider this scenario: suppose both farmer and sheep are in the cell 0. Since the left side of the sheep is closed, it can only move to the right. Thus, it moves to the second cell. Now, suppose the farmer also decides to go to the second cell. Thus, again both of them are in the same cell. However, this time, since the left side of the sheep is open, it may decide to go there. Suppose sheep decides to go the left cell. Then, the farmer also goes back to the first cell. Once again, they are both in the first cell and the same scenario can repeat forever. A correct program for the farmer utilizes the behavior of the sheep, while avoiding going into an infinite loop and steers the sheep to the desired location.  
We modeled this problem using JavaScript for different sizes. We used a program with an empty set of transitions as the input program. Algorithm 1 successfully adds stabilization to the given program. Table 1 shows the repair time for different sizes.