From 9b9a11f66ee708f6ae7a2e111a8a69ba554e0b74 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 3 Jan 2016 17:34:48 +0100
Subject: [PATCH] done with 1

---
 a2/1.tex       | 44 +++++++++++++++++++++++++++-----------------
 a2/src/1a.bash |  2 +-
 2 files changed, 28 insertions(+), 18 deletions(-)

diff --git a/a2/1.tex b/a2/1.tex
index 11692f6..8aeb788 100644
--- a/a2/1.tex
+++ b/a2/1.tex
@@ -65,12 +65,10 @@ $$const\wedge initial\wedge
 	\item \emph{Show that it is impossible to deliver food packages in such a
 		way that each of the villages consumes one food package per time unit
 		forever.}
+		Incrementally increasing the number of iterations does not result in a
+		state where a city is without food. Therefore we try to find proof that
+		the truck is actually capable of keeping all cities saturated.
 
-	\item \emph{Show that this is possible if the capacity of the truck is
-		increased to 320 food packages. (Note that a finite graph contains an
-		infinite path starting in a node $v$ if and only if there is a path
-		from $v$ to a node $w$ for which there is a non-empty path from $w$ to
-		itself.)}
 		To show this we need to prove that there is a state in the statespace
 		that is exactly the same as some previous state. To do this we add the
 		following formula to the conjunction.
@@ -81,26 +79,38 @@ $$const\wedge initial\wedge
 		When we incrementally increase the number of iterations we see that
 		when we have more then $8$ iterations we encounter a cycle. This is
 		shown in the following table where iteration $2$ and iteration $9$ are
-		equal.
+		equal. The amount dumped is only shown for more readability. For state
+		isomorphism it is not a factor.
 		\begin{table}[H]
 			\centering
-			\begin{tabular}{ccccccc}
+			\begin{tabular}{lrrrrcr}
 				\toprule
 				$I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
 				\midrule
-				$0$ & $40$ & $30$ & $145$ & $320$ & $0$ & $0$\\
-				$1$ & $19$ & $22$ & $124$ & $307$ & $2$ & $9$\\
-				$2$ & $96$ & $5$ & $107$ & $213$ & $1$ & $98$\\
-				$3$ & $79$ & $119$ & $90$ & $82$ & $2$ & $133$\\
-				$4$ & $58$ & $98$ & $69$ & $320$ & $0$ & $0$\\
-				$5$ & $108$ & $69$ & $40$ & $241$ & $1$ & $79$\\
-				$6$ & $76$ & $37$ & $194$ & $55$ & $3$ & $186$\\
-				$7$ & $39$ & $55$ & $157$ & $0$ & $2$ & $53$\\
-				$8$ & $18$ & $34$ & $136$ & $320$ & $0$ & $0$\\
-				$9$ & $96$ & $5$ & $107$ & $213$ & $1$ & $107$\\
+				$0$ & $40$  & $30$  & $145$ & $300$ & $S$ & $0$\\
+				$1$ & $19$  & $36$  & $124$ & $273$ & $B$ & $27$\\
+				\textbf{2} & \textbf{120} & \textbf{19}  & \textbf{107} &
+					\textbf{155} & \textbf{A} & \textbf{118}\\
+				$3$ & $103$ & $117$ & $90$  & $40$  & $B$ & $115$\\
+				$4$ & $82$  & $96$  & $69$  & $300$ & $S$ & $0$\\
+				$5$ & $94$  & $67$  & $40$  & $259$ & $A$ & $41$\\
+				$6$ & $62$  & $35$  & $194$ & $73$  & $C$ & $186$\\
+				$7$ & $25$  & $69$  & $157$ & $2$   & $B$ & $71$\\
+				$8$ & $4$   & $48$  & $136$ & $300$ & $S$ & $0$\\
+				\textbf{9} & \textbf{120} & \textbf{19}  & \textbf{107} &
+					\textbf{155} & \textbf{A} & \textbf{145}\\
 				\bottomrule
 			\end{tabular}
 		\end{table}
+	\item \emph{Show that this is possible if the capacity of the truck is
+		increased to 320 food packages. (Note that a finite graph contains an
+		infinite path starting in a node $v$ if and only if there is a path
+		from $v$ to a node $w$ for which there is a non-empty path from $w$ to
+		itself.)}
+		Solution idem to $a.$. Just imagine the truck operator glueing $20$
+		food packages to the truck which he can not deliver.
 	\item \emph{Figure out whether it is possible if the capacity of the truck
 		is set to $318$.}
+		Solution idem to $a.$. Just imagine the truck operator glueing $18$
+		food packages to the truck which he can not deliver.
 \end{enumerate}
diff --git a/a2/src/1a.bash b/a2/src/1a.bash
index 1724514..f157243 100755
--- a/a2/src/1a.bash
+++ b/a2/src/1a.bash
@@ -160,7 +160,7 @@ GEN
 	echo ")))"
 }
 it=1
-while generate $it 318 | $YICES -m | pee sort "grep -q unsat"
+while generate $it 300 | $YICES -m | pee sort "grep -q unsat"
 do
 	echo $((it++))
 done
-- 
2.20.1