done with 1

diff --git a/a2/1.tex b/a2/1.tex
index 11692f6..8aeb788 100644 (file)
--- 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.}
        \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.
                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
                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{table}[H]
                        \centering

-                       \begin{tabular}{ccccccc}
+                       \begin{tabular}{lrrrrcr}

                                \toprule
                                $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
                                \midrule
                                \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}
                                \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$.}
        \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}
 \end{enumerate}

diff --git a/a2/src/1a.bash b/a2/src/1a.bash
index 1724514..f157243 100755 (executable)
--- a/a2/src/1a.bash
+++ b/a2/src/1a.bash
@@ -160,7 +160,7 @@ GEN
        echo ")))"
 }
 it=1
        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
 do
        echo $((it++))
 done