Initial discussion of encountered problems

2 files changed, 16 insertions, 0 deletions

diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex
index 4e0424b..c9a94f7 100644
--- a/Assignment2/report/assignment2.tex
+++ b/Assignment2/report/assignment2.tex
@@ -35,6 +35,7 @@
 \input{intro}
 \input{method}
 \input{implementation}
+\input{discussion}
 
 \bibliography{library}
 \bibliographystyle{splncs04}
diff --git a/Assignment2/report/discussion.tex b/Assignment2/report/discussion.tex
new file mode 100644
index 0000000..24e0003
--- /dev/null
+++ b/Assignment2/report/discussion.tex
@@ -0,0 +1,15 @@
+zsection{Discussion}
+There were many things that we encountered during the creation of this tool.
+This section serves to provide an overview of these things.
+
+\paragraph{Storm}
+Our initial plan was to use stormpy for the conversion of the transition formulas to smt2.
+We would do this by creating exporting the model as DRN, and then parse this model using storm.
+The DRN files that storm outputs suggest that it is capable parsing DRN files of parameterized DTMCs~\footnote{The output file contains the @parameters keyword}.
+Unfortunately, we quickly realized that this is not the case.
+To overcome this problem we had to implement a formula parser and create a function that could convert infix notation to the prefix notation that is used in smt2.
+
+\paragraph{z3}
+We encountered slight performance issues with z3.
+When we include the cost-function (as described earlier in this paper) z3 is no longer able to create a model within reasonable time~\footnote{Where reasonable time is less than 5 seconds}.
+We tried to work around this issue by limiting the domain the of Real numbers to the integers \texttt{[0 .. 1000]}, but this had no effect.