\chapter{Modelverse State}
\label{sec:modelverse_state}
We start our specification with the Modelverse State (MvS).
The MvS maps the Physical Type Model (PGM) to the hardware.
Essentially, the MvS needs to implement the CRUD interface using whatever algorithms and data representation it sees fit.
Despite the liberal choice of data representation and algorithm, the interface is strictly defined and uses a special kind of graph, defined in this chapter.
We will first describe the conceptual representation of the PTM, followed by the operations on it that the MvS should support.

\section{Data representation}
Conceptually, all data in the MvS is stored in the form of a kind of graph, as defined below.
Informally, we define a graph which can have a primitive value in a node, and both nodes and edges can be connected using edges.
Allowing edges to connect other edges allows for a more explicit representation, such as type links on associations, (\axiomModelEverything).
While edges between edges could also be conceptualized using the standard notions of graphs, using tricks similar to hypergraphs, having a closer mapping between the PTM and the models will allow for higher performance (\axiomScalability).
Both nodes and edges can be accessed using a unique identifier.

An actual implementation of this interface might store the graph in different physical representations (\textit{e.g.}, using a relational database or triplestores).
This allows for more specialized implementations, depending on the problem domain (\axiomScalability), while still being interoperable (\axiomInteroperability).
Despite the need for multi-view (\axiomMultiView), multi-formalism (\axiomMultiFormalism), and multi-abstraction (\axiomMultiAbstraction), everything is represented uniformly at this level.
It is only at the Modelverse Kernel (MvK) level, that an interpretation is given to this graph.

We define a graph $G$, element of $\mathcal{G}$ (the set of all possible states of the MvS).
A graph consists of nodes ($N_G$), possibly with values (in $\mathbb{U}$) defined on them (mapping $N_{V,G}$), and edges (stored in $E_G$ as triples).
Edges can run between both nodes and edges.
All identifiers allocated to edges are stored in $E_{IDS,G}$.
Nodes and edges have a unique identifier, with $IDS_G$ being (exactly) the set of all identifiers.
This also means that identifiers cannot be reused between nodes and edges.

Edges which are self-connecting can be problematic for certain recursive algorithms, which traverse an edge by going on to the source and target.
Therefore, edges can, by construction, only link elements that already exist.
This effectively prevents (indirect) links to itself.
With this restriction, such constructs are disallowed and these recursive algorithms are therefore guaranteed to terminate.
Such a restriction is also not limiting, as it is a normal requirement to only connect elements that already exist.

The requirement for ever increasing identifiers might seem contradictory to \axiomForeverRunning, as the identifier would go up to infinity, consequently endangering \axiomScalability.
In theory, this is not a problem, though implementations will specifically have to handle this to prevent problematic situations (\textit{e.g.}, integer overflow or slow operations).
In an implementation, this could easily be solved by periodical \textit{``identifier compaction''} (identifiers are reassigned, to filter out removed identifiers), or reusing removed identifiers (keeping in mind the constraint).

\begin{gather*}
G = \langle N_G, E_G, N_{V,G} \rangle \in \mathcal{G}\\
n_i \in N_G \subseteq IDS_G \\
e_j \in E_G \subseteq IDS_G \times IDS_G \times IDS_G \\
N_{V,G} : N_G \rightarrow \mathbb{U} \\
E_{IDS,G} = \lbrace b \vert (a, b, c) \in E_G \rbrace \\
N_G \cap E_{IDS,G} = \emptyset \\
N_G \cup E_{IDS,G} = IDS_G \\
\forall e_i, e_j \in E : e_i = (a, b, c), e_j = (d, e, f), (b = e) \Rightarrow (e_i = e_j) \\
\forall e_i \in E : e_i = (a,b,c), (a < b) \land (c < b)
\end{gather*}

