interaction rules subsection 3.1.2thesis

7 files changed, 1320 insertions, 2 deletions

diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex
index 36919e5..a6a69c5 100644
--- a/chapters/01-introduction.tex
+++ b/chapters/01-introduction.tex
@@ -28,7 +28,7 @@ The tool is divided into three steps:
 	\item \textbf{Reduction}: the interaction net gets reduced to its normal form by Inpla;
 	\item \textbf{Evaluation}: the normal form gets processed along with the property to verify by Z3.
 \end{itemize}
-Z3 is not optimized for ReLU splitting, but it was chosen for it's mature Python package.
+Z3 is not optimized for ReLU splitting, but it was chosen for its mature Python package.
 In any case a specialized solver like Marabou can be integrated to improve performance.
 Our contributions are:
 \begin{itemize}
diff --git a/chapters/03-core.tex b/chapters/03-core.tex
index 9369522..d8913d3 100644
--- a/chapters/03-core.tex
+++ b/chapters/03-core.tex
@@ -6,3 +6,5 @@
 \input{chapters/core/01-implementation}
 
 \input{chapters/core/02-soundness-proof}
+
+\input{chapters/core/03-benchmarks}
diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex
new file mode 100644
index 0000000..40c1986
--- /dev/null
+++ b/chapters/core/03-benchmarks.tex
@@ -0,0 +1,4 @@
+\section{Benchmarks}
+\label{sec:benchmarks}
+
+% This section contains the varius benchmarks
diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex
index bef0970..1cf4d26 100644
--- a/chapters/core/implementation/02-interaction-rules.tex
+++ b/chapters/core/implementation/02-interaction-rules.tex
@@ -1,4 +1,826 @@
 \subsection{Interaction Rules}
 \label{sec:interaction-rules}
 
