From a7cea2181b5cb75e2ff62ad5a80c9532880e5346 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 6 Jul 2018 21:37:11 +0200
Subject: Lalala

---
 Assignment2/report/assignment2.tex | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'Assignment2/report/assignment2.tex')

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}
-- 
cgit v1.2.3