blob: 692870199d5ee61f3fe855fc9204394b89584bc3 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
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.
\paragraph{Our tool}
There are many thing that were not implemented in the tool described in this paper, either because of a time constraint, or constraints in the tools that were used.
Our tool fully capable of dealing with parameterized DRN files, we can fully parse and output them.
Due to limitations with storm however, this was not extensively tested.
Right now, the interface to z3 that was created for our tool is very na\"ively implemented.
Ideally, we would like to create a python-like api to z3.
This does not mean that our interface is less powerful, in fact, we provide a reasonable subset of smt2 that can easily be extended to provide full support.
|
