diff options
| author | Erin van der Veen | 2018-07-06 16:48:48 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 16:48:48 +0200 |
| commit | 817fe8af61f565e87780538ba1ebbfac8c4da0ef (patch) | |
| tree | 398a553d1b8f138cb4cb96a878544d5b5e41fa4b /Assignment2 | |
| parent | Initial discussion of encountered problems (diff) | |
Shortcommings of our own tool
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/report/discussion.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Assignment2/report/discussion.tex b/Assignment2/report/discussion.tex index 24e0003..6928701 100644 --- a/Assignment2/report/discussion.tex +++ b/Assignment2/report/discussion.tex @@ -13,3 +13,12 @@ To overcome this problem we had to implement a formula parser and create a funct 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. |