# Union Models for Model Families: Efficient Reasoning over Space and Time
## 6 Analysis and Reasoning with Model Families
### Analysis and Experiments
#### 6.2.2 Implementation  
To validate our approach, we used the NetworkX 2.2 Python library [26] to implement attributed typed graphs (according to Definition 5); we implemented our own union algorithm on top of that library to construct \(M_{U}\) (based on Definitions 9 and 11). NetworkX 2.2 is a Python package for the creation, manipulation, and study of the structure, dynamics, and functions of complex graphs [26]. It is enriched with a variety of features, from the support of graph data structures and algorithms to analysis measures to visualization options. To ensure that we had a family of state machine models, NetworkX's graph generator was applied to randomly generate valid attributed typed graphs with different _SIZE_ and _INDV_ parameters. These graphs corresponded to typed state machines with _likely evolutions_, i.e., a sequence of random but typical manipulations on state machine models that lead to different versions. A sample of the generated graphs was manually checked to make sure that we had generated likely changes to existing models rather than generating completely independent models. Due to the completely random nature of the graph generators, we found that although the amount of changes in state machine models could be controlled, the topology of the resulting graph could not; that is, the same node in a model could change its incoming and/or outgoing edges randomly, leading to a different model. Such deviations between individual models can lead to a union model with large variations, indicated by the number of annotations on each element. Although this is not the best or even the typical case of state machine model families, we decided to perform experiments on the generated \begin{table}
\begin{tabular}{c c c c c} \hline \hline \#**Elements/Model** & **(0, 30]** & **(30, 110]** & **(110, 420]** & **(420, 1640]** \\ \hline Exemplar & 12 & 56 & 240 & 930 \\ Category & S & M & L & XL \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Categories of SIZE parameter (number of elements in a model). \begin{table}
\begin{tabular}{c c c c} \hline \hline \#**Indiv.** & **(0, 20]** & **(20, 72]** & **(72, 156]** & **(156, 272]** \\ \hline Exemplar & 6 & 42 & 110 & 210 \\ Category & S & M & L & XL \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Categories of INDV parameter (number of individual members in a family). models in order to examine the complex families, for which the performance is unlikely to be worse. For GRL models, the generation of models was less random; we took a set of real GRL models of smart homes published in [12] as a starting point and enlarged them according to the different combinations of the _SIZE_ and _INDV_ parameters. While growing the models, we created a set of random realistic modifications that involved adding and/or deleting intentional elements and/or element links or modifying their attributes. We then constructed \(\mathrm{G_{U}}\) from the generated graphs using our union algorithm. \(\mathrm{G_{U}}\) is the union of a set of typed graphs; hence, \(\mathrm{G_{U}}\) corresponds to \(M_{U}\). It is worth mentioning here that the random generation of graphs was only used to check the scalability of the approach in order to provide a proof of concept for the suggested approach. Properties checked on such random graphs may be satisfied or not; this is not important here as long as the results for the model family are the same as the results for individual models, which is the case here. For RT1, we checked the cyclic composition property inspired by [23], which ensures that the model does not contain self-looping edges. A propositional formula (\(\Phi p=\{\forall e:E_{G},src_{G}(e)\
eq tgt_{G}(e)\}\)) was generated for this property. The propositional encodings were generated according to the rules discussed in Section 5, and were fed as literals to the _MiniSAT_ solver included in the _SATisPY_ package [27]. SATisPy is a Python library that provides an interface for various SAT solver applications.