\section{Discussion}
Our tool is fully capable of dealing with parameterized DRN files.
The parameters of the model are then added as constants to the Z3 model, and model repair proceeds as usually.
However, unfortunately, it turned out that Storm is not able to output (or parse) parameterized DRN files%
	\footnote{Since the DRN files contain a \texttt{@parameters} key, it was a reasonable assumption that this key would be considered in at least one direction.}.
Therefore, this was not tested extensively.
For the same reason, we have not been able to extend our approach to MDPs.

Another drawback of the lack of parameterization is that properties have to be specified on the generated DTMC rather than on the \PRISM\ program itself.
This means one must have a look at the generated DRN file when writing properties.
For each property that should be satisfied, we need to pass an assertion to Z3.
However, this assertion depends on the parameterized DTMC after state elimination, which lives in a Clean data structure.
Since Storm is not able to parse such a DTMC, we cannot let Storm parse properties and generate the Z3 assertions for us.
Implementing this in Clean for all kinds of properties was beyond the scope of this project.
Currently, we only support formulas of the forms $\mathbb P_{< p}s$, $\mathbb P_{= p}s$ and $\mathbb P_{> p}s$, where $s$ is a state in the DTMC.
However, are tool \emph{can} satisfies conjunctions of these formulas.

Because we could not let Storm generate the Z3 assertions, we also had to implement a function to convert prefix notation (of the probabilities in the DRN files) to infix notation (of Z3's default SMT2 format).
This is done in Clean.

Z3 is well able to repair the unfair Knuth-Yao die of \cref{fig:var-unfair-die}, when it is not given a minimization goal.
As rules, we set $\mathbb P_{> 0.166666666}s_i$ for $i\in\{7,8,9,10,11,12\}$.
The result approximates the Knuth-Yao die with $p=0.5$, as expected, within a negligible amount of time.
Unfortunately, adding a minimization goal increases the complexity drastically.
The NMT measure is in principle decidable, but takes too long (over 10 minutes on the unfair die example).
The SSE measure is not decidable, and Z3 is not able to solve the system.
However, the cost can be approximated by adding an upper bound on the cost as a Z3 assertion.
When a satisfying model is found, the cost of that model can be used as a new upper bound.
This can be repeated until the model cannot be satisfied.