Status of CTMDP support

[pranavashok]

Hi @davexparker @kleinj , I wanted to know if there are any plans to make CTMDP support mainstream. I can see a CTMDPModelChecker with bounded reachability implemented, but I couldn't find a way to invoke this through the CLI/GUI. The parser doesn't seem to support files starting with ctmdp either. Is there some hidden way in which one can input CTMDPs and do stuff on it? As far as I understand, CTMDP class extends MDPSimple and distributions store the rates instead (correct me if I'm wrong). It doesn't seem too hard to somehow write a CTMDP model file like one writes a MDP model file and parse it. Is it worth the effort to go this way?

[davexparker]

Hi. This functionality is not really complete. From memory, the basic probability computation methods in CTMDPModelChecker work ok, but there is no attempt to connect them to PRISM language models. The latter would actually be pretty trivial if you just allow the ctmdp keyword as a model type and then take the existing notation for MDP models, but allow probabilities to be rates instead. If that was the preferred specification, then changing explicit.ConstructModel to support CTMDPs would be very straightforward (using MDPSimple or a simple subclass of it).

So, if you want to do some coding or try new algorithms with CTMDPs, this would be a fairly easy way to get a nice front-end for it. On the other hand, if you just want a way of solving some CTMDP models you already have, I suspect you'd find that the methods implemented in CTMDPModelChecker are not very efficient. I lost track, but I believe people came up with more efficient numerical solution/model checking algorithms since then.

[pranavashok]

Hi Dave, thanks for the reply.

The latter would actually be pretty trivial if you just allow the ctmdp keyword as a model type and then take the existing notation for MDP models, but allow probabilities to be rates instead. If that was the preferred specification, then changing explicit.ConstructModel to support CTMDPs would be very straightforward (using MDPSimple or a simple subclass of it).

I think I'll do this.

So, if you want to do some coding or try new algorithms with CTMDPs, this would be a fairly easy way to get a nice front-end for it.

Yes, this is what I needed.

[davexparker]

OK, great. Take a look and please just ask if you have questions.

[pranavashok]

@davexparker It was just a matter of adding two lines in PrismParser.jj. I was able to check a bounded until property on a CTMDP without doing anything else. Rest of the infrastructure was already present. :-)

[nihsel]

@pranavashok Hello, I am also trying to enable CTMDP in PRISM. Could you please share with me the modifications that you did in order to achieve that?
Thank you in advance!

[pranavashok]

Hi @nihsel, really sorry for not noticing your question earlier. This comment is probably not useful for you now, but maybe for others who stumble upon this issue in the future. The following changes in src/parser/PrismParser.jj should allow you to start working with CTMDPs.

1. Add | < CTMDP: "ctmdp" > under the line | < CTMC: "ctmc" >
2. Add | <CTMDP> { modelType=ModelType.CTMDP; } under the line | (<CTMC>|<STOCHASTIC>) { modelType=ModelType.CTMC; }

[nihsel]

hi @pranavashok,
I ended up figuring out what to do back in 2018, but regardless thank you very much for the reply!

[pazhamalai]

Hi. I recently wanted to add the CTMDP support in PRISM. This discussion is very helpful in solving the matter quickly. I wanted to add one more observation, it might help for future readers.

After modifying the code in PrismParser.jj, we need to re-generate the PrismParser.java file with JavaCC tool, using the same version as used in the Prism. I Installed JavaCC version 5.0, which is the default version in Ubuntu repositories. But PRISM uses version 6. Because of this inconsistency in version, I couldn't run the PRISM library. Issue got resolved, when I again re-generated PrismParser.java with JavaCC version 6.

[davexparker]

Thanks for flagging this @pazhamalai. I added a note to our developer resources here: https://github.com/prismmodelchecker/prism/wiki