Add text about PRISM repair

1 files changed, 9 insertions, 0 deletions

diff --git a/Assignment2/report/future.tex b/Assignment2/report/future.tex
index 5adb602..4bdc071 100644
--- a/Assignment2/report/future.tex
+++ b/Assignment2/report/future.tex
@@ -7,3 +7,12 @@ Either of these options seem to be possible straightforwardly given more knowled
 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.