A bunch of fixes to the solver, and moving it in to clang.

Also some contribution writing stuff.

Basically: lots of work.

1 files changed, 25 insertions, 5 deletions

diff --git a/tex/thesis/contribution/contribution.tex b/tex/thesis/contribution/contribution.tex
index 66d5b4a..3d00b86 100644
--- a/tex/thesis/contribution/contribution.tex
+++ b/tex/thesis/contribution/contribution.tex
@@ -130,11 +130,31 @@ algorithm is presented in Listing \ref{algo:kleene}.
 For each iteration the entire system is evaluated, irrespective of
 whether it could possibly have changed value. This results in a
 considerable inefficiency in practice, requiring the evaluation of
-$O(n^3)$ right-hand-sides, and thus an approach which can evaluate
-smaller portions of the system in each iteration would be a
-significant improvement.
+many right-hand-sides repeatedly for the same value. Thus an
+approach which can evaluate smaller portions of the system in each
+iteration would be a significant improvement.
+
+An additional deficiency of Kleene iteration is that it is not
+guaranteed to terminate. In some cases Kleene iteration must iterate
+an infinite number of times in order to reach a fixpoint. An example
+system is presented as Figure \ref{fig:kleene-infinite}. In this case
+$x$ will take the value of $0$ in the first iteration, then $y$ will
+evaluate to $-1$. In the next iteration $x$ will also take the value
+$-1$, thereby requiring $y$ to take the value $-2$. This will continue
+without bound, resulting in the Kleene iteration never reaching the
+greatest fixpoint of $\{ x \mapsto -\infty, y \mapsto -\infty \}$.
+
+\begin{figure}[H]
+  \begin{align*}
+    x &= \min(0, x) \\
+    y &= x - 1
+  \end{align*}
+  \caption{An example equation system for which Kleene iteration will
+    not terminate}
+  \label{fig:kleene-infinite}
+\end{figure}
 
-\subsection{W-DFS algorithm} \ref{sec:wdfs}
+\subsection{W-DFS algorithm} \label{sec:wdfs}
 
 The W-DFS algorithm presented by Seidl, et al. takes into account some
 form of data-dependencies as it solves the system. This gives it the
@@ -255,7 +275,7 @@ problem it is possible
 \end{algorithm}
 
 
-\subsection{Adapted W-DFS algorithm} \ref{sec:adapted-wdfs}
+\subsection{Adapted W-DFS algorithm} \label{sec:adapted-wdfs}
 
 This, then, allows us to use the W-DFS algorithm to re-evaluate only
 those parts of the strategy which have changed. Listing