Translate PTA model to MDP?

[rpgoldman]

Looking at the code, it looks like there's a facility for translating PTA models into MDPs, by making the timed quotient, but I can't figure out how to use it, or even if it is used in the current version of PRISM, or if it's old code just not removed.

There are buildMDP methods in BackwardsReachabilityGraph.java and ForwardsReachabilityGraph.java, but the only call I can find is in PTAModelCheckerCL.java, and uses only the forward reachability graph method.

I'm asking because I would like to use buildMDP to try solving a PTA with an MDP solving algorithm (a PRISM add-on in the works).