$\mathbb{U}$ defines the set of all possible values, or the union of all possible types:
$\mathbb{U} = \mathbb{I} \cup \mathbb{F} \cup \mathbb{S} \cup \mathbb{B} \cup \mathbb{A} \cup \Sigma_{type}$.
We define the following primitive types, supported in the PTM, for which the MvS needs to provide native support:
\begin{itemize}
\item \textbf{Integer} ($\mathbb{I}$) as the set of integers in the range $[-(2^{63}), 2^{63} - 1]$ (\textit{i.e.}, as would be available using 64-bit integers);
\item \textbf{Float} ($\mathbb{F}$) as the set of floating point numbers, as defined by IEEE 754, with double precision (\textit{i.e.}, as would be available using 64-bit floating point numbers). Values outside of this range will be rounded towards $-\infty$ or $\infty$;
\item \textbf{String} ($\mathbb{S}$) as the set of all ordered combinations of ASCII characters;
\item \textbf{Boolean} ($\mathbb{B}$) as either True or False;
\item \textbf{Action} ($\mathbb{A}$) as an action language construct ($\lbrace If, While, Assign, Call, Break, Continue, Return, Resolve, Access \rbrace$), used by the Modelverse Kernel to define the semantics.
\item \textbf{Type} ($\Sigma_{type}$) as the set of all supported types ($\lbrace IntType, FloatType, StringType, BooleanType, ActionType, TypeType \rbrace$).
These types differ from the set denoting all elements (\textit{i.e.}, $\mathbb{I}$ does not equal $IntType$), as the type is an instance itself.
\end{itemize}

We use $\mathbb{I}$ and $\mathbb{F}$, instead of $\mathbb{Z}$ and $\mathbb{R}$, respectively, because an implementation of these infinite concepts would not be able to exploit current hardware.
This is required for \axiomScalability, as otherwise primitive operations would be inefficient due to their generality.
With this restriction, we enforce the size of the data values, thus preventing implementation-dependent behaviour (\textit{e.g.}, some implementation using 32-bit integers, whereas another uses 64-bit integers).

The use of primitives does not violate \axiomModelEverything, as primitives will still be explicitly modelled in the linguistic dimension.
In the physical dimension however, we shift the representation of the data to the physical level to obtain higher performance (\axiomScalability) and to have a basic type system available.

None of the value sets overlap, therefore it is possible to infer the type of the data, using $N_T$.

