search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
132 stars 74 forks source link

Is there anyway to create an Exact sparse mdp model ? #331

Closed oyendrila-dobe closed 1 year ago

oyendrila-dobe commented 1 year ago

This has been previously discussed in this stormpy issue. I'm however, unable to locate the corresponding c++ method for exact sparse matrix builder. Is there any existing method that generates the model from PRISM files saving the transitions as Rational numbers? If not, can you point me to the c++ method that can be used to create such a matrix manually?

volkm commented 1 year ago

All functions in storm are templated and you can provide the number type you want to use as a template argument. See for example this test which works with exact (rational) numbers.

You can create a DTMC with rational numbers from a Prism file as follows:

std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc =
        storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
auto matrix = dtmc.getTransitionMatrix();
oyendrila-dobe commented 1 year ago

Thanks, Matthias. That was really helpful.