diff options
Diffstat (limited to 'Assignment2/report/discussion.tex')
| -rw-r--r-- | Assignment2/report/discussion.tex | 15 |
1 files changed, 15 insertions, 0 deletions
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. |