diff options
Diffstat (limited to 'Assignment2/report')
| -rw-r--r-- | Assignment2/report/implementation.tex | 72 |
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} |