# Union Models for Model Families: Efficient Reasoning over Space and Time
## 5 Propositional Encoding Language with Annotations (PELA)
### Definitions  
The propositional encoding of models using PELA is defined as follows:  
Definition 9: **ElementToPropositionWithAnnotation**: Given a model \(M=(G\), type, ATG), where \(G=(N_{G}\), \(N_{D}\), \(E_{G}\), \(E_{NA}\), \((\text{src}_{j}\), \(\text{tgt}_{j})\), \(j\in\{G\), \(NA\), \(EA\})\) (see Definition 6), together with \begin{table}
\begin{tabular}{c c} \hline \hline
**Config** & **Description** \\ \hline TYPE1 & Size = M, Location = Ontario, Flight = national \\ TYPE2 & Size = L, Location = Ontario, Flight = international \\ TYPE3 & Size = M, Location = Quebec, Flight = national \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Mapping configurations to their detailed descriptions. a STAL annotation specifying version numbers and configuration information, the mapping of elements of \(M\) into propositions with annotation ElementToPropositionWithAnnotation(elem) is defined according the following syntactical rules (along with their semantics):_  
* _A graph node_ \(n\in N_{G}\) _of type_ \(t\in N_{\text{ATG}}\) _is mapped into a propositional variable \"_\(t\)_-_\(\mathit{cver}_{\text{num}}\)_,_ \(\mathit{conf}_{\text{info}}\)_>\" to express the semantics: \"a model (with_ \(\mathit{ver}_{\text{num}}\) _and_ \(\mathit{conf}_{\text{info}}\)_) contains a node_ \(n\) _of type_ \(t\)_\". Formally:_ \(n\)_-_\(t\) _iff_ \(\exists n\in N_{G}\wedge\mathit{type}(n)=t\)_._
* _A graph edge_ \(e\in E_{G}\) _of type_ \(t\in E_{\text{ATG}}\) _with source node_ \(x\) _and target node_ \(y\) _is mapped into a propositional variable \"_\(e\)_-_\(x\)_-_\(y\)_-_\(t\)_-_\(\mathit{cver}_{\text{num}}\)_,_ \(\mathit{conf}_{\text{info}}\)_>\" to express the semantics: \"a model (with_ \(\mathit{ver}_{\text{num}}\) _and_ \(\mathit{conf}_{\text{info}}\)_) contains an edge_ \(e\) _of type_ \(t\) _from node_ \(x\) _to node_ \(y\)_\". Formally:_ \(e\)_-_\(x\)_-_\(y\)_-_\(t\)_ iff_ \(\exists e\in E_{G}\wedge\mathit{type}(e)=t\wedge\mathit{src}_{G}(e)=x\wedge \mathit{tgt}_{G}(e)=y\)_._
* _A data node_ \(dn\in N_{D}\) _of type_ \(t\in\mathit{dataType}\) _owned by a graph node_ \(n\in N_{G}\) _is mapped into a propositional variable \"_\(dn\)_-_\(n\)_-_\(t\)_-_\(\mathit{cver}_{\text{num}}\)_,_ \(\mathit{conf}_{\text{info}}\)_>\" to express the semantics: \"a model (with_ \(\mathit{ver}_{\text{num}}\) _and_ \(\mathit{conf}_{\text{info}}\)_) contains a node_ \(n\) _that owns a data node_ \(dn\) _of type_ \(t\)_\". Formally:_ \(dn\)_-_\(t\)_-_\(\mathit{iff}\)_ \(\exists n\in N_{G}\wedge\mathit{owner}(dn)=n\wedge\mathit{type}(dn)=t\)_._
* _A node attribute edge_ \(n\in E_{\text{NA}}\) _of type_ \(t\in\mathit{attribute\_name}\) _that is represented as a special edge between a graph node_ \(n\in N_{G}\) _and a data node_ \(dn\in N_{D}\)_, where_ \(n\) _is also the owner of that attribute, is mapped into a propositional variable \"_\(n\)_-_\(n\)_-_\(dn\)_-_\(t\)_-_\(\mathit{cver}_{\text{num}}\)_,_ \(\mathit{conf}_{\text{info}}\)_>\" to express the semantics: \"a model (with_ \(\mathit{ver}_{\text{num}}\) _and_ \(\mathit{conf}_{\text{info}}\)_) contains a node_ \(n\) _which owns an attribute_ _na of type_ \(t\)_, and this_ _na_ _ise is represented as an edge from graph node_ \(n\) _to data node_ \(dn\)_\". Formally:_ \(n\)_-_\(n\)_-_\(tn\)_-_\(t\)_iff_ \(\exists n\in E_{\text{NA}}\wedge\mathit{owner}(n\text{ne})=n\wedge\mathit{ type}(n\text{ne})=t\wedge\mathit{src}(n\text{ne})=n\ \wedge\mathit{tgt}(n\text{ne})=dn\)_. It is worth clarifying that the \"_\(n\)_-_\(n\)_\" part in the pattern_ \(n\)_-_\(n\)_-_\(dn\)_-_\(t\)_ represents the same element_ \(n\)_. The first_ \(n\) _indicates the owner of the attribute, and the second_ \(n\) _indicates that this owner is also a source of the edge.