Using MTBDD Engine with ModelGenerator

[Edoardo]

Hello,

I've been working on an extension to PRISM where an MDP is passed programmatically to PRISM using the ModelGenerator interface (which I believe was recently introduced in version 4.4). This works well with the Explicit engine, but if I set the engine to the MTBDD one, I get a different result (I'm checking a Pmax=? property, and the result is completely different, not just within some rounding error).

I've added a prism.initialise() call, which is needed to initialise CUDD and avoid errors. Apart from this, is there anything else I should be doing differently in order to use the MTBDD engine rather than the Explicit one? Does anyone have any example code using the ModelGenerator interface together with the MTBDD engine that I could have a look at?

I'm happy to share code individually if someone would like to have a look, but would rather not share it publically since it involves ongoing unpublished work.

Thanks for your help!

Best,

Edoardo

P.S. I've seen in the ModelGenerator2MTBDD class that there's a hardcoded maximum number of choices of action in each state of 32, this isn't an issue here as the MDP I'm checking has much fewer actions than this.

[Edoardo]

After a bit of debugging, I've managed to find the issue. My ModelGenerator was using unbounded integer variables, which are not supported by the MTBDD engine.

It would be nice if the ModelGenerator2MTBDD class checked for this, as the Modules2MTBDD one already does. I've submitted a pull request for this here:

https://github.com/prismmodelchecker/prism/pull/89

[Dave Parker]

Excellent. Many thanks for this Edoardo. I'll look at the PR. Glad it is
working well for you.

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
> To post to this group, send email to
> prismmodel...@googlegroups.com
> <mailto:prismmodel...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/prismmodelchecker-dev.