Lalala

1 files changed, 10 insertions, 1 deletions

diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex
index c9a94f7..48e9328 100644
--- a/Assignment2/report/assignment2.tex
+++ b/Assignment2/report/assignment2.tex
@@ -29,13 +29,22 @@
 \maketitle
 
 \begin{abstract}
-	Model repair bladibla % TODO
+	We discuss an approach to the repair of parametric models using an SMT solver.
+	To repair a model $\mathcal M$ which does not satisfy a probabilistic CTL formula $\phi$,
+		we add an additional parameter to the probability of each transition in $\mathcal M$,
+		after which we eliminate all non-initial non-absorbing states.
+	The SMT solver gets constraints to ensure that the repaired model remains valid
+		and to satisfy $\phi$.
+	Cost functions for the model repair problem can be formulated as a minimisation goal for the SMT solver.
+	Unfortunately, some technical issues prevent us from using the tool in practice.
+	We provide pointers to future work to resolve these issues.
 \end{abstract}
 
 \input{intro}
 \input{method}
 \input{implementation}
 \input{discussion}
+\input{future}
 
 \bibliography{library}
 \bibliographystyle{splncs04}