# An Actor-Based Formal Model and Runtime Environment for Resource-Bounded IoT Services +
## 4 Operational Semantics
### Transition Rules
#### 4.2.5 Creating a New Service  
Here, we present the composition of running contributing services to create a new service based on the definition of \(\rho\).  
Consider a function _create_: When providing as parameters a service request \(\rho\); a set of contributing services, \(S_{\rho}\), which could collectively contribute to serving \(\rho\); and the name of the client service \(s\) requesting \(\rho\), _create_ creates a new service which satisfies \(\rho\)'s requirements. Then, the _create_ function returns the name of the newly created service \(s^{\prime}\), and a set of contracts \(C_{\rho}\) between \(s^{\prime}\) and \(S_{\rho}\). The _create_ function is defined as follows:  
\[create(\rho,S_{\rho},s)=(\{s^{\prime}\},C_{\rho},c) \tag{9}\]  
If there exist contributing services whose feeds are sufficient for generating \(\rho\), then the service request is accepted. This operation is shown in the following:  
\[\begin{split} search(\rho,s)\xrightarrow{\lambda}_{X}(S_{\rho}, \emptyset)\Rightarrow\\ \langle\llbracket I:\ [R[search(\rho,s)]]_{a_{s_{d}}},\ \alpha:O]_{s_{d}},\ S\mid C\mid M \rangle\rightarrow\\ \langle\llbracket I:\ [R[(S_{\rho},\emptyset)]]_{a_{s_{d}}},\ \alpha:O]_{s_{d}},\ S\mid C\mid M\rangle \end{split} \tag{10}\]  
where \(X=\{a_{s_{d}}\}\) is the context in which \(search(\rho,s)\) is reduced to \((S_{\rho},\emptyset)\), \(s_{d}\) is the directory service, \(a_{s_{d}}\) is \(s_{d}\)'s coordinator actor, \(\rho\) is the service request, and \(s\) is the name of the client service which sent \(\rho\). This transition happens if and only if \(search(\rho,s)\) is evaluated to \((S_{\rho},\emptyset)\).  
The directory service then uses the _create_ function to create a new service utilizing the contributing services. The transition rule for creating a new service is as follows:  
\[\begin{split} create(\rho,S_{\rho},s)\xrightarrow{\lambda}_{X}( \{s^{\prime}\},C_{\rho},c)\Rightarrow\\ \langle\llbracket I:[R[create(\rho,S_{\rho},s)]]_{a_{s_{d}}}, \alpha:O]_{s_{d}},S\mid C\mid M\rangle\rightarrow\\ \langle\llbracket I:[R[(s^{\prime}),C_{\rho},c)]\rrbracket_{a_{s_{d }}},\alpha:O]_{s_{d}},S^{\prime}\mid C^{\prime}\mid\langle s\Leftarrow s^{ \prime}\rangle,M\rangle\end{split} \tag{11}\]  
\[\begin{split}&\{s^{\prime}\}\,\ C_{\rho}\ \text{and}\ c\ \text{are fresh}\end{split}\]where \(X=\{a_{s_{d}}\}\) is the context in which \(create(\rho,S_{\rho},s)\) is reduced to \((\{s^{\prime}\},C_{\rho},c)\); \(s_{d}\) is the directory service; \(a_{s_{d}}\) is \(s_{d}\)'s coordinator actor; \(s\) is the client service which sent the service request \(\rho\); \(s^{\prime}\) is the newly created service producing \(\rho\) from \(C_{\rho}\)'s contributions; \(C_{\rho}\) is a new set of contracts created between \(s^{\prime}\) and \(S_{\rho}\); \(c\) is a new contract created between \(s^{\prime}\) and \(s\), which has the form \((s^{\prime},\ s,\ (o_{\sigma}\ ;\ i_{s}))\) where \(o_{\sigma^{\prime}}\in O_{\sigma^{\prime}}\) is an output port of \(s^{\prime}\) and \(i_{s}\in I_{s}\) is an input port of \(s\); \(C^{\prime}=C\ \cup\ C_{\rho}\ \cup\ \{c\}\); and \(S^{\prime}=S\cup\{s^{\prime}\}\). This transition happens if and only if \(search(\rho,s)\) is evaluated to \((S_{\rho},\emptyset)\). This leads to the creation of message \(\langle s\Leftarrow s^{\prime}\rangle\) containing the name of the new service \(s^{\prime}\), the creation of new sets of contracts \(C_{\rho}\) and \(\{c\}\), and the creation of a new service \(s^{\prime}\) on the right hand side.