Improve text on PRISM programsHEADmaster

1 files changed, 5 insertions, 4 deletions

diff --git a/Assignment2/report/future.tex b/Assignment2/report/future.tex
index 4bdc071..c0a5a8b 100644
--- a/Assignment2/report/future.tex
+++ b/Assignment2/report/future.tex
@@ -10,9 +10,10 @@ Another option is to find different kinds of cost functions which can be minimis
 
 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.
+A straightforward way to do this would be to add parameters on the transitions in the \PRISM\ file rather than in the DRN file%
+	\footnote{This is impossible in the current setup, as Storm cannot generate parameterized DRN files. However, this is no insurmountable problem.}.
 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.
+Note however that this method would 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 original \PRISM\ program,
+	similar to debugging symbols added by a compiler to allow for disassembly.
 Then the DRN can be fixed with the solution found by Z3, and the \PRISM\ program can be reconstructed from there.