-% This subsection talks about the interaction rules that implement the symbolic simplification
+This subsection contains the definition of the agents and the interaction rules that implement the symbolic simplification.
+
+The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into three groups:
+\begin{itemize}
+	\item
+		\textbf{Carriers}: Agents that contain float attributes.
+		\begin{itemize}
+			\item \textbf{Linear}: Represents the linear transformation $f(x) = q \cdot x + r$.
+			\item \textbf{Concrete}: Represents a constant value $k$.
+		\end{itemize}
+	\item
+		\textbf{Operators}: Agents that perform some kind of operation on the carrier agents.
+		\begin{itemize}
+			\item \textbf{Add}: Binary operator for addition.
+			\item \textbf{Mul}: Binary operator for multiplication.
+			\item \textbf{ReLU}: Unary operator for rectified linear unit.
+			\item \textbf{Eraser}: Built-in Inpla unary operator to delete other agents.
+			\item \textbf{Duplicator}: Built-in Inpla unary operator to duplicate other agents.
+		\end{itemize}
+	\item
+		\textbf{Intermediates}: Agents needed to perform each step of the operators.
+		\begin{itemize}
+			\item \textbf{AddCheckLinear}: Intermediate agent that memorizes the other Linear operand that needs to be added.
+			\item \textbf{AddCheckConcrete}: Intermediate agent that memorizes the other Concrete operand that needs to be added.
+			\item \textbf{MulCheckLinear}: Intermediate agent that memorizes the other Linear operand that needs to be multiplied.
+			\item \textbf{MulCheckConcrete}: Intermediate agent that memorizes the other Concrete operand that needs to be multiplied.
+			\item \textbf{Materialize}: Converts a Linear agent into an explicit representation for the SMT solver.
+		\end{itemize}
+	\item
+		\textbf{Inerts}: Agents that will compose the normal form.
+		\begin{itemize}
+			\item \textbf{TermAdd}: This agent that will be parsed as addition for the SMT solver.
+			\item \textbf{TermMul}: This agent that will be parsed as multiplication for the SMT solver.
+			\item \textbf{TermReLU}: This agent that will be parsed as rectified linear unit for the SMT solver.
+			\item \textbf{Symbolic}: This agent that will be parsed as specific variable for the SMT solver.
+		\end{itemize}
+\end{itemize}
+
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{cccc}
+			% Linear
+			\begin{tikzpicture}
+				\agentLinear{L}{q}{r}
+				\inetwirefree(L.pal) \inetwirefree(L.pax)
+				\node[below] at (L.above pal) {$\mathit{out}$};
+				\node[above] at (L.above pax) {$\mathit{x}$};
+			\end{tikzpicture} &
+			% Concrete
+			\begin{tikzpicture}
+				\agentConcrete{C}{k}
+				\inetwirefree(C.pal)
+				\node[below] at (C.above pal) {$\mathit{out}$};
+			\end{tikzpicture} &
+			% Add
+			\begin{tikzpicture}
+				\agentAdd{A}
+				\inetwirefree(A.pal) \inetwirefree(A.pax 1) \inetwirefree(A.pax 2)
+				\node[below] at (A.above pal) {$\mathit{a}$};
+				\node[above] at (A.above pax 1) {$\mathit{out}$};
+				\node[above] at (A.above pax 2) {$\mathit{b}$};
+			\end{tikzpicture} &
+			% Mul
+			\begin{tikzpicture}
+				\agentMul{M}
+				\inetwirefree(M.pal) \inetwirefree(M.pax 1) \inetwirefree(M.pax 2)
+				\node[below] at (M.above pal) {$\mathit{a}$};
+				\node[above] at (M.above pax 1) {$\mathit{out}$};
+				\node[above] at (M.above pax 2) {$\mathit{b}$};
+			\end{tikzpicture} \\
+			(a) $\mathit{Linear}$ & (b) $\mathit{Concrete}$ & (c) $\mathit{Add}$ & (d) $\mathit{Mul}$ \\[0.5cm]
+
+			% ReLU
+			\begin{tikzpicture}
+				\agentReLU{R}
+				\inetwirefree(R.pal) \inetwirefree(R.pax)
+				\node[below] at (R.above pal) {$\mathit{x}$};
+				\node[above] at (R.above pax) {$\mathit{out}$};
+			\end{tikzpicture} &
+			% Materialize
+			\begin{tikzpicture}
+				\agentMaterialize{MAT}
+				\inetwirefree(MAT.pal) \inetwirefree(MAT.pax)
+				\node[below] at (MAT.above pal) {$\mathit{x}$};
+				\node[above] at (MAT.above pax) {$\mathit{out}$};
+			\end{tikzpicture} &
+			% Eraser
+			\begin{tikzpicture}
+				\agentEraser{E}
+				\inetwirefree(E.pal)
+				\node[below] at (E.above pal) {$\mathit{x}$};
+			\end{tikzpicture} &
+			% Duplicator
+			\begin{tikzpicture}
+				\agentDuplicator{D}
+				\inetwirefree(D.pal) \inetwirefree(D.pax 1) \inetwirefree(D.pax 2)
+				\node[below] at (D.above pal) {$\mathit{x}$};
+				\node[above] at (D.above pax 1) {$\mathit{d_{1}}$};
+				\node[above] at (D.above pax 2) {$\mathit{d_{2}}$};
+			\end{tikzpicture} \\
+			(e) $\mathit{ReLU}$ & (f) $\mathit{Materialize}$ & (g) $\mathit{Eraser}$ & (h) $\mathit{Duplicator}$ \\[0.5cm]
+
+			% AddCheckLinear
+			\begin{tikzpicture}
+				\agentAddCheckLinear{AL}{q}{r}
+				\inetwirefree(AL.pal) \inetwirefree(AL.pax 1) \inetwirefree(AL.pax 2)
+				\node[below] at (AL.above pal) {$\mathit{b}$};
+				\node[above] at (AL.above pax 1) {$\mathit{out}$};
+				\node[above] at (AL.above pax 2) {$\mathit{x}$};
+			\end{tikzpicture} &
+			% MulCheckLinear
+			\begin{tikzpicture}
+				\agentMulCheckLinear{ML}{q}{r}
+				\inetwirefree(ML.pal) \inetwirefree(ML.pax 1) \inetwirefree(ML.pax 2)
+				\node[below] at (ML.above pal) {$\mathit{b}$};
+				\node[above] at (ML.above pax 1) {$\mathit{out}$};
+				\node[above] at (ML.above pax 2) {$\mathit{x}$};
+			\end{tikzpicture} &
+			% AddCheckConcrete
+			\begin{tikzpicture}
+				\agentAddCheckConcrete{AC}{k}
+				\inetwirefree(AC.pal) \inetwirefree(AC.pax)
+				\node[below] at (AC.above pal) {$\mathit{b}$};
+				\node[above] at (AC.above pax) {$\mathit{out}$};
+			\end{tikzpicture} &
+			% MulCheckConcrete
+			\begin{tikzpicture}
+				\agentMulCheckConcrete{MC}{k}
+				\inetwirefree(MC.pal) \inetwirefree(MC.pax)
+				\node[below] at (MC.above pal) {$\mathit{b}$};
+				\node[above] at (MC.above pax) {$\mathit{out}$};
+			\end{tikzpicture} \\
+			(i) $\mathit{AddCheckLinear}$ & (j) $\mathit{MulCheckLinear}$ & (k) $\mathit{AddCheckConcrete}$ & (l) $\mathit{MulCheckConcrete}$ \\[0.5cm]
+
+			% TermAdd
+			\begin{tikzpicture}
+				\agentTermAdd{TA}
+				\inetwirefree(TA.pal) \inetwirefree(TA.pax 1) \inetwirefree(TA.pax 2)
+				\node[below] at (TA.above pal) {$\mathit{out}$};
+				\node[above] at (TA.above pax 1) {$\mathit{a}$};
+				\node[above] at (TA.above pax 2) {$\mathit{b}$};
+			\end{tikzpicture} &
+			% TermMul
+			\begin{tikzpicture}
+				\agentTermMul{TM}
+				\inetwirefree(TM.pal) \inetwirefree(TM.pax 1) \inetwirefree(TM.pax 2)
+				\node[below] at (TM.above pal) {$\mathit{out}$};
+				\node[above] at (TM.above pax 1) {$\mathit{a}$};
+				\node[above] at (TM.above pax 2) {$\mathit{b}$};
+			\end{tikzpicture} &
+			% TermReLU
+			\begin{tikzpicture}
+				\agentTermReLU{TR}
+				\inetwirefree(TR.pal) \inetwirefree(TR.pax)
+				\node[below] at (TR.above pal) {$\mathit{out}$};
+				\node[above] at (TR.above pax) {$\mathit{x}$};
+			\end{tikzpicture} &
+			% Symbolic
+			\begin{tikzpicture}
+				\agentSymbolic{S}{id}
+				\inetwirefree(S.pal)
+				\node[below] at (S.above pal) {$\mathit{out}$};
+			\end{tikzpicture} \\
+			(m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{Symbolic}$ \\[0.5cm]
+		\end{tabular}
+	}
+	\caption{Agents used in VEIN.}
+	\label{fig:agents}
+\end{figure}
+
+The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents as illustrated in
+\textbf{\Cref{fig:rule-linear-add}} and \textbf{\Cref{fig:rule-linear-mul}}. Because interactions are local, the binary
+operators need to check one operator at the time. For this reason \textit{Add} and \textit{Mul} gets replaced by
+\textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$ and their
+principal port is faced toward the other operand.
+
+% Linear >< Add
+\begin{figure}[ht]
+	\centering
+	\interactionrule{
+		\agentLinear{L}{q}{r}[90]
+		\agentAdd[right=of L.pal]{A}[-90]
+		\inetwire(L.pal)(A.pal)
+		\inetwirefree(L.pax) \inetwirefree(A.pax 1) \inetwirefree(A.pax 2)
+		\node[left] at (L.above pax) {$\mathit{x}$};
+		\node[right] at (A.above pax 1) {$\mathit{out}$};
+		\node[right] at (A.above pax 2) {$\mathit{b}$};
+	}{
+		\agentAddCheckLinear{AL}{q}{r}[90]
+		\inetwirefree(AL.pal) \inetwirefree(AL.pax 1) \inetwirefree(AL.pax 2)
+		\node[right] at (AL.above pal) {$\mathit{b}$};
+		\node[left] at (AL.above pax 1) {$\mathit{out}$};
+		\node[left] at (AL.above pax 2) {$\mathit{x}$};
+	}
+	\caption{Interaction rule for $\mathit{Linear}$ and $\mathit{Add}$.}
+	\label{fig:rule-linear-add}
+\end{figure}
+
+% Linear >< Mul
+\begin{figure}[ht]
+	\centering
+	\interactionrule{
+		\agentLinear{L}{q}{r}[90]
+		\agentMul[right=of L.pal]{M}[-90]
+		\inetwire(L.pal)(M.pal)
+		\inetwirefree(L.pax) \inetwirefree(M.pax 1) \inetwirefree(M.pax 2)
+		\node[left] at (L.above pax) {$\mathit{x}$};
+		\node[right] at (M.above pax 1) {$\mathit{out}$};
+		\node[right] at (M.above pax 2) {$\mathit{b}$};
+	}{
+		\agentMulCheckLinear{ML}{q}{r}[90]
+		\inetwirefree(ML.pal) \inetwirefree(ML.pax 1) \inetwirefree(ML.pax 2)
+		\node[right] at (ML.above pal) {$\mathit{b}$};
+		\node[left] at (ML.above pax 1) {$\mathit{out}$};
+		\node[left] at (ML.above pax 2) {$\mathit{x}$};
+	}
+	\caption{Interaction rule for $\mathit{Linear}$ and $\mathit{Mul}$.}
+	\label{fig:rule-linear-mul}
+\end{figure}
+
+The same logic is applied to the \textit{Concrete} carrier agent, but here analyzing the attribute $k$
+enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}} we can see that when summing a \textit{Concrete}
+with $k=0$ we do not need to check the other operand and we simply wire it to the output.
+This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1$, as shown in
+\textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$ the other operand is deleted
+before the SMT solver is even invoked.
+
+% Concrete >< Add
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule{
+				\agentConcrete{C}{k}[90]
+				\agentAdd[right=of C.pal]{A}[-90]
+				\inetwire(C.pal)(A.pal)
+				\inetwirefree(A.pax 1) \inetwirefree(A.pax 2)
+				\node[right] at (A.above pax 1) {$\mathit{out}$};
+				\node[right] at (A.above pax 2) {$\mathit{b}$};
+			}
+			{
+				\agentAddCheckConcrete{AC}{k}[90]
+				\inetwirefree(AC.pal) \inetwirefree(AC.pax)
+				\node[right] at (AC.above pal) {$\mathit{b}$};
+				\node[left] at (AC.above pax) {$\mathit{out}$};
+			} \\
+			% k == 0
+			\interactionrule[$k=0$]{
+				\agentConcrete{C}{0}[90]
+				\agentAdd[right=of C.pal]{A}[-90]
+				\inetwire(C.pal)(A.pal)
+				\inetwirefree(A.pax 1) \inetwirefree(A.pax 2)
+				\node[right] at (A.above pax 1) {$\mathit{out}$};
+				\node[right] at (A.above pax 2) {$\mathit{b}$};
+			}{
+				\node(out) at (-1,0) {$\mathit{out}$};
+				\node(b) at (1, 0) {$\mathit{b}$};
+				\draw[\inetwirestyle] (b) -- (out);
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Concrete}$ and $\mathit{Add}$.}
+	\label{fig:rule-concrete-add}
+\end{figure}
+
+% Concrete >< Mul
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule{
+				\agentConcrete{C}{k}[90]
+				\agentMul[right=of C.pal]{M}[-90]
+				\inetwire(C.pal)(M.pal)
+				\inetwirefree(M.pax 1) \inetwirefree(M.pax 2)
+				\node[right] at (M.above pax 1) {$\mathit{out}$};
+				\node[right] at (M.above pax 2) {$\mathit{b}$};
+			}
+			{
+				\agentMulCheckConcrete{MC}{k}[90]
+				\inetwirefree(MC.pal) \inetwirefree(MC.pax)
+				\node[right] at (MC.above pal) {$\mathit{b}$};
+				\node[left] at (MC.above pax) {$\mathit{out}$};
+			} \\
+			% k == 0
+			\interactionrule[$k=0$]{
+				\agentConcrete{C}{0}[90]
+				\agentMul[right=of C.pal]{M}[-90]
+				\inetwire(C.pal)(M.pal)
+				\inetwirefree(M.pax 1) \inetwirefree(M.pax 2)
+				\node[right] at (M.above pax 1) {$\mathit{out}$};
+				\node[right] at (M.above pax 2) {$\mathit{b}$};
+			}{
+				\agentConcrete{C}{0}[90]
+				\agentEraser[below=of C]{E}[90]
+				\inetwirefree(C.pal) \inetwirefree(E.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+				\node[right] at (E.above pal) {$\mathit{b}$};
+			} \\
+			% k == 1
+			\interactionrule[$k=1$]{
+				\agentConcrete{C}{1}[90]
+				\agentMul[right=of C.pal]{M}[-90]
+				\inetwire(C.pal)(M.pal)
+				\inetwirefree(M.pax 1) \inetwirefree(M.pax 2)
+				\node[right] at (M.above pax 1) {$\mathit{out}$};
+				\node[right] at (M.above pax 2) {$\mathit{b}$};
+			}{
+				\node(out) at (-1,0) {$\mathit{out}$};
+				\node(b) at (1, 0) {$\mathit{b}$};
+				\draw[\inetwirestyle] (b) -- (out);
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Concrete}$ and $\mathit{Mul}$.}
+	\label{fig:rule-concrete-mul}
+\end{figure}
+
+If both operands are \textit{Linear} agents they need to be materialized before being wrapped in another
+\textit{Linear} to allow further simplification. This is done because multiplying two linear packets
+gives a non-linear result.
+While adding two linear packets gives a linear result, it depends on two free variables and the \textit{Linear} agent
+only supports one. A solution to this could be storing a dictionay of variables instead of a single one.
+This is illustrated in \textbf{\Cref{fig:rule-linear-addchecklinear}}
+and \textbf{\Cref{fig:rule-linear-mulchecklinear}} where the result of the materialization is passed
+to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Linear} with attributes
+$q=1,r=0$.
+
+% Linear >< AddCheckLinear
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule{
+				\agentLinear{L}{s}{t}[90]
+				\agentAddCheckLinear[right=of L.pal]{AL}{q}{r}[-90]
+				\inetwire(L.pal)(AL.pal)
+				\inetwirefree(L.pax) \inetwirefree(AL.pax 1) \inetwirefree(AL.pax 2)
+				\node[left] at (L.above pax) {$\mathit{y}$};
+				\node[right] at (AL.above pax 1) {$\mathit{out}$};
+				\node[right] at (AL.above pax 2) {$\mathit{x}$};
+			}{
+				\agentLinear{L1}{q}{r}[90]
+				\agentLinear[below=1.5cm of L1]{L2}{s}{t}[90]
+				\agentMaterialize[right=of L1.pal]{MAT1}[-90]
+				\agentMaterialize[right=of L2.pal]{MAT2}[-90]
+				\agentTermAdd[at=($(MAT1.pax)!0.5!(MAT2.pax)$), xshift=1cm]{TA}[90]
+				\agentLinear[right=of TA]{L3}{1}{0}[90]
+				\inetwire(L1.pal)(MAT1.pal) \inetwire(L2.pal)(MAT2.pal) \inetwire(MAT1.pax)(TA.pax 1) \inetwire(MAT2.pax)(TA.pax 2) \inetwire(TA.pal)(L3.pax)
+				\inetwirefree(L1.pax) \inetwirefree(L2.pax) \inetwirefree(L3.pal)
+				\node[left] at (L1.above pax) {$\mathit{x}$};
+				\node[left] at (L2.above pax) {$\mathit{y}$};
+				\node[right] at (L3.above pal) {$\mathit{out}$};
+			} \\
+			% (s == 0) && (t == 0)
+			\interactionrule[$(s=0)\land(t=0)$]{
+				\agentLinear{L}{0}{0}[90]
+				\agentAddCheckLinear[right=of L.pal]{AL}{q}{r}[-90]
+				\inetwire(L.pal)(AL.pal)
+				\inetwirefree(L.pax) \inetwirefree(AL.pax 1) \inetwirefree(AL.pax 2)
+				\node[left] at (L.above pax) {$\mathit{y}$};
+				\node[right] at (AL.above pax 1) {$\mathit{out}$};
+				\node[right] at (AL.above pax 2) {$\mathit{x}$};
+			}{
+				\agentLinear{L}{q}{r}[90]
+				\agentEraser[below=of L]{E}[90]
+				\inetwirefree(L.pal) \inetwirefree(L.pax) \inetwirefree(E.pal)
+				\node[left] at (L.above pax) {$\mathit{x}$};
+				\node[right] at (L.above pal) {$\mathit{out}$};
+				\node[right] at (E.above pal) {$\mathit{y}$};
+			} \\
+			% (q == 0) && (r == 0)
+			\interactionrule[$(q=0)\land(r=0)$]{
+				\agentLinear{L}{s}{t}[90]
+				\agentAddCheckLinear[right=of L.pal]{AL}{0}{0}[-90]
+				\inetwire(L.pal)(AL.pal)
+				\inetwirefree(L.pax) \inetwirefree(AL.pax 1) \inetwirefree(AL.pax 2)
+				\node[left] at (L.above pax) {$\mathit{y}$};
+				\node[right] at (AL.above pax 1) {$\mathit{out}$};
+				\node[right] at (AL.above pax 2) {$\mathit{x}$};
+			}{
+				\agentLinear{L}{s}{t}[90]
+				\agentEraser[below=of L]{E}[90]
+				\inetwirefree(L.pal) \inetwirefree(L.pax) \inetwirefree(E.pal)
+				\node[left] at (L.above pax) {$\mathit{y}$};
+				\node[right] at (L.above pal) {$\mathit{out}$};
+				\node[right] at (E.above pal) {$\mathit{x}$};
+			} \\
+			% (q == 0) && (r == 0) && (s == 0) && (t == 0)
+			\interactionrule[$(q=0)\land(r=0)\land(s=0)\land(t=0)$]{
+				\agentLinear{L}{0}{0}[90]
+				\agentAddCheckLinear[right=of L.pal]{AL}{0}{0}[-90]
+				\inetwire(L.pal)(AL.pal)
+				\inetwirefree(L.pax) \inetwirefree(AL.pax 1) \inetwirefree(AL.pax 2)
+				\node[left] at (L.above pax) {$\mathit{y}$};
+				\node[right] at (AL.above pax 1) {$\mathit{out}$};
+				\node[right] at (AL.above pax 2) {$\mathit{x}$};
+			}{
+				\agentConcrete{C}{0}[90]
+				\agentEraser[below=of C]{E1}[90]
+				\agentEraser[below=of E1]{E2}[90]
+				\inetwirefree(E1.pal) \inetwirefree(E2.pal) \inetwirefree(C.pal)
+				\node[right] at (E1.above pal) {$\mathit{x}$};
+				\node[right] at (E2.above pal) {$\mathit{y}$};
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Linear}$ and $\mathit{AddCheckLinear}$.}
+	\label{fig:rule-linear-addchecklinear}
+\end{figure}
+
+% Linear >< MulCheckLinear
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule{
+				\agentLinear{L}{s}{t}[90]
+				\agentMulCheckLinear[right=of L.pal]{ML}{q}{r}[-90]
+				\inetwire(L.pal)(ML.pal)
+				\inetwirefree(L.pax) \inetwirefree(ML.pax 1) \inetwirefree(ML.pax 2)
+				\node[left] at (L.above pax) {$\mathit{y}$};
+				\node[right] at (ML.above pax 1) {$\mathit{out}$};
+				\node[right] at (ML.above pax 2) {$\mathit{x}$};
+			}{
+				\agentLinear{L1}{q}{r}[90]
+				\agentLinear[below=1.5cm of L1]{L2}{s}{t}[90]
+				\agentMaterialize[right=of L1.pal]{MAT1}[-90]
+				\agentMaterialize[right=of L2.pal]{MAT2}[-90]
+				\agentTermMul[at=($(MAT1.pax)!0.5!(MAT2.pax)$), xshift=1cm]{TM}[90]
+				\agentLinear[right=of TM]{L3}{1}{0}[90]
+				\inetwire(L1.pal)(MAT1.pal) \inetwire(L2.pal)(MAT2.pal) \inetwire(MAT1.pax)(TM.pax 1) \inetwire(MAT2.pax)(TM.pax 2) \inetwire(TM.pal)(L3.pax)
+				\inetwirefree(L1.pax) \inetwirefree(L2.pax) \inetwirefree(L3.pal)
+				\node[left] at (L1.above pax) {$\mathit{x}$};
+				\node[left] at (L2.above pax) {$\mathit{y}$};
+				\node[right] at (L3.above pal) {$\mathit{out}$};
+			} \\
+			% ((q == 0) && (r == 0)) || ((s == 0) && (t == 0))
+			\interactionrule[$((q=0)\land(r=0))\lor((s=0)\land(t=0))$]{
+				\agentLinear{L}{s}{t}[90]
+				\agentMulCheckLinear[right=of L.pal]{ML}{q}{r}[-90]
+				\inetwire(L.pal)(ML.pal)
+				\inetwirefree(L.pax) \inetwirefree(ML.pax 1) \inetwirefree(ML.pax 2)
+				\node[left] at (L.above pax) {$\mathit{y}$};
+				\node[right] at (ML.above pax 1) {$\mathit{out}$};
+				\node[right] at (ML.above pax 2) {$\mathit{x}$};
+			}{
+				\agentConcrete{C}{0}[90]
+				\agentEraser[below=of C]{E1}[90]
+				\agentEraser[below=of E1]{E2}[90]
+				\inetwirefree(E1.pal) \inetwirefree(E2.pal) \inetwirefree(C.pal)
+				\node[right] at (E1.above pal) {$\mathit{x}$};
+				\node[right] at (E2.above pal) {$\mathit{y}$};
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Linear}$ and $\mathit{MulCheckLinear}$.}
+	\label{fig:rule-linear-mulchecklinear}
+\end{figure}
+
+Instead if the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent different rules are applied.
+In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) we add the attribute of the \textit{Concrete}
+agent to the attribute that represents the constant of the \textit{Linear} agent.
+For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) we multiply the attribute of
+the \textit{Concrete} agent to both the attributes of the \textit{Linear}
+
+% Concrete >< AddCheckLinear
+\begin{figure}[ht]
+	\centering
+	\interactionrule{
+		\agentConcrete{C}{j}[90]
+		\agentAddCheckLinear[right=of C.pal]{AL}{q}{r}[-90]
+		\inetwire(C.pal)(AL.pal)
+		\inetwirefree(AL.pax 1) \inetwirefree(AL.pax 2)
+		\node[right] at (AL.above pax 1) {$\mathit{out}$};
+		\node[right] at (AL.above pax 2) {$\mathit{x}$};
+	}{
+		\agentLinear{L}{q}{r + j}[90]
+		\inetwirefree(L.pal) \inetwirefree(L.pax)
+		\node[right] at (L.above pal) {$\mathit{out}$};
+		\node[left] at (L.above pax) {$\mathit{x}$};
+	}
+	\caption{Interaction rule for $\mathit{Concrete}$ and $\mathit{AddCheckLinear}$.}
+	\label{fig:rule-concrete-addchecklinear}
+\end{figure}
+
+% Concrete >< MulCheckLinear
+\begin{figure}[ht]
+	\centering
+	\interactionrule{
+		\agentConcrete{C}{j}[90]
+		\agentMulCheckLinear[right=of C.pal]{ML}{q}{r}[-90]
+		\inetwire(C.pal)(ML.pal)
+		\inetwirefree(ML.pax 1) \inetwirefree(ML.pax 2)
+		\node[right] at (ML.above pax 1) {$\mathit{out}$};
+		\node[right] at (ML.above pax 2) {$\mathit{x}$};
+	}{
+		\agentLinear{L}{q * j}{r * j}[90]
+		\inetwirefree(L.pal) \inetwirefree(L.pax)
+		\node[right] at (L.above pal) {$\mathit{out}$};
+		\node[left] at (L.above pax) {$\mathit{x}$};
+	}
+	\caption{Interaction rule for $\mathit{Concrete}$ and $\mathit{MulCheckLinear}$.}
+	\label{fig:rule-concrete-mulchecklinear}
+\end{figure}
+
+In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}}
+we follow the exact same logic except the first operand is a \textit{Concrete} and the second is a \textit{Linear}.
+
+% Linear >< AddCheckConcrete
+\begin{figure}[ht]
+	\centering
+	\interactionrule{
+		\agentLinear{L}{s}{t}[90]
+		\agentAddCheckConcrete[right=of L.pal]{AC}{k}[-90]
+		\inetwire(L.pal)(AC.pal)
+		\inetwirefree(L.pax) \inetwirefree(AC.pax)
+		\node[left] at (L.above pax) {$\mathit{y}$};
+		\node[right] at (AC.above pax) {$\mathit{out}$};
+	}{
+		\agentLinear{L}{s}{t + k}[90]
+		\inetwirefree(L.pal) \inetwirefree(L.pax)
+		\node[right] at (L.above pal) {$\mathit{out}$};
+		\node[left] at (L.above pax) {$\mathit{y}$};
+	}
+	\caption{Interaction rule for $\mathit{Linear}$ and $\mathit{AddCheckConcrete}$.}
+	\label{fig:rule-linear-addcheckconcrete}
+\end{figure}
+
+% Linear >< MulCheckConcrete
+\begin{figure}[ht]
+	\centering
+	\interactionrule{
+		\agentLinear{L}{s}{t}[90]
+		\agentMulCheckConcrete[right=of L.pal]{MC}{k}[-90]
+		\inetwire(L.pal)(MC.pal)
+		\inetwirefree(L.pax) \inetwirefree(MC.pax)
+		\node[left] at (L.above pax) {$\mathit{y}$};
+		\node[right] at (MC.above pax) {$\mathit{out}$};
+	}{
+		\agentLinear{L}{s * k}{t * k}[90]
+		\inetwirefree(L.pal) \inetwirefree(L.pax)
+		\node[right] at (L.above pal) {$\mathit{out}$};
+		\node[left] at (L.above pax) {$\mathit{y}$};
+	}
+	\caption{Interaction rule for $\mathit{Linear}$ and $\mathit{MulCheckConcrete}$.}
+	\label{fig:rule-linear-mulcheckconcrete}
+\end{figure}
+
+Finally if both operands are \textit{Concrete} agents they are either merged into a single \textit{Concrete}
+or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckconcrete}} and
+\textbf{\Cref{fig:rule-concrete-mulcheckconcrete}} following a similar logic to the previous rules.
+
+% Concrete >< AddCheckConcrete
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule{
+				\agentConcrete{C}{j}[90]
+				\agentAddCheckConcrete[right=of C.pal]{AC}{k}[-90]
+				\inetwire(C.pal)(AC.pal)
+				\inetwirefree(AC.pax)
+				\node[right] at (AC.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{k + j}[90]
+				\inetwirefree(C.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+			% j == 0
+			\interactionrule[$j=0$]{
+				\agentConcrete{C}{0}[90]
+				\agentAddCheckConcrete[right=of C.pal]{AC}{k}[-90]
+				\inetwire(C.pal)(AC.pal)
+				\inetwirefree(AC.pax)
+				\node[right] at (AC.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{k}[90]
+				\inetwirefree(C.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Concrete}$ and $\mathit{AddCheckConcrete}$.}
+	\label{fig:rule-concrete-addcheckconcrete}
+\end{figure}
+
+% Concrete >< MulCheckConcrete
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule{
+				\agentConcrete{C}{j}[90]
+				\agentMulCheckConcrete[right=of C.pal]{MC}{k}[-90]
+				\inetwire(C.pal)(MC.pal)
+				\inetwirefree(MC.pax)
+				\node[right] at (MC.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{k * j}[90]
+				\inetwirefree(C.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+			% j == 0
+			\interactionrule[$j = 0$]{
+				\agentConcrete{C}{0}[90]
+				\agentMulCheckConcrete[right=of C.pal]{MC}{k}[-90]
+				\inetwire(C.pal)(MC.pal)
+				\inetwirefree(MC.pax)
+				\node[right] at (MC.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{0}[90]
+				\inetwirefree(C.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+			% j == 1
+			\interactionrule[$j = 1$]{
+				\agentConcrete{C}{1}[90]
+				\agentMulCheckConcrete[right=of C.pal]{MC}{k}[-90]
+				\inetwire(C.pal)(MC.pal)
+				\inetwirefree(MC.pax)
+				\node[right] at (MC.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{k}[90]
+				\inetwirefree(C.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Concrete}$ and $\mathit{MulCheckConcrete}$.}
+	\label{fig:rule-concrete-mulcheckconcrete}
+\end{figure}
+
+When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is no
+enough informations to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}},
+the agent is just materialized, passed to a \textit{TermReLU} and then wrapped in a \textit{Linear}.
+In \textbf{\Cref{fig:rule-concrete-relu}} is illustrated that when the \textit{Concrete} carrier agent
+meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either with attribute $k$
+if $k>0$ or with attribute equal $0$ otherwise.
+
+% Linear >< ReLU
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\interactionrule{
+			\agentLinear{L}{q}{r}[90]
+			\agentReLU[right=of L.pal]{R}[-90]
+			\inetwire(L.pal)(R.pal)
+			\inetwirefree(L.pax) \inetwirefree(R.pax)
+			\node[left] at (L.above pax) {$\mathit{x}$};
+			\node[right] at (R.above pax) {$\mathit{out}$};
+		}{
+			\agentLinear{L1}{q}{r}[90]
+			\agentMaterialize[right=of L1.pal]{MAT}[-90]
+			\agentTermReLU[right=of MAT]{TR}[90]
+			\agentLinear[right=of TR]{L2}{1}{0}[90]
+			\inetwire(L1.pal)(MAT.pal) \inetwire(MAT.pax)(TR.pax) \inetwire(TR.pal)(L2.pax)
+			\inetwirefree(L1.pax) \inetwirefree(L2.pal)
+			\node[left] at (L1.above pax) {$\mathit{x}$};
+			\node[right] at (L2.above pal) {$\mathit{out}$};
+		}
+	}
+	\caption{Interaction rule for $\mathit{Linear}$ and $\mathit{ReLU}$.}
+	\label{fig:rule-linear-relu}
+\end{figure}
+
+% Concrete >< ReLU
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule[$k <= 0$]{
+				\agentConcrete{C}{k}[90]
+				\agentReLU[right=of C.pal]{R}[-90]
+				\inetwire(C.pal)(R.pal)
+				\inetwirefree(R.pax)
+				\node[right] at (R.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{0}[90]
+				\inetwirefree(C.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+			% k > 0
+			\interactionrule[$k > 0$]{
+				\agentConcrete{C}{k}[90]
+				\agentReLU[right=of C.pal]{R}[-90]
+				\inetwire(C.pal)(R.pal)
+				\inetwirefree(R.pax)
+				\node[right] at (R.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{k}[90]
+				\inetwirefree(C.pal)
+				\node[right] at (C.above pal) {$\mathit{out}$};
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Concrete}$ and $\mathit{ReLU}$.}
+	\label{fig:rule-concrete-relu}
+\end{figure}
+
+When a \textit{Linear} is materialized it will explicitly build an AST using \textit{TermAdd} and \textit{TermMul}
+to recreate $q*x+r$ as shown in \textbf{\Cref{fig:rule-linear-materialize}}.
+When a \textit{Concrete} needs to be materialized nothing needs to be done and it is directly wired to output
+\textbf{\Cref{fig:rule-concrete-materialize}}.
+
+% Linear >< Materialize
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\begin{tabular}{c}
+			% otherwise
+			\interactionrule{
+				\agentLinear{L}{q}{r}[90]
+				\agentMaterialize[right=of L.pal]{MAT}[-90]
+				\inetwire(L.pal)(MAT.pal)
+				\inetwirefree(L.pax) \inetwirefree(MAT.pax)
+				\node [left] at (L.above pax) {$\mathit{x}$};
+				\node [right] at (MAT.above pax) {$\mathit{out}$};
+			}{
+				\agentTermAdd{TA}[90]
+				\agentTermMul[left=of TA.pax 1]{TM}[90]
+				\agentConcrete[left=of TA.pax 2, below=of TM]{C1}{r}[90]
+				\agentConcrete[left=of TM.pax 1]{C2}{q}[90]
+				\inetwire(TA.pax 1)(TM.pal) \inetwire(TA.pax 2)(C1.pal) \inetwire(TM.pax 1)(C2.pal)
+				\inetwirefree(TA.pal) \inetwirefree(TM.pax 2)
+				\node [left] at (TM.above pax 2) {$\mathit{x}$};
+				\node [right] at (TA.above pal) {$\mathit{out}$};
+			} \\
+			% q == 0
+			\interactionrule[$q=0$]{
+				\agentLinear{L}{0}{r}[90]
+				\agentMaterialize[right=of L.pal]{MAT}[-90]
+				\inetwire(L.pal)(MAT.pal)
+				\inetwirefree(L.pax) \inetwirefree(MAT.pax)
+				\node [left] at (L.above pax) {$\mathit{x}$};
+				\node [right] at (MAT.above pax) {$\mathit{out}$};
+			}{
+				\agentConcrete{C}{r}[90]
+				\agentEraser[below=of C]{E}[90]
+				\inetwirefree(C.pal) \inetwirefree(E.pal)
+				\node [right] at (C.above pal) {$\mathit{out}$};
+				\node [right] at (E.above pal) {$\mathit{x}$};
+			} \\
+			% (q == 1) && (r == 0)
+			\interactionrule[$(q=1)\land(r=0)$]{
+				\agentLinear{L}{1}{0}[90]
+				\agentMaterialize[right=of L.pal]{MAT}[-90]
+				\inetwire(L.pal)(MAT.pal)
+				\inetwirefree(L.pax) \inetwirefree(MAT.pax)
+				\node [left] at (L.above pax) {$\mathit{x}$};
+				\node [right] at (MAT.above pax) {$\mathit{out}$};
+			}{
+				\node(out) at (-1,0) {$\mathit{out}$};
+				\node(x) at (1, 0) {$\mathit{x}$};
+				\draw[\inetwirestyle] (x) -- (out);
+			} \\
+			% (q == 1) && (r != 0)
+			\interactionrule[$(q=1)\land(r\neq0)$]{
+				\agentLinear{L}{1}{r}[90]
+				\agentMaterialize[right=of L.pal]{MAT}[-90]
+				\inetwire(L.pal)(MAT.pal)
+				\inetwirefree(L.pax) \inetwirefree(MAT.pax)
+				\node [left] at (L.above pax) {$\mathit{x}$};
+				\node [right] at (MAT.above pax) {$\mathit{out}$};
+			}{
+				\agentTermAdd{TA}[90]
+				\agentConcrete[left=of TA.right pax]{C}{r}[90]
+				\inetwire(C.pal)(TA.pax 2)
+				\inetwirefree(TA.pax 1) \inetwirefree(TA.pal)
+				\node [left] at (TA.above pax 1) {$\mathit{x}$};
+				\node [right] at (TA.above pal) {$\mathit{out}$};
+			} \\
+			% (q != 0) && (r == 0)
+			\interactionrule[$(q\neq0)\land(r=0)$]{
+				\agentLinear{L}{q}{0}[90]
+				\agentMaterialize[right=of L.pal]{MAT}[-90]
+				\inetwire(L.pal)(MAT.pal)
+				\inetwirefree(L.pax) \inetwirefree(MAT.pax)
+				\node [left] at (L.above pax) {$\mathit{x}$};
+				\node [right] at (MAT.above pax) {$\mathit{out}$};
+			}{
+				\agentTermMul{TM}[90]
+				\agentConcrete[left=of TM.left pax]{C}{q}[90]
+				\inetwire(C.pal)(TM.pax 1)
+				\inetwirefree(TM.pax 2) \inetwirefree(TM.pal)
+				\node [left] at (TM.above pax 2) {$\mathit{x}$};
+				\node [right] at (TM.above pal) {$\mathit{out}$};
+			} \\
+		\end{tabular}
+	}
+	\caption{Interaction rules for $\mathit{Linear}$ and $\mathit{Materialize}$.}
+	\label{fig:rule-linear-materialize}
+\end{figure}
+
+% Concrete >< Materialize
+\begin{figure}[ht]
+	\centering
+	\resizebox{\textwidth}{!}{
+		\interactionrule{
+			\agentConcrete{C}{k}[90]
+			\agentMaterialize[right=of C.pal]{MAT}[-90]
+			\inetwire(C.pal)(MAT.pal)
+			\inetwirefree(MAT.pax)
+			\node [right] at (MAT.above pax) {$\mathit{out}$};
+		}{
+			\agentConcrete{C}{k}[90]
+			\inetwirefree(C.pal)
+			\node [right] at (C.above pal) {$\mathit{out}$};
+		}
+	}
+	\caption{Interaction rule for $\mathit{Concrete}$ and $\mathit{Materialize}$.}
+	\label{fig:rule-concrete-materialize}
+\end{figure}
diff --git a/macros.tex b/macros.tex
new file mode 100644
index 0000000..32b4789
--- /dev/null
+++ b/macros.tex
@@ -0,0 +1,85 @@
+% Linear
+\newcommand{\agentLinear}[4][]{% [#1=options, #2=name, #3=q, #4=r]
+	\inetcell[arity=1, #1](#2){$\mathit{L}_{#3,#4}$}
+}
+% Concrete
+\newcommand{\agentConcrete}[3][]{% [#1=options, #2=name, #3=k]
+	\inetcell[arity=0, #1](#2){$\mathit{C}_{#3}$}
+}
+% Add
+\newcommand{\agentAdd}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=2, #1](#2){$\mathit{A}$}
+}
+% Mul
+\newcommand{\agentMul}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=2, #1](#2){$\mathit{M}$}
+}
+% ReLU
+\newcommand{\agentReLU}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=1, #1](#2){$\mathit{R}$} 
+}
+% AddCheckLinear
+\newcommand{\agentAddCheckLinear}[4][]{% [#1=options, #2=name, #3=q, #4=r]
+	\inetcell[arity=2, #1](#2){$\mathit{AL}_{#3,#4}$}
+}
+% MulCheckLinear
+\newcommand{\agentMulCheckLinear}[4][]{% [#1=options, #2=name, #3=q, #4=r
+	\inetcell[arity=2, #1](#2){$\mathit{ML}_{#3,#4}$}
+}
+% AddCheckConcrete
+\newcommand{\agentAddCheckConcrete}[3][]{% [#1=options, #2=name, #3=k]
+	\inetcell[arity=1, #1](#2){$\mathit{AC}_{#3}$}
+}
+% MulCheckConcrete
+\newcommand{\agentMulCheckConcrete}[3][]{% [#1=options, #2=name, #3=k]
+	\inetcell[arity=1, #1](#2){$\mathit{MC}_{#3}$}
+}
+% Materialize
+\newcommand{\agentMaterialize}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=1, #1](#2){$\mathit{MAT}$}
+}
+% Eraser
+\newcommand{\agentEraser}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=0, #1](#2){$\epsilon$}
+}
+% Duplicator
+\newcommand{\agentDuplicator}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=2, #1](#2){$\delta$}
+}
+% TermAdd
+\newcommand{\agentTermAdd}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=2, #1](#2){$\mathit{TA}$}
+}
+% TermMul
+\newcommand{\agentTermMul}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=2, #1](#2){$\mathit{TM}$}
+}
+% TermReLU
+\newcommand{\agentTermReLU}[2][]{% [#1=options, #2=name]
+	\inetcell[arity=1, #1](#2){$\mathit{TR}$}
+}
+% Symbolic
+\newcommand{\agentSymbolic}[3][]{% [#1=options, #2=name, #3=symbol]
+	\inetcell[arity=0, #1](#2){$\mathit{S_{#3}}$}
+}
+% Interaction Rule
+\newcommand{\interactionrule}[3][]{
+	\begin{tikzpicture}
+		\node(arrow) at (0,0){
+			\begin{tikzpicture}
+				\node (arrow) at (0,0) {$\longrightarrow$};
+				\if\relax\detokenize{#1}\relax\else
+					\node[above=0.1cm of arrow, font=\scriptsize\itshape] {#1};
+				\fi
+			\end{tikzpicture}
+		};
+		% LHS
+		\node(LHS)[left=of arrow]{
+			\begin{tikzpicture} #2 \end{tikzpicture}
+		};
+		% RHS
+		\node(RHS)[right=of arrow]{
+			\begin{tikzpicture} #3 \end{tikzpicture}
+		};
+	\end{tikzpicture}
+}
diff --git a/main.tex b/main.tex
index dbc7999..bcb97c8 100644
--- a/main.tex
+++ b/main.tex
@@ -11,6 +11,10 @@
 \usepackage[colorinlistoftodos]{todonotes}
 % \usepackage[scaled=.83]{beramono} 
 \usepackage{lineno}
+\usepackage{tikz-inet}
+\usetikzlibrary{calc}
+
+\input{macros}
 
 \title{VEIN: VErification via Interaction Nets for Neural Networks}
 \author{Eric Marin}
diff --git a/tikz-inet.sty b/tikz-inet.sty
new file mode 100644
index 0000000..69a54dd
--- /dev/null
+++ b/tikz-inet.sty
@@ -0,0 +1,401 @@
+% Copyright 2008 by Marc de Falco
+%
+% This file may be distributed and/or modified
+%
+% 1. under the LaTeX Project Public License and/or
+% 2. under the GNU Public License.
+%
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{tikz-inet}[2008/06/02 v0.1 tikz interaction nets library]
+\RequirePackage{tikz}
+\RequirePackage{ifthen}
+
+% We need this to load the \emph{isosceles triangle} shape
+\usetikzlibrary{shapes.geometric}
+\usetikzlibrary{shadows}
+\usetikzlibrary{positioning}
+\usetikzlibrary{matrix}
+\usetikzlibrary{fit}
+
+\pgfkeys{/pgf/.cd,
+    arity/.initial=4,
+}
+
+% The definition of the shape of a cell
+\pgfdeclareshape{cellule}{
+    \savedmacro\arity{%        
+        \pgfmathtruncatemacro\arity{\pgfkeysvalueof{/pgf/arity}}%
+    }
+
+    \inheritsavedanchors[from=isosceles triangle]
+    \inheritanchorborder[from=isosceles triangle]
+    \inheritanchor[from=isosceles triangle]{center}
+    \inheritanchor[from=isosceles triangle]{left corner}
+    \inheritanchor[from=isosceles triangle]{right corner}
+    \inheritanchor[from=isosceles triangle]{south}
+    \inheritanchor[from=isosceles triangle]{west}
+    \inheritanchor[from=isosceles triangle]{north east}
+    \inheritanchor[from=isosceles triangle]{north west}
+    \inheritanchor[from=isosceles triangle]{south east}
+    \inheritanchor[from=isosceles triangle]{south west}
+    \inheritanchor[from=isosceles triangle]{east}
+    \inheritanchor[from=isosceles triangle]{north}
+    \inheritanchor[from=isosceles triangle]{lower left}
+    \inheritanchor[from=isosceles triangle]{apex}
+   
+    \anchor{above pax}{
+        \trianglepoints
+        \pgfmathrotatepointaround{
+            \pgfpointadd{
+                \pgfpointadd{\pgfpoint{-2ex}{0cm}}{
+                    \pgfpointlineattime{0.5}
+                        {\lowerleftanchor}{\lowerrightanchor}
+                    }
+                }
+                {\centerpoint}
+            }{\centerpoint}{\rotate}
+        }
+
+  
+    \anchor{above middle pax}{
+        \trianglepoints
+        \pgfmathrotatepointaround{
+            \pgfpointadd{
+                \pgfpointadd{\pgfpoint{-2ex}{0cm}}{
+                    \pgfpointlineattime{0.5}
+                        {\lowerleftanchor}{\lowerrightanchor}
+                    }
+                }
+                {\centerpoint}
+            }{\centerpoint}{\rotate}
+        }
+
+                    \anchor{pax}{
+                    \trianglepoints
+                    \pgfmathrotatepointaround{
+                    \pgfpointadd{\pgfpointlineattime{0.5}
+                    {\lowerleftanchor}{\lowerrightanchor}}{\centerpoint}}
+                    {\centerpoint}{\rotate}
+                    }
+
+
+                    \anchor{middle pax}{
+                    \trianglepoints
+                    \pgfmathrotatepointaround{
+                    \pgfpointadd{\pgfpointlineattime{0.5}
+                    {\lowerleftanchor}{\lowerrightanchor}}{\centerpoint}}
+                    {\centerpoint}{\rotate}
+                    }
+
+                    \anchor{above left pax}{
+                    \trianglepoints
+                    \pgfmathrotatepointaround{
+                    \pgfpointadd{
+                    \pgfpointadd{\pgfpoint{-2ex}{0cm}}{
+                    \pgfpointlineattime{0.25}
+                    {\lowerleftanchor}{\lowerrightanchor}
+                    }
+                    }
+                    {\centerpoint}
+                    }{\centerpoint}{\rotate}
+                    }
+
+
+                    \anchor{left pax}{
+                    \trianglepoints
+                    \pgfmathrotatepointaround{
+                    \pgfpointadd{\pgfpointlineattime{0.25}
+                    {\lowerleftanchor}{\lowerrightanchor}}{\centerpoint}}
+                    {\centerpoint}{\rotate}
+                    }
+
+    \anchor{above right pax}{
+    \trianglepoints
+    \pgfmathrotatepointaround{
+    \pgfpointadd{
+    \pgfpointadd{\pgfpoint{-2ex}{0cm}}{
+    \pgfpointlineattime{0.75}
+    {\lowerleftanchor}{\lowerrightanchor}
+    }
+    }
+    {\centerpoint}
+    }{\centerpoint}{\rotate}
+    }
+
+
+    \anchor{right pax}{
+    \trianglepoints
+    \pgfmathrotatepointaround{
+    \pgfpointadd{\pgfpointlineattime{0.75}
+    {\lowerleftanchor}{\lowerrightanchor}}{\centerpoint}}
+    {\centerpoint}{\rotate}
+    }
+
+    \anchor{above pal}{
+    \trianglepoints
+    \pgfpointadd{\centerpoint}{
+    \pgfmathrotatepointaround{
+    \pgfpointadd{\pgfpoint{2ex}{0cm}}{\apexanchor}}
+    {\pgfpointorigin}{\rotate}
+    }
+    }
+
+
+    \anchor{pal}{
+    \trianglepoints
+    \pgfpointadd{\centerpoint}{
+    \pgfmathrotatepointaround{
+    \pgfpointadd{\pgfpoint{-0.07cm}{0cm}}{\apexanchor}
+    }{\pgfpointorigin}{\rotate}
+    }
+    }
+
+
+    \backgroundpath{
+        \trianglepoints{
+            \pgftransformshift{\centerpoint}
+            \pgftransformrotate{\rotate}
+            \pgfpathmoveto{\apex}
+            \pgfpathlineto{
+                \pgfpointlineattime{0.8}{\apex}{\lowerleft}
+            }
+            \pgfpathcurveto{
+                \pgfpointlineattime{0.9}{\apex}{\lowerleft}
+            }{
+                \pgfpointlineattime{0.1}{\lowerleft}{\lowerleft\pgf@y-\pgf@y}
+            }{
+    \pgfpointlineattime{0.2}{\lowerleft}{\lowerleft\pgf@y-\pgf@y}
+    }
+    \pgfpathlineto{
+    \pgfpointlineattime{0.8}{\lowerleft}{\lowerleft\pgf@y-\pgf@y}
+    }
+    \pgfpathcurveto{
+    \pgfpointlineattime{0.9}{\lowerleft}{\lowerleft\pgf@y-\pgf@y}
+    }{
+    \pgfpointlineattime{0.1}{\lowerleft\pgf@y-\pgf@y}{\apex}
+    }{
+    \pgfpointlineattime{0.2}{\lowerleft\pgf@y-\pgf@y}{\apex}
+    }
+
+    \pgfpathclose
+    }
+    }
+    
+    \expandafter\pgfutil@g@addto@macro\csname pgf@sh@s@cellule\endcsname{%
+		\c@pgf@counta\arity\relax%
+		\pgfmathloop%
+			\ifnum\c@pgf@counta>0\relax%
+				\pgfutil@ifundefined{pgf@anchor@cellule@pax\space\the\c@pgf@counta}{%
+                % I HATE TeX
+				\expandafter\xdef\csname pgf@anchor@cellule@pax\space\the\c@pgf@counta\endcsname{% 
+                \noexpand\pgfmathadd@{\noexpand\arity}{-1}%
+                \noexpand\c@pgf@countb=\noexpand\pgfmathresult%
+                \noexpand\pgfmathadd@{\the\c@pgf@counta}{-1}%
+                \noexpand\pgfmathdivide@{\noexpand\pgfmathresult}%
+                    {\noexpand\the\c@pgf@countb}%
+                \noexpand\pgfmathmultiply@{\noexpand\pgfmathresult}{0.5}%
+                \noexpand\pgfmathadd@{\noexpand\pgfmathresult}{0.25}%
+                \noexpand\let\noexpand\time\noexpand\pgfmathresult%
+                \noexpand\trianglepoints%
+                  \noexpand\pgfmathrotatepointaround{%
+                  \noexpand\pgfpointadd{%
+                    \noexpand\pgfpointlineattime%
+                    {\noexpand\time}%
+                    {\noexpand\lowerleftanchor}%
+                    {\noexpand\lowerrightanchor}%
+                  }{\noexpand\centerpoint}%
+                  }{\noexpand\centerpoint}{\noexpand\rotate}%
+                }%
+                \expandafter\xdef\csname pgf@anchor@cellule@above pax\space\the\c@pgf@counta\endcsname{%
+                \noexpand\pgfmathadd@{\noexpand\arity}{-1}%
+                \noexpand\c@pgf@countb=\noexpand\pgfmathresult%
+                \noexpand\pgfmathadd@{\the\c@pgf@counta}{-1}%
+                \noexpand\pgfmathdivide@{\noexpand\pgfmathresult}%
+                    {\noexpand\the\c@pgf@countb}%
+                \noexpand\pgfmathmultiply@{\noexpand\pgfmathresult}{0.5}%
+                \noexpand\pgfmathadd@{\noexpand\pgfmathresult}{0.25}%
+                \noexpand\let\noexpand\time\noexpand\pgfmathresult%
+                \noexpand\trianglepoints
+                  \noexpand\pgfmathrotatepointaround{%
+                      \noexpand\pgfpointadd{%
+                            \noexpand\pgfpointadd{
+                                \noexpand\pgfpoint{-2ex}{0cm}}{%
+                                    \noexpand\pgfpointlineattime%
+                                        {\noexpand\time}%
+                                        {\noexpand\lowerleftanchor}%
+                                        {\noexpand\lowerrightanchor}%
+                                    }%
+                            }{\noexpand\centerpoint}%
+                    }%
+                    {\noexpand\centerpoint}%
+                    {\noexpand\rotate}%
+                }%
+			}{\c@pgf@counta0\relax}% 
+			\advance\c@pgf@counta-1\relax%
+		\repeatpgfmathloop%	
+	}%
+
+}
+
+\newcommand\inetoptions{\setkeys{inet}}
+\newcommand{\inetcolor}{red}
+\define@key{inet}{color}{\renewcommand{\inetcolor}{#1}}
+\newcommand{\inet@defaultangle}{0}
+\define@key{inet}{defaultangle}{\renewcommand{\inet@defaultangle}{#1}}
+
+\newcount\inet@angle
+\inet@angle=0
+
+\tikzset{wirestyle/.style = {draw, line width=0.15ex, line cap=rect}}
+\tikzset{cellstyle/.style = {
+    draw, line width=0.2ex, fill=white,
+    inner sep=0.2ex,
+    }}
+\tikzset{boxstyle/.style = {draw,line width=0.1ex}}
+\tikzfading[name=inet fading,
+    left color=transparent!0,
+    right color=transparent!100]
+\tikzset{fancywirestyle/.style = {draw, line width=0.15ex,
+    draw=black!50!#1,
+    double=white!50!#1,double distance=0.2ex,
+   }}
+\tikzset{fancycellstyle/.style={%
+    general shadow={fill, shadow scale=1.0,%
+    shadow xshift=0.3ex,shadow yshift=-0.3ex,opacity=0.2},
+    line width=0.15ex,%
+    inner sep=0.2ex,%
+    draw=black!50!#1,%
+    top color=#1,%
+    bottom color=white,%!80!#1,%
+    shading angle=\inet@angle,%
+    }}
+\tikzset{fancyboxstyle/.style = {line width=0.2ex,fill opacity=0.5,
+    fill=white!20!#1,draw=black!30!#1}}
+
+\newif\ifinet@fancy\inet@fancyfalse
+
+\DeclareOption{fancy}{\inet@fancytrue}
+\DeclareOption{nofancy}{\inet@fancyfalse}
+
+\newcommand{\inetfancy}{\inet@fancytrue}
+\newcommand{\inetnofancy}{\inet@fancyfalse}
+
+\newcommand{\inetsetfancycellstyle}[1]{
+    \tikzset{fancycellstyle/.style = {#1}}%
+}
+\newcommand{\inetsetfancywirestyle}[1]{
+    \tikzset{fancycellstyle/.style = {#1}}%
+}
+
+\DeclareOption*{\expandafter\inetoptions\expandafter{\CurrentOption}}
+\ProcessOptions\relax
+
+\pgfdeclarelayer{wire layer}
+\pgfdeclarelayer{box layer}
+\pgfsetlayers{box layer,wire layer,main}
+
+\makeatletter
+
+\newcommand{\inetcellstyle}{%
+    \ifinet@fancy fancycellstyle\else cellstyle\fi%
+}
+
+\newcommand{\inetwirestyle}{%
+    \ifinet@fancy fancywirestyle\else wirestyle\fi%
+}
+
+\newcommand{\inetboxstyle}{%
+    \ifinet@fancy fancyboxstyle\else boxstyle\fi%
+}
+
+
+\newcommand{\inetcell}[1][]{%
+    \@ifnextchar({%
+    \inetcell@ii[#1]%
+    }{%
+    \inetcell@iib[#1]%
+    }%
+}
+
+\def\inetcell@iib[#1]#2{%
+    \inetcell@ii[#1](#2){#2}%
+}
+
+\def\inetcell@ii[#1](#2)#3{%
+    \@ifnextchar[{\inetcell@iii[#1](#2){#3}%
+    }{\inetcell@iii[#1](#2){#3}[\inet@defaultangle]}%
+}
+
+\def\inetcell@iii[#1](#2)#3[#4]{%
+    \ifthenelse{\equal{#4}{U}}{\inet@angle=180}{%
+        \ifthenelse{\equal{#4}{D}}{\inet@angle=0}{%
+            \ifthenelse{\equal{#4}{L}}{\inet@angle=270}{%
+                \ifthenelse{\equal{#4}{R}}{\inet@angle=90}{\inet@angle=#4}%
+            }%
+        }%
+    }%
+    \node[%
+    \inetcellstyle=\inetcolor%
+    ,shape border rotate=\inet@angle-90%
+    ,cellule, isosceles triangle apex angle=60,%
+    shape border uses incircle, #1] (#2) {#3};%
+}
+
+\def\inetwirecoords(#1)(#2){%
+    \begin{pgfonlayer}{wire layer}%
+        \draw[\ifinet@fancy fancywirestyle\else wirestyle\fi=\inetcolor]%
+        (#1) -- (#2);%
+    \end{pgfonlayer}
+}
+
+\def\inetwire{%
+    \@ifnextchar[{\inetwire@i}{\inetwire@i[]}%
+}
+
+\def\inetwire@i[#1](#2.#3)(#4.#5){%
+    \begin{pgfonlayer}{wire layer}%
+        \draw[\inetwirestyle=\inetcolor,#1]%
+        (#2.#3) .. controls (#2.above #3) and (#4.above #5) .. (#4.#5);%
+    \end{pgfonlayer}%
+}
+
+\def\inetwirefree{%
+    \@ifnextchar[{\inetwirefree@i}{\inetwirefree@i[]}%
+}
+\def\inetwirefree@i[#1](#2.#3){%
+    \begin{pgfonlayer}{wire layer}%
+        \draw[\ifinet@fancy fancywirestyle\else wirestyle\fi=\inetcolor,#1]%
+        (#2.#3) -- (#2.above #3);%
+    \end{pgfonlayer}%
+}
+
+\newcommand{\inetloop}[1][]{%
+    \begin{pgfonlayer}{wire layer}%
+        \node[\ifinet@fancy fancywirestyle\else wirestyle\fi=\inetcolor,%
+        #1,circle,inner sep=6pt] {};
+    \end{pgfonlayer}%
+}
+
+\newcommand{\inetbox}[1][]{%
+    \inetbox@i[#1]%
+}
+
+\def\inetbox@i[#1]#2(#3){%
+    \begin{pgfonlayer}{box layer}%
+        \node[\ifinet@fancy fancyboxstyle\else boxstyle\fi=\inetcolor,
+        fit=#2,inner sep=10pt,#1] (#3) {};%
+    \end{pgfonlayer}%
+}
+
+\newcommand{\inetprombox}[1][]{%
+    \inetprombox@i[#1]%
+}
+\def\inetprombox@i[#1]#2(#3){%
+   \inetbox@i[#1]{#2}(b#3)%
+   \inetcell[above=-4ex of b#3.south](#3){$!$}%
+   %\inetcell[above=-4ex of $(b#3.south west)!.75!(b#3.south)$](#3){$!$}%
+}
+
+\makeatother
+
+\endinput