# Formal Algebraic Model of an Edge Data Center with a Redundant Ring Topology
## 6 Formal Algebraic Model
Supposing a given node \(x\), such as \(V_{x}\), that being the source node of a migration, then the traffic flow associated to such an action may head for its successor if the node destination is \(y=(x+1)_{|n}\), whereas it may lead to its predecessor if the node destination is \(y=(x-1)_{|n}\), or otherwise, it may go any way if the node destination is \(y=(x+2)_{|n}\), as both paths, namely clockwise and counterclockwise, are redundant with equal cost. Hence, the formal algebraic model for the resource migration take all three possibilities, as exhibited in (13) for the node source \(V_{x}\) and in (14) for the node destination \(V_{y}\). Regarding verification, it is obvious that send and read action clearly match, thus verification of this model is analogous to the previous one. \[ \begin{split}& V_{x}=\sum_{x=0}^{n-1}\Big{(}\sum_{p=1}^{1}s_{x,p} (d)\triangleleft y=(x+1)_{|n}\triangleright\\ &\big{(}\sum_{p=2}^{3}s_{x,p}(d)\triangleleft y=(x-1)_{|n} \triangleright\sum_{p=0}^{3}s_{x,p}(d)\big{)}\Big{)}\end{split}  \tag{13}\]  
\[ \begin{split}& V_{y}=\sum_{y=0}^{n-1}\Big{(}\sum_{p=2}^{3}r_{y,p} (d)\triangleleft y=(x+1)_{|n}\triangleright\\ &\big{(}\sum_{p=0}^{1}r_{y,p}(d)\triangleleft y=(x-1)_{|n} \triangleright\sum_{p=0}^{3}r_{y,p}(d)\big{)}\Big{)}\end{split}  \tag{14}\]  
Additionally, some theorems could be derived from the aforementioned expressions in order to assure that the model works as expected. All incoming messages from the sensors which are processed by the brokers are redirected out of the system and applied to the actuators. Proof of Theorem 3.1.: Taking Equation (9), which exhibits the sequence of events of the model, it may be seen that information collected from the sensors in the environment \((\textit{env})\) are taken by either the pole \(i\)\((r_{\textit{env}\to i})\) or the drone \(j\)\((r_{\textit{env}\to i})\), which in turn sends a raw message \((d)\) to broker \(u\) (either \(c_{i\to u}\) or otherwise \(c_{j\to u}\)). At that point, if the broker is able to process the raw message (\(AI_{B}\) condition is true), then the raw message \((d)\) is transformed into the processed message \((e)\), meaning that such a message is not forwarded to the orchestrator \(v\), which is expressed by \(\emptyset\). Afterwards, the broker \(b\) sends the processed message \((e)\) to either the pole \(i\)\((c_{u\to i})\) or the drone \(j\)\((c_{u\to j})\), which in turn, is sent to the actuator so as to act on the environment \((\textit{env})\) as \((s_{i\to\textit{env}})\) or \((s_{j\to\textit{env}})\), respectively. All incoming messages from the sensors which are processed by the orchestrators are redirected out of the system and applied to the actuators. Proof of Theorem 3.2.: Keeping the focus on Equation (9), and following the explanation given in the previous theorem, if the broker \(u\) is not able to process the raw message (\(AI_{B}\) condition is false), then it is forwarded to the orchestrator \(v\)\((c_{u\to v})\). At that point, if the broker is able to process the raw message (\((AI_{O}\) condition is true), then the raw message \((d)\) is transformed into the processed message \((e)\), meaning that such a message is not forwarded to the cloud \(w\), which is expressed by \(\emptyset\). After that, the orchestrator \(v\) sends the processed message \((e)\) to the broker \(u\)\((c_{v\to u})\), and from that point on, it follows the explanation given in the previous theorem. All incoming messages from the sensors which are processed by the clouds are redirected out of the system and applied to the actuators. Proof of Theorem 3.3.: Sticking to Equation (9), and following the explanation given in the last theorem, if the orchestrator \(v\) is not able to process the raw message (\(AI_{O}\) condition is false), then it is forwarded to the cloud \(w\)\((c_{v\to w})\). At that point, the cloud is able to process the raw message (\(AI_{C}\) poses no condition, as it is always able to deal with raw data), then the raw message \((d)\) is transformed into the processed message \((e)\).