moves-rwth / storm

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

Move From Nondeterministic to Deterministic Model #69

Open sjunges opened 4 years ago

sjunges commented 4 years ago

What is the right way to force an MDP to being a DTMC, without much overhead? That is, if I have an MDP (e.g., after applyScheduler with a full scheduler) and I want to get an DTMC, how do I make the resulting MDP a DTMC? Is there any code doing that already?

This is related to https://github.com/moves-rwth/storm/issues/63 and https://github.com/moves-rwth/stormpy/issues/14

tquatmann commented 4 years ago

AFAIK there currently is a getter for each model component, that retrieves it by (non-const) reference. It should be possible to do std::make_shared<DTMC<VT>>(std::move(mdp.getTransitionMatrix()), std::move(mdp.getStateLabeling()), std::move(mdp.getRewardModels); (this disregards other components like choice labels)

Another more elegant way could be to write the inverse of this guy. Then you could

I'm not sure, but you might also need SparseMatrix.makeRowGroupingTrivial()