From c6c5b35f65e4bb0b91554b65de1403345a41cc1a Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 4 Jan 2016 10:06:46 +0100
Subject: [PATCH] fixed 1

---
 a2/1.tex       |  74 ++++++++++-----------
 a2/src/1a.bash |  18 ++---
 a2/src/1b.bash | 155 ++++++++++++++++++++++++++++---------------
 a2/src/1c.bash | 175 +++++++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 323 insertions(+), 99 deletions(-)
 mode change 100755 => 100644 a2/src/1a.bash
 mode change 100755 => 100644 a2/src/1b.bash
 create mode 100644 a2/src/1c.bash

diff --git a/a2/1.tex b/a2/1.tex
index 324e7d8..6de7ceb 100644
--- a/a2/1.tex
+++ b/a2/1.tex
@@ -38,18 +38,20 @@ We reason about the new iteration $i$ from the things we know about iteration
 $i-1$. The crucial part is the location we were in iteration $i-1$ and we make
 a disjunction over all possible cities and describe the result in the following
 formula called $trans$. We introduce a function $conn(s)$ that returns the set
-of all cities connected to city $s$. $(2)$ deals with the fact that the truck
-can not dump any food in city $S$ and constraints the amount of food dumped in
-the city. $(3)$ deals with the fact that the dumped food is added to the
-current stock of the city. Sub formula $(4)$ deals with the fact that if the
-truck is in $S$ it is replenished and otherwise the dumped load is subtracted
-from the trucks load. Finally $(5)$ deals with the other cities which will have
-their stock decremented with the distance traveled.
+of all cities connected to city $s$. To begin with $(1)$ sets the location of
+the previous iteration correct and checks whether the city will not run out of
+food while travelled too. $(2)$ deals with the fact that the truck can not dump
+any food in city $S$ and constraints the amount of food dumped in the city.
+$(3)$ deals with the fact that the dumped food is added to the current stock of
+the city. Sub formula $(4)$ deals with the fact that if the truck is in $S$ it
+is replenished and otherwise the dumped load is subtracted from the trucks
+load. Finally $(5)$ deals with the other cities which will have their stock
+decremented with the distance traveled.
 
 \begin{align}
 	\bigvee_{k\in\{S\}\cup V}
 		l_{i-1}=k\wedge
