\section{Future Work}
To get this tool to a usable state,
	either Storm needs to be able to read and write parametric DTMCs to DRN files,
	or the logic of our tool needs to be re-implemented in Python or C(++) on Storm's data structures.
Either of these options seem to be possible straightforwardly given more knowledge or documentation of Storm.

To implement the cost functions properly, there are different options.
The simplest would be implementing the approximation method described in the previous section.
Another option is to find different kinds of cost functions which can be minimised efficiently.

The present implementation works on DTMCs directly.
It would be more useful to be able to perform model repair on \PRISM\ files directly.
A straightforward way to work on \PRISM\ files directly would be to add parameters on the transitions in the \PRISM\ file rather than in the DRN file.
Then the instantiations found by Z3 can be used directly to modify the transition probabilities in the \PRISM\ program.

This does not resolve all faults, because one transition in a \PRISM\ program may describe several transitions in the DTMC.
To fix such transitions independent from each other, one could add annotations to the DRN format to be able to reconstruct the \PRISM\ program.
Then the DRN can be fixed with the solution found by Z3, and the \PRISM\ program can be reconstructed from there.