started with the report

[master.git] / ar / assignments / 4.tex

diff --git a/ar/assignments/4.tex b/ar/assignments/4.tex
new file mode 100644 (file)
index 0000000..e0f3ac0
--- /dev/null
+++ b/ar/assignments/4.tex
@@ -0,0 +1,54 @@
+\paragraph{Problem 4}
+
+{\em
+Seven integer variables $a_1; a_2; a_3; a_4; a_5; a_6; a_7$ are given, for
+which the initial value of $a_i$ is $i$ for $i=1,\ldots,7$. The following steps
+are defined: choose $i$ with $1<i<7$ and execute
+$$a_i:=a_{i-1}+a_{i+1}$$
+that is, $a_i$ gets the sum of the values of its neighbors and all other
+values remain unchanged. Show how it is possible that after a number of steps
+a number of steps a number $\ge 50$ occurs at least twice in $a_1; a_2; a_3;
+a_4; a_5; a_6; a_7$.
+}
+
+\paragraph{Solution}
+Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations.
+For every $a_i$ in every iteration we make a variable $i_na_i$ where $n$ is the
+number of the iteration. For $a_0$ and $a_7$ we can make an exception since
+they do not change over iterations. For documenting purposes we also keep a counter
+variable $c_n$ for every $n$th iteration. This leads in the initial state
+expressed by:
+
+$$
+\left(c_0=0\right)\wedge
+\left(a_1=1\right)\wedge
+\left(a_I=I\right)\wedge
+\bigwedge_{k=2}^{I-1} \left(i_0a_i = i\right)
+$$
+
+Every next iteration we only increment one $i$ from $2,\ldots,6$.
+
+Say we want to check if the state is reachable in $N$ iterations. Then we can
+specifiy postconditions. For every $i$ we specify this:
+$$\bigvee_{k=2}^{I-1}\left(
+       \left(i_Na_k >= 50\right)\wedge\left(
+               \bigvee_{j=2}^{I-1}\left(i_Na_k=i_Na_j\right)\wedge
+               \left(k\neq j\right)
+       \right)
+\right)$$
+
+$\begin{array}{c|c|ccccc}
+       \# & i & a_2 & a_3 & a_4 & a_5 & a_6\\
+       \hline
+       0 & - & 2 & 3 & 4 & 5 & 6\\
+       1 & 4 & 2 & 3 & \bm{8} & 5 & 6\\
+       2 & 5 & 2 & 3 & 8 & \bm{14} & 6\\
+       3 & 2 & \bm{4} & 3 & 8 & 14 & 6\\
+       4 & 4 & 4 & 3 & \bm{17} & 14 & 6\\
+       5 & 5 & 4 & 3 & 17 & \bm{23} & 6\\
+       6 & 6 & 4 & 3 & 17 & 23 & \bm{30}\\
+       7 & 5 & 4 & 3 & 17 & \bm{47} & 30\\
+       8 & 4 & 4 & 3 & \bm{50} & 47 & 30\\
+       9 & 3 & 4 & \bm{54} & 50 & 47 & 30\\
+       10 & 6 & 4 & 54 & 50 & 47 & \bm{54}\\
+\end{array}$