From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 23 Oct 2015 18:18:03 +0000 (+0200)
Subject: final ar
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=HEAD;p=master.git

final ar
---

diff --git a/ar/assignment1/3.tex b/ar/assignment1/3.tex
index cf68821..457c1e9 100644
--- a/ar/assignment1/3.tex
+++ b/ar/assignment1/3.tex
@@ -50,14 +50,14 @@ definition.
 \end{itemize}
 
 \subsection{SMT format solution}
-The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a3.py}. The Python
+The formula is easily convertable via a script to SMT format by literal
+conversion and said script is listed in Listing~\ref{listing:a3.bash}. The
 script optimizes a little bit from the original formula by leaving out the
 shared resource checking for the same jobs. The minimization is done by
 incrementing variable $T$ every time the current $T$ yields unsat with a bash
 script shown in Listing~\ref{listing:3.bash}.
 
-\lstinputlisting[language=bash,
+\lstinputlisting[language=bash,firstline=46,
 	caption={Iteratively find the shortest solution for problem 3},
 	label={listing:3.bash}]{src/a3.bash}
 
diff --git a/ar/assignment1/4.tex b/ar/assignment1/4.tex
index 153cfec..68b3242 100644
--- a/ar/assignment1/4.tex
+++ b/ar/assignment1/4.tex
@@ -46,21 +46,21 @@ postcondition.
 
 \subsection{SMT format solution}
 The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a4.py}. The Python
-script optimizes a little bit from the original formula by leaving out the
-$i=j$ comparison in subformula 17 and 18 by removing them from the set looped
-over. The script also optimizes by not checking variables $a_0^n$ and $a_I^n$
-since they always stay the same anyways. The minimization is done by
+conversion and said script is listed in Listing~\ref{listing:a4.bash}. The
+Python script optimizes a little bit from the original formula by leaving out
+the $i=j$ comparison in subformula 17 and 18 by removing them from the set
+looped over. The script also optimizes by not checking variables $a_0^n$ and
+$a_I^n$ since they always stay the same anyways. The minimization is done by
 incrementing variable $N$ every time the current $N$ yields unsat with a bash
 script shown in Listing~\ref{listing:4.bash}.
 
-\lstinputlisting[language=bash,
+\lstinputlisting[language=bash,firstline=58,
 	caption={Iteratively find the shortest solution for problem 4},
 	label={listing:4.bash}]{src/a4.bash}
 
 \subsection{Solution}
 The bash script finds and shows the minimal solution in which the postcondition
-is satisfied for $N=11$. Finding this solution takes less then $75$ seconds and
+is satisfied for $N=10$. Finding this solution takes less then $75$ seconds and
 is shown in Table~\ref{tab:s4}.
 
 Every line in the table represents the iteration and the bold items represent
diff --git a/ar/assignment1/a.tex b/ar/assignment1/a.tex
index e0ac8a3..9785572 100644
--- a/ar/assignment1/a.tex
+++ b/ar/assignment1/a.tex
@@ -14,9 +14,9 @@ RAM: 8GB
 	label={listing:a2.py}]{src/a2.py}
 
 \newpage
-\lstinputlisting[language=python,caption={a3.py},
-	label={listing:a3.py}]{src/a3.py}
+\lstinputlisting[language=python,caption={a3.bash},
+	label={listing:a3.py}]{src/a3.bash}
 
 \newpage
-\lstinputlisting[language=python,caption={a4.py},
-	label={listing:a4.py}]{src/a4.py}
+\lstinputlisting[language=python,caption={a4.bash},
+	label={listing:a4.bash}]{src/a4.bash}
diff --git a/ar/assignment1/src/a1.bash b/ar/assignment1/src/a1.bash
index 5ef0e5f..339536f 100644
--- a/ar/assignment1/src/a1.bash
+++ b/ar/assignment1/src/a1.bash
@@ -4,4 +4,3 @@ while [ $(sed "s/<REP>/$i/g" a1.smt | yices-smt) = "sat" ]; do
 	i=$((i+1))
 done
 echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))"
