From 92f75c9d70924d65785c140babe60481a8b18af6 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Fri, 23 Oct 2015 20:18:03 +0200 Subject: [PATCH] final ar --- ar/assignment1/3.tex | 6 ++-- ar/assignment1/4.tex | 14 ++++----- ar/assignment1/a.tex | 8 ++--- ar/assignment1/src/a1.bash | 1 - ar/assignment1/src/a2.py | 1 - ar/assignment1/src/a3.bash | 51 +++++++++++++++++++++++++++++--- ar/assignment1/src/a3.py | 45 ---------------------------- ar/assignment1/src/a4.bash | 60 ++++++++++++++++++++++++++++++++++++-- ar/assignment1/src/a4.py | 53 --------------------------------- 9 files changed, 119 insertions(+), 120 deletions(-) delete mode 100644 ar/assignment1/src/a3.py delete mode 100644 ar/assignment1/src/a4.py 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//$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//$((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("))") -- 2.20.1