refinement

4 files changed, 14 insertions, 13 deletions

diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex
index eeebf47..57d3195 100644
--- a/chapters/core/implementation/01-inpla.tex
+++ b/chapters/core/implementation/01-inpla.tex
@@ -1,7 +1,7 @@
 \subsection{INPLA fork}
 \label{sec:inpla}
 
-The VEIN reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}},
+The \textbf{VEIN} reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}},
 a multi-threaded parallel interpreter of IN. Performance and ease of use motivated the choice of
 INPLA. Additionally, it supports attribute values, which is a special extension that allows agents
 to hold numerical values at their ports.
@@ -24,7 +24,7 @@ INPLA evaluates nets which consist of connections between terms. Terms are built
 <term> ::= <name> | <agent>
 <name> ::= <nameID>
 <agent> ::= <agentID>
-					| <agentID> ['(' <term> ',' ... ',' <term> ')']
+          | <agentID> ['(' <term> ',' ... ',' <term> ')']
 \end{verbatim}
 \end{small}
 \begin{itemize}
@@ -37,12 +37,12 @@ Interaction rules rewrite connections between agents:
 \begin{verbatim}
 <interaction-rule> ::= <rule-agent> '><' <rule-agent> '=>' <connections> ';'
 <rule-agent> ::= <agentID>
-							 | <agentID> '(' <name> ',' ... ',' <name> ')'
+               | <agentID> '(' <name> ',' ... ',' <name> ')'
 \end{verbatim}
 \end{small}
 
 \paragraph{Example}
-Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successive function). For
+Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successor function). For
 instance, 0, 1, 2, 3 are expressed as \texttt{Z}, \texttt{S(Z)}, \texttt{S(S(Z))}, \texttt{S(S(S(Z)))}. Here, let's think about an
 increment operation ``inc'' such that:
 \begin{small}
diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex
index 49a8a70..8b02c3c 100644
--- a/chapters/core/implementation/02-interaction-rules.tex
+++ b/chapters/core/implementation/02-interaction-rules.tex
@@ -1,7 +1,7 @@
 \subsection{Interaction Rules}
 \label{sec:interaction-rules}
 
-The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into four groups:
+The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into five groups:
 \begin{itemize}
 	\item
 		\textbf{Carriers}: Agents that contain float attributes.
@@ -179,7 +179,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 			(m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{TermSymbolic}$ & (q) $\mathit{TermConcrete}$ \\[0.5cm]
 		\end{tabular}
 	}
-	\caption{Agents used in VEIN.}
+	\caption{Agents used in \textbf{VEIN}.}
 	\label{fig:agents}
 \end{figure}
 
@@ -495,7 +495,7 @@ If, instead, the first operand is a \textit{Linear} agents and the second is a \
 are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) the system adds 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}}) the system multiplies the attribute of
-the \textit{Concrete} agent to both the attributes of the \textit{Linear}
+the \textit{Concrete} agent to both the attributes of the \textit{Linear}.
 
 % Concrete >< AddCheckLinear
 \begin{figure}[H]
diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex
index 0a2eec0..b86e060 100644
--- a/chapters/core/implementation/03-translation.tex
+++ b/chapters/core/implementation/03-translation.tex
@@ -9,7 +9,8 @@ necessary copies of a value required by the next operations. Since nodes do not
 nodes will utilize their outputs, the translation layer traverses the DAG in reverse order
 to be able to instantiate the correct number of \textit{Dup} agents. The main algorithm, illustrated
 in \textbf{\Cref{alg:onnx-to-in}}, maintains an \textit{interactions} dictionary data-structure, that maps each tensor
-name to a list of ports, to keep track of the graph traversal.
+name to a list of ports, to keep track of the graph traversal. The ONNX operators supported are Gemm
+(General matrix multiplication) and ReLU.
 
 \begin{algorithm}[H]
 	\caption{Backwards ONNX-to-IN Translation}
@@ -79,9 +80,9 @@ To maximize the concurrency of the INPLA engine, the translation layer avoids ge
 chains of agents, opting instead for balanced binary trees for signal distribution (single input to
 multiple output) and signal reduction (multiple input to single output). As \textbf{\Cref{alg:balanced-fan-in}}
 and \textbf{\Cref{alg:balanced-fan-out}} illustrate, the depth of agent chains (especially \textit{Dup} chains)
-is limited to $O(\log N)$. The two algorithms are very similar, the difference is in how they wire the
+is limited to $O(\log N)$. The two algorithms are very similar; the difference is in how they wire the
 agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the
-\textit{Fan-Out} they are facing the root.
+\textit{Fan-Out} they face the root.
 
 \begin{algorithm}[H]
 	\caption{Balanced Fan-In}
diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex
index a40df41..6023c2e 100644
--- a/chapters/core/implementation/04-python-module.tex
+++ b/chapters/core/implementation/04-python-module.tex
@@ -1,8 +1,8 @@
 \subsection{Python Module}
 \label{sec:python-module}
 
-The core functionality of the VEIN system is implemented via the \texttt{vein.Solver}, an extension of
-the \texttt{z3.Solver} class offered in the Z3 python
+The core functionality of the \textbf{VEIN} system is implemented via the \texttt{vein.Solver}, an extension of
+the \texttt{z3.Solver} class offered in the Z3 Python
 package\footnote{\href{https://pypi.org/project/z3-solver}{\textbf{PyPi package}}}. This design choice
 ensures flexibility and ease of use for researchers already familiar with using the Z3 Python API.
 
@@ -19,7 +19,7 @@ into a pending queue and it is reduced to normal form only after the \texttt{che
 called.
 
 The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}}
-format. It should contain the input and output symbolic variables declaration, optional range
+format. It should contain the input and output symbolic variables declarations, optional range
 constraints on the input variables and the properties to be verified. For Multi-Network (relational)
 verification, the system ensures that multiple networks share the same input symbolic variables.
 This approach allows Z3 to compare their outputs directly given the same inputs.