-sed "s/<REP>/$((i-1))/g" a1.smt | yices-smt -m
diff --git a/ar/assignment1/src/a2.py b/ar/assignment1/src/a2.py
index 529f6b8..a782fe7 100644
--- a/ar/assignment1/src/a2.py
+++ b/ar/assignment1/src/a2.py
@@ -5,7 +5,6 @@ mx = 29
 my = 22
 pd = 17
 
-
 # Print variables and preamble
 print('(benchmark a4.smt')
 print(':logic QF_UFLIA')
diff --git a/ar/assignment1/src/a3.bash b/ar/assignment1/src/a3.bash
index 0a21dee..5b16adc 100644
--- a/ar/assignment1/src/a3.bash
+++ b/ar/assignment1/src/a3.bash
@@ -1,7 +1,50 @@
+#!/bin/bash
+JOBS=12
+J=$(seq 1 $JOBS)
+JPRIME="5 7 10"
+
+function pi {
+	case $1 in
+		3) echo 1 2;;
+		5) echo 3 4;;
+		7) echo 3 4 6;;
+		9) echo 5 8;;
+		11) echo 10;;
+		12) echo 9 11;;
+		*);;
+	esac
+}
+
+function generate {
+	local i j
+	echo "(benchmark a4.smt"
+	echo ":logic QF_UFLIA"
+	echo ":extrafuns ("
+	for i in $J; do
+		echo "(j$i Int)"
+	done
+	echo ")"
+	echo ":formula"
+	echo "(and"
+	for i in $J; do
+		echo "(> j$i 0) (<= (+ j$i $i) $1)"
+		for j in $(pi $i); do
+			echo "(>= j$i (+ j$j $j))"
+		done
+	done
+	for i in $JPRIME; do
+		for j in $JPRIME; do
+			if [ $i != $j ]; then
+				echo "(or (>= j$i (+ j$j $j))"
+				echo "    (<= (+ j$i $i) j$j))"
+			fi
+		done
+	done
+	echo "))"
+}
+
 i=1
-while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do
-	echo "T=$i is still unsat"
-	i=$((i+1))
+while [ $(generate $i | yices-smt) = "unsat" ]; do
+	echo "T=$((i++)) is still unsat"
 done
 echo "T=$i is sat thus the minimum T=$i"
