LaTeX 0 - Camil 1

1 files changed, 36 insertions, 36 deletions

diff --git a/Assignment2/report/implementation.tex b/Assignment2/report/implementation.tex
index 3acdea6..1df4217 100644
--- a/Assignment2/report/implementation.tex
+++ b/Assignment2/report/implementation.tex
@@ -21,42 +21,6 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists
 	\caption{The DRN file representing the unfair Knuth-Yao die model with $p=0.4$.\label{fig:unfair-drn}}
 \end{figure}
 
-\begin{figure}
-	\centering
-	\begin{tikzpicture}[->,>=stealth,scale=0.9,every node/.style={scale=0.9,transform shape}, node distance=2cm]
-		\node[state,initial,initial text={}] (s0) {$s_0$};
-
-		\node[state,above right=of s0] (s1) {$s_1$};
-		\draw (s0) -- node[above left] {$0.4 + v_{0,1}$} ++ (s1);
-		\node[state,above right=of s1] (s3) {$s_3$};
-		\draw (s1) -- node[below right] {$0.4 + v_{1,3}$} ++ (s3);
-		\draw (s3) edge[bend right=45] node[above left] {$0.4 + v_{3,1}$} (s1);
-		\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
-		\draw (s3) -- node[above] {$0.6 + v_{3,7}$} ++ (s7);
-		\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
-		\draw (s1) -- node[below,xshift=-.5em] {$0.6 + v_{1,4}$} ++ (s4);
-		\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
-		\draw (s4) -- node[above] {$0.4 + v_{4,8}$} ++ (s8);
-		\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
-		\draw (s4) -- node[below] {$0.6 + v_{4,9}$} ++ (s9);
-
-		\node[state,below right=of s0] (s2) {$s_2$};
-		\draw (s0) -- node[below left] {$0.6 + v_{0,2}$} ++ (s2);
-		\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
-		\draw (s2) -- node[above,xshift=-.5em] {$0.6 + v_{2,5}$} ++ (s5);
-		\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
-		\draw (s5) -- node[above] {$0.4 + v_{5,10}$} ++ (s10);
-		\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
-		\draw (s5) -- node[below] {$0.6 + v_{5,11}$} ++ (s11);
-		\node[state,below right=of s2] (s6) {$s_6$};
-		\draw (s2) -- node[above right] {$0.4 + v_{2,6}$} ++ (s6);
-		\draw (s6) edge[bend left=45] node[below left] {$0.4 + v_{6,2}$} (s2);
-		\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
-		\draw (s6) -- node[above] {$0.6 + v_{6,12}$} ++ (s12);
-	\end{tikzpicture}
-	\caption{An unfair instance of the Knuth-Yao die model with fresh variables.\label{fig:var-unfair-die}}
-\end{figure}
-
 \begin{enumerate}
 	\item
 		The \PRISM\ program is read and parsed by stormpy.
@@ -96,3 +60,39 @@ The Model Repair procedure for a \PRISM\ program and a property $\phi$ consists
 		The generated Z3 model is returned to the user.
 		It contains the instantiations of the variables $v_{s,s'}$, with which $\mathcal M$ can be adapted to satisfy $\phi$.
 \end{enumerate}
+
+\begin{figure}
+	\centering
+	\begin{tikzpicture}[->,>=stealth,scale=0.9,every node/.style={scale=0.9,transform shape}, node distance=2cm]
+		\node[state,initial,initial text={}] (s0) {$s_0$};
+
+		\node[state,above right=of s0] (s1) {$s_1$};
+		\draw (s0) -- node[above left] {$0.4 + v_{0,1}$} ++ (s1);
+		\node[state,above right=of s1] (s3) {$s_3$};
+		\draw (s1) -- node[below right] {$0.4 + v_{1,3}$} ++ (s3);
+		\draw (s3) edge[bend right=45] node[above left] {$0.4 + v_{3,1}$} (s1);
+		\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
+		\draw (s3) -- node[above] {$0.6 + v_{3,7}$} ++ (s7);
+		\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
+		\draw (s1) -- node[below,xshift=-.5em] {$0.6 + v_{1,4}$} ++ (s4);
+		\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
+		\draw (s4) -- node[above] {$0.4 + v_{4,8}$} ++ (s8);
+		\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
+		\draw (s4) -- node[below] {$0.6 + v_{4,9}$} ++ (s9);
+
+		\node[state,below right=of s0] (s2) {$s_2$};
+		\draw (s0) -- node[below left] {$0.6 + v_{0,2}$} ++ (s2);
+		\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
+		\draw (s2) -- node[above,xshift=-.5em] {$0.6 + v_{2,5}$} ++ (s5);
+		\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
+		\draw (s5) -- node[above] {$0.4 + v_{5,10}$} ++ (s10);
+		\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
+		\draw (s5) -- node[below] {$0.6 + v_{5,11}$} ++ (s11);
+		\node[state,below right=of s2] (s6) {$s_6$};
+		\draw (s2) -- node[above right] {$0.4 + v_{2,6}$} ++ (s6);
+		\draw (s6) edge[bend left=45] node[below left] {$0.4 + v_{6,2}$} (s2);
+		\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
+		\draw (s6) -- node[above] {$0.6 + v_{6,12}$} ++ (s12);
+	\end{tikzpicture}
+	\caption{An unfair instance of the Knuth-Yao die model with fresh variables.\label{fig:var-unfair-die}}
+\end{figure}