Move From Nondeterministic to Deterministic Model

[sjunges]

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]

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

• get the model components
• change the model type of the components
• and then execute buildModelFromComponents

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