-		\bigvee_{k'\in conn(k)} & l_i=k'\wedge\\
+		\bigvee_{k'\in conn(k)} & l_i=k'\wedge k'_{i-1}\geq dist(k,k')\wedge\\
 			& (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
 			& (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
 			& (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
@@ -65,10 +67,14 @@ $$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.
-
+		Incrementally increasing the number of iterations does result in
+		finding an unsatisfiable formula with $I=21$. Thus there is no infinite
+		path that keeps the cities saturated forever.
+	\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 state space
 		that is exactly the same as some previous state. To do this we add the
 		following formula to the conjunction.
@@ -77,40 +83,34 @@ $$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. The amount dumped is only shown for more readability. For state
-		isomorphism it is not a factor.
+		when we have more then $10$ iterations we encounter a cycle. This is
+		shown in Table~\ref{tbl:s3b} where iteration $4$ and iteration $11$ are
+		equal. 
 		\begin{table}[H]
 			\centering
 			\begin{tabular}{lrrrrcr}
 				\toprule
 				$I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
 				\midrule
-				$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}\\
+				$0$ &  $40$  & $30$  & $145$ & $320$ & $S$ & $0$\\
+				$1$ &  $19$  & $35$  & $124$ & $294$ & $B$ & $26$\\
+				$2$ &  $120$ & $18$  & $107$ & $176$ & $A$ & $118$\\  
+				$3$ &  $103$ & $120$ & $90$  & $57$  & $B$ & $119$\\   
+				\textbf{4} & \textbf{82} & \textbf{99} & \textbf{69} &
+					\textbf{320} & \textbf{S} & \textbf{0}\\
+				$5$ &  $119$ & $70$  & $40$  & $254$ & $A$ & $66$\\    
+				$6$ &  $87$  & $38$  & $194$ & $68$  & $C$ & $186$\\
+				$7$ &  $50$  & $67$  & $157$ & $2$   & $B$ & $66$\\
+				$8$ &  $29$  & $46$  & $136$ & $320$ & $S$ & $0$\\
+				$9$ &  $120$ & $17$  & $107$ & $200$ & $A$ & $120$\\  
+				$10$ & $103$ & $120$ & $90$  & $80$  & $B$ & $120$\\
+				\textbf{11} & \textbf{82} & \textbf{99} & \textbf{69} &
+					\textbf{320} & \textbf{S} & \textbf{0}\\
 				\bottomrule
 			\end{tabular}
+			\caption{Solution for problem $3b$}\label{tbl:s3b}
 		\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
old mode 100755
new mode 100644
index f157243..e39419f
--- a/a2/src/1a.bash
+++ b/a2/src/1a.bash
@@ -37,6 +37,7 @@ GEN
 			(= l$((i-1)) 0)
 			(or
 				(and ; now in A
+					(>= a$((i-1)) 29)
 					(= l$i 1)
 					(<= d$i (+ 29 (- $AMAX a$((i-1)))))
 					(= a$i (+ (- a$((i-1)) 29) d$i))
@@ -46,6 +47,7 @@ GEN
 
 					(= t$i (- t$((i-1)) d$i))
 				) (and ; now in B
+					(>= b$((i-1)) 21)
 					(= l$i 2)
 					(<= d$i (+ 21 (- $BMAX b$((i-1)))))
 					(= b$i (+ (- b$((i-1)) 21) d$i))
@@ -70,6 +72,7 @@ GEN
 
 					(= t$i $TMAX)
 				) (and ; now in B
+					(>= b$((i-1)) 17)
 					(= l$i 2)
 					(<= d$i (+ 17 (- $BMAX b$((i-1)))))
 					(= b$i (+ (- b$((i-1)) 17) d$i))
@@ -79,6 +82,7 @@ GEN
 
 					(= t$i (- t$((i-1)) d$i))
 				) (and ; now in C
+					(>= c$((i-1)) 32)
 					(= l$i 3)
 
 					(<= d$i (+ 32 (- $CMAX c$((i-1)))))
@@ -104,6 +108,7 @@ GEN
 
 					(= t$i $TMAX)
 				) (and ; now in A
+					(>= a$((i-1)) 17)
 					(= l$i 1)
 					(<= d$i (+ 17 (- $AMAX a$((i-1)))))
 					(= a$i (+ (- a$((i-1)) 17) d$i))
@@ -113,6 +118,7 @@ GEN
 
 					(= t$i (- t$((i-1)) d$i))
 				) (and ; now in C
+					(>= c$((i-1)) 37)
 					(= l$i 3)
 					(<= d$i (+ 37 (- $CMAX c$((i-1)))))
 					(= c$i (+ (- c$((i-1)) 37) d$i))
@@ -128,6 +134,7 @@ GEN
 			(= l$((i-1)) 3)
 			(or
 				(and ; now in A
+					(>= a$((i-1)) 32)
 					(= l$i 1)
 					(<= d$i (+ 32 (- $AMAX a$((i-1)))))
 					(= a$i (+ (- a$((i-1)) 32) d$i))
@@ -137,6 +144,7 @@ GEN
 
 					(= t$i (- t$((i-1)) d$i))
 				) (and ; now in B
+					(>= b$((i-1)) 37)
 					(= l$i 2)
 					(<= d$i (+ 37 (- $BMAX b$((i-1)))))
 					(= b$i (+ (- b$((i-1)) 37) d$i))
@@ -151,16 +159,10 @@ GEN
 	)
 GEN
 	done
-	echo "(or"
-	for i in $(seq 0 $ITERATIONS); do
-		for j in $(seq $((i+1)) $ITERATIONS); do
-			echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
-		done
-	done
-	echo ")))"
+	echo "))"
 }
 it=1
-while generate $it 300 | $YICES -m | pee sort "grep -q unsat"
+while generate $it 300 | $YICES | pee sort "grep -q \"^sat\""
 do
 	echo $((it++))
 done
diff --git a/a2/src/1b.bash b/a2/src/1b.bash
old mode 100755
new mode 100644
index 17a3e78..bbed09f
--- a/a2/src/1b.bash
+++ b/a2/src/1b.bash
@@ -28,82 +28,131 @@ GEN
 	(> a$i 0)
 	(> b$i 0)
 	(> c$i 0)
+	(>= d$i 0)
+	(<= d$i $TMAX)
+	(>= t$i 0)
+	(<= t$i $TMAX)
 	(or ;-- ITERATION $i
-		(and ;-- SPECIAL CASE FOR STATE S(0)
-			(= l$i 0)
-			(= d$i 0)
-			(= t$i $TMAX)
+		(and ;-- WAS IN S
+			(= l$((i-1)) 0)
 			(or
-				(and ;-- CAME FROM A
-					(= l$((i-1)) 1)
-					(= a$i (- a$((i-1)) 29))
+				(and ; now in A
+					(>= a$((i-1)) 29)
+					(= l$i 1)
+					(<= d$i (+ 29 (- $AMAX a$((i-1)))))
+					(= a$i (+ (- a$((i-1)) 29) d$i))
+
 					(= b$i (- b$((i-1)) 29))
 					(= c$i (- c$((i-1)) 29))
-				)
-				(and ;-- CAME FROM B
-					(= l$((i-1)) 2)
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in B
+					(>= b$((i-1)) 21)
+					(= l$i 2)
+					(<= d$i (+ 21 (- $BMAX b$((i-1)))))
+					(= b$i (+ (- b$((i-1)) 21) d$i))
+
 					(= a$i (- a$((i-1)) 21))
-					(= b$i (- b$((i-1)) 21))
 					(= c$i (- c$((i-1)) 21))
+
+					(= t$i (- t$((i-1)) d$i))
 				)
 			)
 		)
-		(and ;-- CASE FOR STATE A(1)
-			(= l$i 1) 
-			(>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $AMAX a$((i-1))))
-			(= t$i (- t$((i-1)) d$i)) (= a$i (+ a$((i-1)) d$i))
-			
+		(and ;-- WAS IN A
+			(= l$((i-1)) 1)
 			(or
-				(and  ;-- CAME FROM S(0)
-					(= l$((i-1)) 0)
+				(and ; now in S
+					(= l$i 0)
+					(= d$i 0)
+
+					(= a$i (- a$((i-1)) 29))
 					(= b$i (- b$((i-1)) 29))
-				   	(= c$i (- c$((i-1)) 29))
-				) (and  ;-- CAME FROM B(2)
-					(= l$((i-1)) 2)
-					(= b$i (- b$((i-1)) 17))
+					(= c$i (- c$((i-1)) 29))
+
+					(= t$i $TMAX)
+				) (and ; now in B
+					(>= b$((i-1)) 17)
+					(= l$i 2)
+					(<= d$i (+ 17 (- $BMAX b$((i-1)))))
+					(= b$i (+ (- b$((i-1)) 17) d$i))
+
+					(= a$i (- a$((i-1)) 17))
 					(= c$i (- c$((i-1)) 17))
-				) (and ;-- CAME FROM C(3)
-					(= l$((i-1)) 3)
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in C
+					(>= c$((i-1)) 32)
+					(= l$i 3)
+
+					(<= d$i (+ 32 (- $CMAX c$((i-1)))))
+					(= c$i (+ (- c$((i-1)) 32) d$i))
+
+					(= a$i (- a$((i-1)) 32))
 					(= b$i (- b$((i-1)) 32))
-					(= c$i (- c$((i-1)) 32))
+
+					(= t$i (- t$((i-1)) d$i))
 				)
 			)
 		)
-		(and ;-- CASE FOR STATE B(2)
-			(= l$i 2)
-			(>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $BMAX b$((i-1))))
-			(= t$i (- t$((i-1)) d$i)) (= b$i (+ b$((i-1)) d$i))
-
+		(and ;-- WAS IN B
+			(= l$((i-1)) 2)
 			(or
-				(and  ;-- CAME FROM S(0)
-					(= l$((i-1)) 0)
+				(and ; now in S
+					(= l$i 0)
+					(= d$i 0)
+
 					(= a$i (- a$((i-1)) 21))
-				   	(= c$i (- c$((i-1)) 21))
-				) (and  ;-- CAME FROM A(1)
-					(= l$((i-1)) 1)
-					(= a$i (- a$((i-1)) 17))
+					(= b$i (- b$((i-1)) 21))
+					(= c$i (- c$((i-1)) 21))
+
+					(= t$i $TMAX)
+				) (and ; now in A
+					(>= a$((i-1)) 17)
+					(= l$i 1)
+					(<= d$i (+ 17 (- $AMAX a$((i-1)))))
+					(= a$i (+ (- a$((i-1)) 17) d$i))
+
+					(= b$i (- b$((i-1)) 17))
 					(= c$i (- c$((i-1)) 17))
-				) (and ;-- CAME FROM C(3)
-					(= l$((i-1)) 3)
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in C
+					(>= c$((i-1)) 37)
+					(= l$i 3)
+					(<= d$i (+ 37 (- $CMAX c$((i-1)))))
+					(= c$i (+ (- c$((i-1)) 37) d$i))
+
 					(= a$i (- a$((i-1)) 37))
-					(= c$i (- c$((i-1)) 37))
+					(= b$i (- b$((i-1)) 37))
+
+					(= t$i (- t$((i-1)) d$i))
 				)
 			)
 		)
-		(and ;-- CASE FOR STATE C(3)
-			(= l$i 3)
-			(>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $CMAX c$((i-1))))
-			(= t$i (- t$((i-1)) d$i)) (= c$i (+ c$((i-1)) d$i))
-
+		(and ;-- WAS IN C
+			(= l$((i-1)) 3)
 			(or
-				(and  ;-- CAME FROM A(1)
-					(= l$((i-1)) 1)
-					(= a$i (- a$((i-1)) 32))
+				(and ; now in A
+					(>= a$((i-1)) 32)
+					(= l$i 1)
+					(<= d$i (+ 32 (- $AMAX a$((i-1)))))
+					(= a$i (+ (- a$((i-1)) 32) d$i))
+
 					(= b$i (- b$((i-1)) 32))
-				) (and ;-- CAME FROM B(2)
-					(= l$((i-1)) 2)
+					(= c$i (- c$((i-1)) 32))
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in B
+					(>= b$((i-1)) 37)
+					(= l$i 2)
+					(<= d$i (+ 37 (- $BMAX b$((i-1)))))
+					(= b$i (+ (- b$((i-1)) 37) d$i))
+
 					(= a$i (- a$((i-1)) 37))
-					(= b$i (- b$((i-1)) 37))
+					(= c$i (- c$((i-1)) 37))
+
+					(= t$i (- t$((i-1)) d$i))
 				)
 			)
 		)
@@ -118,10 +167,8 @@ GEN
 	done
 	echo ")))"
 }
-
 it=1
-while generate $it 320 | $YICES -m | pee sort "grep unsat"
+while generate $it 320 | $YICES -m | pee sort "grep -q unsat"
 do
-	it=$((it+1))
+	echo $((it++))
 done
-echo $it
diff --git a/a2/src/1c.bash b/a2/src/1c.bash
new file mode 100644
index 0000000..f8ba916
--- /dev/null
+++ b/a2/src/1c.bash
@@ -0,0 +1,175 @@
+#!/bin/bash
+YICES=~/projects/yices-2.4.2/bin/yices-smt
+AI=40
+BI=30
+CI=145
+AMAX=120
+BMAX=120
+CMAX=200
+
+function generate {
+	ITERATIONS=$1
+	TMAX=$2
+	cat<<GEN
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+$(	for i in $(seq 0 $ITERATIONS); do
+		echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
+	done)
+)
+:formula
+(and
+	;-- PRECONDITION
+	(and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0))
+GEN
+	for i in $(seq 1 $ITERATIONS); do
+		cat<<GEN
+	(> a$i 0)
+	(> b$i 0)
+	(> c$i 0)
+	(>= d$i 0)
+	(<= d$i $TMAX)
+	(>= t$i 0)
+	(<= t$i $TMAX)
+	(or ;-- ITERATION $i
+		(and ;-- WAS IN S
+			(= l$((i-1)) 0)
+			(or
+				(and ; now in A
+					(>= a$((i-1)) 29)
+					(= l$i 1)
+					(<= d$i (+ 29 (- $AMAX a$((i-1)))))
+					(= a$i (+ (- a$((i-1)) 29) d$i))
+
+					(= b$i (- b$((i-1)) 29))
+					(= c$i (- c$((i-1)) 29))
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in B
+					(>= b$((i-1)) 21)
+					(= l$i 2)
+					(<= d$i (+ 21 (- $BMAX b$((i-1)))))
+					(= b$i (+ (- b$((i-1)) 21) d$i))
+
+					(= a$i (- a$((i-1)) 21))
+					(= c$i (- c$((i-1)) 21))
+
+					(= t$i (- t$((i-1)) d$i))
+				)
+			)
+		)
+		(and ;-- WAS IN A
+			(= l$((i-1)) 1)
+			(or
+				(and ; now in S
+					(= l$i 0)
+					(= d$i 0)
+
+					(= a$i (- a$((i-1)) 29))
+					(= b$i (- b$((i-1)) 29))
+					(= c$i (- c$((i-1)) 29))
+
+					(= t$i $TMAX)
+				) (and ; now in B
+					(>= b$((i-1)) 17)
+					(= l$i 2)
+					(<= d$i (+ 17 (- $BMAX b$((i-1)))))
+					(= b$i (+ (- b$((i-1)) 17) d$i))
+
+					(= a$i (- a$((i-1)) 17))
+					(= c$i (- c$((i-1)) 17))
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in C
+					(>= c$((i-1)) 32)
+					(= l$i 3)
+
+					(<= d$i (+ 32 (- $CMAX c$((i-1)))))
+					(= c$i (+ (- c$((i-1)) 32) d$i))
+
+					(= a$i (- a$((i-1)) 32))
+					(= b$i (- b$((i-1)) 32))
+
+					(= t$i (- t$((i-1)) d$i))
+				)
+			)
+		)
+		(and ;-- WAS IN B
+			(= l$((i-1)) 2)
+			(or
+				(and ; now in S
+					(= l$i 0)
+					(= d$i 0)
+
+					(= a$i (- a$((i-1)) 21))
+					(= b$i (- b$((i-1)) 21))
+					(= c$i (- c$((i-1)) 21))
+
+					(= t$i $TMAX)
+				) (and ; now in A
+					(>= a$((i-1)) 17)
+					(= l$i 1)
+					(<= d$i (+ 17 (- $AMAX a$((i-1)))))
+					(= a$i (+ (- a$((i-1)) 17) d$i))
+
+					(= b$i (- b$((i-1)) 17))
+					(= c$i (- c$((i-1)) 17))
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in C
+					(>= c$((i-1)) 37)
+					(= l$i 3)
+					(<= d$i (+ 37 (- $CMAX c$((i-1)))))
+					(= c$i (+ (- c$((i-1)) 37) d$i))
+
+					(= a$i (- a$((i-1)) 37))
+					(= b$i (- b$((i-1)) 37))
+
+					(= t$i (- t$((i-1)) d$i))
+				)
+			)
+		)
+		(and ;-- WAS IN C
+			(= l$((i-1)) 3)
+			(or
+				(and ; now in A
+					(>= a$((i-1)) 32)
+					(= l$i 1)
+					(<= d$i (+ 32 (- $AMAX a$((i-1)))))
+					(= a$i (+ (- a$((i-1)) 32) d$i))
+
+					(= b$i (- b$((i-1)) 32))
+					(= c$i (- c$((i-1)) 32))
+
+					(= t$i (- t$((i-1)) d$i))
+				) (and ; now in B
+					(>= b$((i-1)) 37)
+					(= l$i 2)
+					(<= d$i (+ 37 (- $BMAX b$((i-1)))))
+					(= b$i (+ (- b$((i-1)) 37) d$i))
+
+					(= a$i (- a$((i-1)) 37))
+					(= c$i (- c$((i-1)) 37))
+
+					(= t$i (- t$((i-1)) d$i))
+				)
+			)
+		)
+	)
+GEN
+	done
+#	echo "(or"
+#	for i in $(seq 0 $ITERATIONS); do
+#		for j in $(seq $((i+1)) $ITERATIONS); do
+#			echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
+#		done
+#	done
+#	echo ")"
+	echo "))"
+}
+it=1
+while generate $it 318 | $YICES | pee sort "grep -q \"^sat\""
+do
+	echo $((it++))
+done
-- 
2.20.1