blob: 24e0003dcd24dadef21a7e319cdd0122a320cd23 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.
|
