diff options
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/report/assignment2.tex | 1 | ||||
| -rw-r--r-- | Assignment2/report/discussion.tex | 15 |
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. |