\begin{gather*}
N_T : \mathbb{U} \rightarrow \Sigma_{type} \\
N_T(d) = \left\{ \begin{array}{rcl}
IntType     & if & d \in \mathbb{I} \\
FloatType   & if & d \in \mathbb{F} \\
StringType  & if & d \in \mathbb{S} \\
BooleanType & if & d \in \mathbb{B} \\
ActionType  & if & d \in \mathbb{A} \\
TypeType    & if & d \in \Sigma_{type} \\
\end{array}\right. \\
\forall i, j \in \lbrace \mathbb{I}, \mathbb{F}, \mathbb{S}, \mathbb{B}, \mathbb{A}, \Sigma_{type} \rbrace : i \neq j \Rightarrow i \cap j = \emptyset \\
\end{gather*}

We can define a subgraph ($M$) of a graph ($G$), as a graph containing a subset of the nodes and edges, with the restriction that all used nodes and node values are copied.
It is implicit that the resulting graph should still be valid according to the restrictions placed on the graph (\textit{e.g.}, source and target of nodes is still present).

\begin{gather*}
M \subseteq G \\
\Leftrightarrow \\
N_M \subseteq N_G \; \land \\
E_M \subseteq E_G \; \land \\
N_{V,M} \subseteq N_{V,G} \; \land \\
\forall (a \rightarrow b) \in N_{V,G} : a \in N_M \Rightarrow (a \rightarrow b) \in N_{V,M} \; \land \\
\forall (a, b, c) \in E_M : a, c \in IDS_M
\end{gather*}

\section{CRUD interface}
The final part of the PTM is the interface, or the set of its supported operations, which are defined here.
An MvS implementation needs to offer the operations defined here, irrespective of its implementation algorithm or data structure.
Of course, the implementation does not need to be using a graph similar to the conceptual representation of the PTM, but the operations should always return exactly the same result.

We distinguish four different kinds of operations in our interface: Create, Read, Update, and Delete (CRUD).
For each set of operations, we define the function signature and the required semantics.

Apart from the actual return value, operations also return a status.
This status is an integer specifying a status code: $S = \mathbb{I}$.
We have different categories of status codes: $1xx$ for success; $2xx$ for interface errors; and $3xx$ for execution errors.
An interface error indicates an error in the call, for example wrong type of arguments.
An execution error means that the call itself was well-formed, but could not be executed due to another restriction, such as an element not being defined.

All possible status codes are defined.
Some additional errors might happen in the MvS though, such as out-of-memory problems.
These errors are platform-dependent and are only caused due to the implementation, the hardware, or the combination of both.
As such, an MvS is not allowed to return such errors and needs to handle such situations gracefully.
For example, in the case of an out-of-memory error, the MvS needs to be able to swap out pieces of itself to disk, or over the network.

\subsection{Create}
The first set of instructions that we define are \textit{create} operations.
Create operations cause the creation of new elements in the graph, thus extending its size.
Each newly created element will be assigned an identifier by the MvS, which is returned.
It is this identifier which acts as the handle to that element in the MvS.

Note that there are no restrictions on the created identifier, apart from it being a value that is not yet used for another element.
This allows whatever kind of identifier to be used, and even reuse is possible if the previous element was deleted.

First is the create node operation ($C_N$), which takes no arguments and returns the identifier of the newly created node, which was unused up to now.

\begin{gather*}
C_N : \mathcal{G} \rightarrow \mathcal{G} \times N \times S \\
C_N(G) = (G', n, 100) \\
G = \langle N, E, N_V \rangle \\
G' = \langle N', E, N_V \rangle \\
N' = N \cup \lbrace n \rbrace \\
n \not\in IDS \\
\end{gather*}

The create edge operation ($C_E$) takes the identifier of the source and target elements (either a node or an edge) as argument, and returns the identifier of the newly created edge.

\begin{gather*}
C_E : \mathcal{G} \times IDS \times IDS \rightarrow \mathcal{G} \times E_{IDS} \times S \\
C_E(G, i_1, i_2) = (G', i_3, s) \\
G = \langle N, E, N_V \rangle \\
G' = \langle N, E', N_V \rangle \\
E' = E \cup \lbrace e_i \rbrace \\
e_i \not \in E \\
e_i = (i_1, i_3, i_2) \\
i_3 \not\in IDS \\
s \not = 100 \Leftrightarrow i_3 = None \\
s = \left\{ \begin{array}{rcl}
    200 & if    & i_1 \not \in IDS \\
    201 & if    & i_2 \not \in IDS \\
    100 & else                     \\
\end{array}
\right.
\end{gather*}

The last primitive create operation ($C_{NV}$) creates a new node, and assigns it a value immediately.
It has the same signature as the create node, but takes a primitive value to assign to the created node.
This operation could be implemented by first creating an empty node and afterwards updating its value, though this would negatively impact performance (\axiomScalability).

\begin{gather*}
C_{NV} : \mathcal{G} \times \mathbb{U} \rightarrow \mathcal{G} \times N \times S \\
C_{NV}(G, d) = (G', i, s) \\
G = \langle N, E, N_V \rangle \\
G' = \langle N', E, N'_V \rangle \\
N' = N \cup \lbrace i \rbrace \\
N'_V = N_V \cup ( i \rightarrow d ) \\
i \not \in N \\
s = \left\{ \begin{array}{rcl}
    202 & if    & d \not \in \mathbb{U} \\
    100 & if    & else                        \\
\end{array}
\right.
\end{gather*}

For performance, we add a composite create operation, which creates a named edge between two graph elements ($C_{D}$).
This operation is equivalent to creating an edge between the two elements, followed by creating an edge from the newly created edge, to the data value that was specified.
It is formalised as follows.

\begin{gather*}
C_{D} : \mathcal{G} \times IDS \times \mathbb{U} \times IDS \rightarrow \mathcal{G} \times S \\
C_{D}(G, a, d, b) = (G', s) \\
G = \langle N, E, N_V \rangle \\
G' = \langle N', E', N'_V \rangle \\
N' = N \cup \lbrace c \rbrace \\
E' = E \cup \lbrace (a, i_1, b), (i_1, i_2, c) \rbrace \\
N'_V = N_V \cup \lbrace (c \rightarrow d) \rbrace \\
c, i_1, i_2 \not \in IDS \\
s = \left\{ \begin{array}{rcl}
    203 & if    & a \not \in IDS \\
    204 & if    & d \not \in \mathbb{U} \\
    205 & if    & b \not \in IDS \\
    100 & if    & else \\
\end{array}
\right.
\end{gather*}

\subsection{Read}
The next set of operations consists of the read operations.
As there is no useful information in non-data nodes, there is no read operation defined on nodes, except for their primitive data ($R_V$).
It is an error if the node that is being read does not have a value assigned to it.

\begin{gather*}
R_V : \mathcal{G} \times N \rightarrow \mathbb{U} \times S \\
R_V(G, n) = (d, s) \\
G = \langle N, E, N_V \rangle \\
d = N_V(n) \\
s = \left\{
\begin{array}{rll}
    206 & if    & n \not \in N \\
    300 & if    & n \not \in dom(N_V) \\
    100 & else  & \\
\end{array}
\right.
\end{gather*}

Instead of a read operation on the nodes, it is possible to read out their outgoing edges ($R_O$) and incoming edges ($R_I$).
This works for nodes, but also for edges, as edges can also be the source (and target) of other edges.
The result is the identifier of the connected edges, in an unordered collection.

\begin{gather*}
R_O : \mathcal{G} \times IDS \rightarrow 2^E \times S \\
R_O(G, i) = (e, s) \\
G = \langle N, E, N_V \rangle \\
e = \lbrace (i, b, c) \in E \rbrace \\
s = \left\{ \begin{array}{rcl}
    207 & if    & i \not \in IDS \\
    100 & if    & else           \\
\end{array}
\right.
\end{gather*}

\begin{gather*}
R_I : \mathcal{G} \times IDS \rightarrow 2^E \times S \\
R_I(G, i) = (e, s) \\
G = \langle N, E, N_V \rangle \\
e = \lbrace (a, b, i) \in E \rbrace \\
s = \left\{ \begin{array}{rcl}
    208 & if    & i \not \in IDS \\
    100 & if    & else           \\
\end{array}
\right.
\end{gather*}

A read operation for edges ($R_E$) is defined as returning a tuple consisting of the source and target of the edge.
Due to the restriction on the edge identifier, both the source and target identifier will be smaller than the edge identifier.

\begin{gather*}
R_E : \mathcal{G} \times E_{IDS} \rightarrow IDS \times IDS \times S \\
R_E(G, i_1) = (i_2, i_3, s) \\
G = \langle N, E, N_V \rangle \\
e = (i_2, i_1, i_3) \in E \\
s = \left\{ \begin{array}{rcl}
    209 & if    & i_1 \not \in E_{IDS} \\
    100 & if    & else           \\
\end{array}
\right.
\end{gather*}

For efficiency (\axiomScalability), an additional \textit{``dictionary read''} operation ($R_{dict}$) is defined to read an element which is linked to another one through an edge, which is connected to a node with a primitive value.
This allows for a more efficient implementation of lookups from a specific node, without requiring an exhaustive search of the connected edges.
While the search might still be necessary internally, implementations are free to create specialized data structures for this operation.
Even if that is not the case, this operation reduces the amount of calls required to 1.
Two errors are possible: if the specified entry could not be found in the dictionary, and if a matched link also has other outgoing links, causing ambiguity as to which element is the key to use.

Notice that there is room for ambiguity if a node has multiple outgoing links, linking to the same data value.
While this could cause an error, we explicitly allow for this situation for performance reasons, as otherwise the search would always need to traverse all links, even if a match was already found.

\begin{gather*}
R_{dict} : \mathcal{G} \times IDS \times \mathbb{U} \rightarrow IDS \times S \\
R_{dict}(G, i_1, v) = (i_2, s) \\
G = \langle N, E, N_V \rangle \\
d = N_V(v) \\
\exists b, c \in E_{IDS}: (i_1, b, i_2), (b, c, d) \in E \\
s = \left\{
\begin{array}{rll}
    210 & if    & i_1 \not \in IDS \\
    211 & if    & v \not \in \mathbb{U} \\
    301 & if    & \not \exists b, c \in E_{IDS}: (i_1, b, i_2), (b, c, d) \in E \\
    302 & if    & \exists b, c, e, f \in E_{IDS}: (i_1, b, i_2), (b, c, d), (b, f, e) \in E \land c \neq f \\
    100 & else  & \\
\end{array}
\right.
\end{gather*}

Some other, more complex read operations on dictionaries are also supported, purely for efficiency reasons.
Their errors are similar to the $R_{dict}$ operation.
Each of these operations returns a slightly different result, determined by the frequently used operations in the next section.
These operations are:
\begin{itemize}
\item $R_{dict\_node}$ returns the element being linked to, but instead of a primitive value, it searches for a specific element by identifier.
It therefore does not try to dereference the value stored in the resulting element, nor will it match different elements with the same value.
\item $R_{dict\_edge}$ is equivalent as $R_{dict}$, but returns the identifier of the edge between them, instead of the element itself.
\item $R_{dict\_reverse}$ returns a list of all elements that have an outgoing link towards the passed element, with the provided name on that edge.
It is therefore basically a reverse dictionary lookup: return the dictionaries that contain this exact value with a specified key.
\end{itemize}

Multiple combinations would also be possible, though we only formalize those that are used by the MvK in later sections.

\begin{gather*}
R_{dict\_keys} : \mathcal{G} \times IDS \rightarrow 2^{IDS} \times S \\
R_{dict\_keys}(G, a) = (l, s) \\
G = \langle N, E, N_V \rangle \\
\forall b, c, d, e \in IDS: (a, b, c), (b, d, e) \in E : e \in l \\
s = \left\{
\begin{array}{rll}
    222 & if    & i_1 \not \in IDS \\
    100 & else  & \\
\end{array}
\right.
\end{gather*}

\begin{gather*}
R_{dict\_node} : \mathcal{G} \times IDS \times IDS \rightarrow IDS \times S \\
R_{dict\_node}(G, i_1, i_2) = (i_3, s) \\
G = \langle N, E, N_V \rangle \\
\exists b, c \in E_{IDS}: (i_1, b, i_3), (b, c, i_2) \in E \\
s = \left\{
\begin{array}{rll}
    212 & if    & i_1 \not \in IDS \\
    213 & if    & i_2 \not \in IDS \\
    303 & if    & \not \exists b, c \in E_{IDS}: (i_1, b, i_3), (b, c, i_2) \in E \\
    304 & if    & \exists b, c, e, f \in E_{IDS}: (i_1, b, i_3), (b, c, i_2), (b, e, f) \in E \land c \neq f \\
    100 & else  & \\
\end{array}
\right.
\end{gather*}

\begin{gather*}
R_{dict\_edge} : \mathcal{G} \times IDS \times \mathbb{U} \rightarrow IDS \times S \\
R_{dict\_edge}(G, i_1, v) = (i_2, s) \\
G = \langle N, E, N_V \rangle \\
d = N_V(v) \\
\exists b, c \in E_{IDS}: (i_1, i_2, b), (i_2, c, d) \in E \\
s = \left\{
\begin{array}{rll}
    214 & if    & i_1 \not \in IDS \\
    215 & if    & v \not \in \mathbb{U} \\
    305 & if    & \not \exists b, c \in E_{IDS}: (i_1, i_2, b), (i_2, c, d) \in E \\
    306 & if    & \exists b, c, e, f \in E_{IDS}: (i_1, i_2, b), (i_2, c, d), (i_2, f, e) \in E \land c \neq f \\
    100 & else  & \\
\end{array}
\right.
\end{gather*}

\begin{gather*}
R_{dict\_node\_edge} : \mathcal{G} \times IDS \times IDS \rightarrow IDS \times S \\
R_{dict\_node\_edge}(G, i_1, i_2) = (b, s) \\
G = \langle N, E, N_V \rangle \\
\exists b, c \in E_{IDS}: (i_1, b, i_3), (b, c, i_2) \in E \\
s = \left\{
\begin{array}{rll}
    216 & if    & i_1 \not \in IDS \\
    217 & if    & i_2 \not \in IDS \\
    307 & if    & \not \exists b, c \in E_{IDS}: (i_1, b, i_3), (b, c, i_2) \in E \\
    308 & if    & \exists b, c, e, f \in E_{IDS}: (i_1, b, i_3), (b, c, i_2), (b, e, f) \in E \land c \neq f \\
    100 & else  & \\
\end{array}
\right.
\end{gather*}

\begin{gather*}
R_{dict\_reverse} : \mathcal{G} \times IDS \times \mathbb{U} \rightarrow 2^{IDS} \times S \\
R_{dict\_}(G, i_1, v) = (l, s) \\
G = \langle N, E, N_V \rangle \\
d = N_V(v) \\
l = \lbrace i_2 : \exists b \in E_{IDS} . (i_2, b, i_1), (b, c, d) \in E \rbrace\\
s = \left\{
\begin{array}{rll}
    218 & if    & i_1 \not \in IDS \\
    219 & if    & v \not \in \mathbb{U} \\
    309 & if    & \not \exists b, c \in E_{IDS}: (i_1, b, i_2), (b, c, d) \in E \\
    310 & if    & \exists b, c, e, f \in E_{IDS}: (i_1, b, i_2), (b, c, d), (b, f, e) \in E \land c \neq f \\
    100 & else  & \\
\end{array}
\right.
\end{gather*}

\subsection{Update}
Even though we implement a CRUD interface, we do not offer support for any update operations.

The most important reason is correctness and performance.
Updating the source and target of edges has the potential of creating impossible loops, like an edge connecting itself.
While this is impossible to do when constructing the edge at first (as it is required that its source and target already exist), this can no longer be guaranteed when the edge is updated.
An alternative would be to allow updates, but search for correctness violations (\textit{i.e.}, recursively following the source and target of an edge, we ultimately end up in nodes) after the update was done.
This would have a significant, and unpredictable, impact on performance when performing an update for an edge.
As an update operation is similar to a subsequent create and delete, which have better complexity, we did not think this is a viable approach.
Yet another alternative would be to allow updates again, but only those updates that change the source and target to nodes that existed when the edge was originally created.
This prevents correctness violations by construction, though it does not make the operation generally applicable.
And since we would need to have a fallback method (\textit{i.e.}, subsequent delete and create) anyway, it might be easier to just always use the fallback method.
This also prevents us having to store some kind of causality information, like which elements were created before which other elements.

Another reason is cache management, as also proposed by~\cite{WebGME}.
If a node can be updated, caches can become invalid, implying some kind of MvS-initiated invalidation protocol for the MvK.
While we do not have any significant optimization for this yet, restricting updates has significant potential.

\subsection{Delete}
Finally there are the \textit{delete} operations.
The source and target of each edge should always exist in the graph.
Therefore, if a deleted node or edge is the source or target of an edge, the edge needs to be recursively removed.
The resulting graph should thus be the largest possible subgraph of the original graph, while still being a valid graph.
For the delete node operation ($D_N$), the node itself is removed, and then all connected edges are recursively removed.

\begin{gather*}
D_N : \mathcal{G} \times N \rightarrow \mathcal{G} \times S \\
D_N(G, i) = (G', s) \\
G = \langle N, E, N_V \rangle \\
G' = \langle N', E', N'_V \rangle \\
N' = N \setminus \lbrace i \rbrace \\
G' \subseteq G \\
\forall G'' \subseteq G : (G' \subseteq G'') \Rightarrow G' = G'' \\
s = \left\{
\begin{array}{llr}
220 & if    & i \not \in N \\
100 & else  &                   
\end{array}
\right.
\end{gather*}

The delete edge operation ($D_E$) operation is similar, but it is guaranteed that no nodes are removed at all.
Due to recursive deletions, the resulting set of edges is possibly a subset of the original edges.
The resulting graph is again the largest possible (valid) subgraph, with the specified edge removed.

\begin{gather*}
D_E : \mathcal{G} \times E_{IDS} \rightarrow \mathcal{G} \times S \\
D_E(G, i) = (G', s) \\
G = \langle N, E, N_V \rangle \\
G' = \langle N, E', N'_V \rangle \\
E' \subseteq E \setminus \lbrace (a, i, c) \in E \rbrace \\
G' \subseteq G \\
\forall G'' \subseteq G : (G' \subseteq G'') \Rightarrow G' = G'' \\
s = \left\{
\begin{array}{llr}
221 & if    & i \not \in E_{IDS} \\
100 & else  &                   
\end{array}
\right.
\end{gather*}

