Build DTMC from MDP

[Leonardo Zecchin]

Hi, I'm trying to model check based on a DTMC generated by a series of choices taken on an MDP, but I'm not sure what's the best solution for this problem. I'm trying to export a custom DTMC that implements the ModelGenerator interfaces that stores states, transitions and probabilities from a choice made on the MDP to then model check it but I'm struggling. Thank you in advance.

[Dave Parker]

Hi Leonardo,

How is the MDP defined? If you have already built it in PRISM, and are
using the explicit engine, you should be able to get access to the MDP
object and then use classes such as DTMCFromMDPAndMDStrategy to create a
DTMC without the overhead of defining a model generator and building a
new model. If you can give some more information about how your code
works, I can advise further.

Best wishes,

Dave