-python3 a3.py $i | yices-smt -m
diff --git a/ar/assignment1/src/a3.py b/ar/assignment1/src/a3.py
deleted file mode 100644
index 1d7a848..0000000
--- a/ar/assignment1/src/a3.py
+++ /dev/null
@@ -1,45 +0,0 @@
-#!/usr/bin/env python3
-import sys
-
-if len(sys.argv) != 2:
-    print('usage: {} maxjobstart'.format(sys.argv[0]))
-    exit()
-
-maxjobstart = sys.argv[1]
-jobs = 12
-J = range(1, jobs+1)
-Jprime = {5, 7, 10}
-pi = {
-    3: {1, 2},
-    5: {3, 4},
-    7: {3, 4, 6},
-    9: {5, 8},
-    11: {10},
-    12: {9, 11}
-}
-
-# Print variables and preamble
-print('(benchmark a4.smt')
-print(':logic QF_UFLIA')
-print(':extrafuns (')
-for i in J:
-    print('(j{} Int)'.format(i), end=' ')
-print('\n)')
-
-print(':formula')
-print('(and')
-for i in J:
-    # Make sure the times are positive and within the bound
-    print('(> j{0} 0) (<= (+ j{0} {0}) {1})'.format(i, maxjobstart))
-    # Make sure the dependencies are done when a task is scheduled
-    for k in pi.get(i, {}):
-        print('(>= j{0} (+ j{1} {1}))'.format(i, k))
-# Make sure the shared resources are not used by two tasks at once
-for i in Jprime:
-    for k in Jprime:
-        if i != k:
-            print('(or (>= j{0} (+ j{1} {1}))'.format(i, k), end=' ')
-            print('(<= (+ j{0} {0}) j{1}))'.format(i, k))
-
-# Close the and,benchmark parenthesis
-print('))')
diff --git a/ar/assignment1/src/a4.bash b/ar/assignment1/src/a4.bash
index 23abab8..7f9e0f9 100644
--- a/ar/assignment1/src/a4.bash
+++ b/ar/assignment1/src/a4.bash
@@ -1,7 +1,63 @@
+#!/usr/bin/env python3
+NUMA=7
+
+function generate {
+	local i n j
+	echo "(benchmark a4.smt"
+	echo ":logic QF_UFLIA"
+	echo ":extrafuns ("
+	echo "(a1 Int)"
+	echo "(a$NUMA Int)"
+	for i in $(seq 2 $((NUMA-1))); do
+		for n in $(seq 0 $1); do
+			echo "(i${n}a$i Int)"
+		done
+	done
+	echo ")"
+	echo ":formula"
+	echo "(and"
+
+	echo "(= a1 1)"
+	echo "(= a$NUMA $NUMA)"
+	for i in $(seq 2 $((NUMA-1))); do
+		echo "(= i0a$i $i)"
+	done
+
+	for n in $(seq 1 $1); do
+		echo "(or"
+		for i in $(seq 2 $((NUMA-1))); do
+			echo "(and"
+			[ $i = 2 ] && prev=1 || prev="i$((n-1))a$((i-1))"
+			[ $i = $((NUMA-1)) ] && next=7 || next="i$((n-1))a$((i+1))"
+			echo "(= i${n}a$i (+ $prev $next)) "
+			for j in $(seq 2 $((NUMA-1))); do
+				if [ $i != $j ]; then
+					echo "(= i${n}a$j i$((n-1))a$j)"
+				fi
+			done
+			echo ")"
+		done
+		echo ")"
+	done
+
+	echo "(or"
+	for i in $(seq 2 $((NUMA-1))); do
+		echo "(and"
+		echo "(>= i${1}a$i 50)"
+		echo "(or"
+		for j in $(seq 2 $((NUMA-1))); do
+			if [ $i != $j ]; then
+				echo "(= i${1}a$i i${1}a$j)"
+			fi
+		done
+		echo "))"
+	done
+	echo ")))"
+}
+
 i=1
-while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do
+while [ $(generate $i | yices-smt) = "unsat" ]; do
 	echo "N=$i is still unsat"
 	i=$((i+1))
 done
 echo "N=$i is sat thus minimum N=$i"
-python3 a4.py $i | yices-smt -m
diff --git a/ar/assignment1/src/a4.py b/ar/assignment1/src/a4.py
deleted file mode 100644
index 8883695..0000000
--- a/ar/assignment1/src/a4.py
+++ /dev/null
@@ -1,53 +0,0 @@
-#!/usr/bin/env python3
-import sys
-if len(sys.argv) != 2:
-    print("usage: {} maxiterations".format(sys.argv[0]))
-    exit()
-
-iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11
-numa = 7
-
-# Print variables and preamble
-print("(benchmark a4.smt")
-print(":logic QF_UFLIA")
-print(":extrafuns (")
-print("(a{} Int)".format(1))
-print("(a{} Int)".format(numa))
-for i in range(iterations):
-    for v in range(2, numa):
-        print("(i{}a{} Int) ".format(i, v))
-print(")")
-
-# Print preconditions
-print(":formula")
-print("(and")
-print("(= a1 1)")
-print("(= a{0} {0})".format(numa, numa))
-for i in range(2, numa):
-    print("(= i0a{0} {0})".format(i))
-
-# Print iterations
-for i in range(1, iterations):
-    print("(or")
-    for v in range(2, numa):
-        print("(and")
-        for ov in [k for k in range(2, numa) if k != v]:
-            print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
-        im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
-        ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
-        print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
-        print(")")
-    print(")")
-
-#  Post conditions
-print("(or")
-for v in range(2, numa):
-    print("(and (>= i{}a{} 50)".format(iterations-1, v))
-    print("(or")
-    for ov in [k for k in range(2, numa) if k != v]:
-        print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
-    print("))")
-print(")")
-
-#  Close the and,benchmark parenthesis
-print("))")