\section{Implementation}
In this section we will look at the individual steps as described in the Methods section.
As an example, we will look at the unfair Knuth-Yao die model in \cref{fig:unfair-die}.
\begin{figure}
	\centering
	\begin{tikzpicture}[->,>=stealth,scale=0.9,every node/.style={scale=0.9,transform shape}]
		\node[state,initial,initial text={}] (s0) {$s_0$};

		\node[state,above right=of s0] (s1) {$s_1$};
		\draw (s0) -- node[above left] {$0.4$} ++ (s1);
		\node[state,above right=of s1] (s3) {$s_3$};
		\draw (s1) -- node[below right] {$0.4$} ++ (s3);
		\draw (s3) edge[bend right=45] node[above left] {$0.4$} (s1);
		\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
		\draw (s3) -- node[above] {$0.6$} ++ (s7);
		\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
		\draw (s1) -- node[below,xshift=-.5em] {$0.6$} ++ (s4);
		\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
		\draw (s4) -- node[above] {$0.4$} ++ (s8);
		\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
		\draw (s4) -- node[below] {$0.6$} ++ (s9);

		\node[state,below right=of s0] (s2) {$s_2$};
		\draw (s0) -- node[below left] {$0.6$} ++ (s2);
		\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
		\draw (s2) -- node[above,xshift=-.5em] {$0.6$} ++ (s5);
		\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
		\draw (s5) -- node[above] {$0.4$} ++ (s10);
		\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
		\draw (s5) -- node[below] {$0.6$} ++ (s11);
		\node[state,below right=of s2] (s6) {$s_6$};
		\draw (s2) -- node[above right] {$0.4$} ++ (s6);
		\draw (s6) edge[bend left=45] node[below left] {$0.4$} (s2);
		\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
		\draw (s6) -- node[above] {$0.6$} ++ (s12);
	\end{tikzpicture}
	\caption{An unfair instance of the Knuth-Yao die model~\cite{KnuthYao1976}.\label{fig:unfair-die}}
\end{figure}

\subsection{The \PRISM\ program is read and parsed by stormpy}
Stormpy reads the \PRISM\ program an converts it to its internal DTMC representation.

\subsection{The DTMC is exported in DRN format using stormpy}
In order to parse our model in Clean, stormpy outputs its internal representation to a DRN file.
The resulting DRN file looks like as shown in~\cref{fig:unfair-drn}.
\begin{figure}
	\begin{minted}{text}
	// Exported by storm
	// Original model type: DTMC
	@type: DTMC
	@parameters
	@reward_models
	@nr_states
	13
	@model
	state 0 init
		action 0
			1 : 0.4
			2 : 0.6
	...
	state 6
		action 0
			2 : 0.4
			12 : 0.6
	state 7
		action 0
			7 : 1
	...
	state 12
		action 0
			12 : 1
	\end{minted}
	\caption{The DRN file representing the unfair Knuth-Yao die model.\label{fig:unfair-drn}}
\end{figure}

\subsection{The DRN format is parsed in a Clean}
A parser for DRN files was written for Clean.
This parser parses the DRN file into an internal presentation.
Note that, in state elimination, transitions are used in whole.
This meant that the internals of the formulas are not of concern.
For this reason, we chose to store the formulas as their string representation.

\subsection{Parameters are added to the transitions}
Given the Clean Datastructure, which makes use of uniqueness to improve performance, a simple algorithm was created to give every transition an additional fresh variable.
The resulting model is shown in \cref{fig:var-unfair-die}.
\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 + v0\_1$} ++ (s1);
		\node[state,above right=of s1] (s3) {$s_3$};
		\draw (s1) -- node[below right] {$0.4 + v0\_3$} ++ (s3);
		\draw (s3) edge[bend right=45] node[above left] {$0.4 + v3\_1$} (s1);
		\node[state,right=of s3,label={right:\enquote{1}}] (s7) {$s_7$};
		\draw (s3) -- node[above] {$0.6 + v3\_7$} ++ (s7);
		\node[state,below right=of s1,yshift=3em] (s4) {$s_4$};
		\draw (s1) -- node[below,xshift=-.5em] {$0.6 + v1\_4$} ++ (s4);
		\node[state,right=of s4,yshift=2.7em,label={right:\enquote{2}}] (s8) {$s_8$};
		\draw (s4) -- node[above] {$0.4 + v4\_8$} ++ (s8);
		\node[state,right=of s4,yshift=-1em,label={right:\enquote{3}}] (s9) {$s_9$};
		\draw (s4) -- node[below] {$0.6 + v4\_9$} ++ (s9);

		\node[state,below right=of s0] (s2) {$s_2$};
		\draw (s0) -- node[below left] {$0.6 + v0\_2$} ++ (s2);
		\node[state,above right=of s2,yshift=-3em] (s5) {$s_5$};
		\draw (s2) -- node[above,xshift=-.5em] {$0.6 + v2\_5$} ++ (s5);
		\node[state,right=of s5,yshift=1em,label={right:\enquote{4}}] (s10) {$s_{10}$};
		\draw (s5) -- node[above] {$0.4 + v5\_10$} ++ (s10);
		\node[state,right=of s5,yshift=-2.7em,label={right:\enquote{5}}] (s11) {$s_{11}$};
		\draw (s5) -- node[below] {$0.6 + v5\_11$} ++ (s11);
		\node[state,below right=of s2] (s6) {$s_6$};
		\draw (s2) -- node[above right] {$0.4 + v2\_6$} ++ (s6);
		\draw (s6) edge[bend left=45] node[below left] {$0.4 + v6\_2$} (s2);
		\node[state,right=of s6,label={right:\enquote{6}}] (s12) {$s_{12}$};
		\draw (s6) -- node[above] {$0.6 + v6\_12$} ++ (s12);
	\end{tikzpicture}
	\caption{An unfair instance of the Knuth-Yao die model with fresh variables~\cite{KnuthYao1976}.\label{fig:var-unfair-die}}
\end{figure}

\subsection{State elimination is performed in Clean}
%TODO: Camil, please write this section

\subsection{The DRN format is exported by Clean}
In order to convert our internal representation back to a DRN file, a Clean function was created: \mintinline{Clean}|printDTMC :: !*DTMC -> *(!String, !*DTMC)|.
This step is performed to pass our model back to stormpy.
We want to do this, to allow us to easily create Z3 formulas.

\subsection{The formulas are passed to z3 with additional constraints by stormpy}
The transition labels are passed to z3.
Additionally, we ensure that the sum of all outgoing transitions of a state equals 1.
Furthermore, z3 is required to minimize the sum of all fresh variables introduced in step 4.

The last assertion that is passed to z3 is, of course, the goal.
In our case, we want that eventually reaching an absorbing state is $\frac{1}{6}$.

%TODO: Describe resulting model
