final ar

diff --git a/ar/assignment1/3.tex b/ar/assignment1/3.tex
index cf68821..457c1e9 100644 (file)
--- a/ar/assignment1/3.tex
+++ b/ar/assignment1/3.tex
@@ -50,14 +50,14 @@ definition.
 \end{itemize}
 
 \subsection{SMT format solution}
 \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}.
 
 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}
 
        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 (file)
--- 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
 
 \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}.
 
 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
        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
 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 (file)
--- a/ar/assignment1/a.tex
+++ b/ar/assignment1/a.tex
@@ -14,9 +14,9 @@ RAM: 8GB
        label={listing:a2.py}]{src/a2.py}
 
 \newpage
        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
 
 \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 (file)
--- 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))"
        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 (file)
--- a/ar/assignment1/src/a2.py
+++ b/ar/assignment1/src/a2.py
@@ -5,7 +5,6 @@ mx = 29
 my = 22
 pd = 17
 
 my = 22
 pd = 17
 

-

 # Print variables and preamble
 print('(benchmark a4.smt')
 print(':logic QF_UFLIA')
 # 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 (file)
--- 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
 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"
 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 (file)
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 (file)
--- 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
 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"
        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 (file)
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("))")