PRISM cannot generate model using sparse engine

[Javier Cámara]

Hi,

I am having some problems with the generation of a small MDP model (approx. 50 states) with the sparse engine in PRISM 4.2.1. When I use the explicit engine, it works without any problems, but with the sparse engine, the tool cannot finish the construction of the model. Any idea of what might be going on?

I need the sparse engine because I need to generate an adversary for the MDP, and if I am not mistaken, this is the only engine that supports this functionality.

Thanks,
Javier

[Dave Parker]

Hi Javier,

The most common scenario where the explicit engine is much faster than
the others is when the model has a potentially very large state space,
only a small fraction of which is reachable from the initial state.
Perhaps this is the cause for you.

Regarding adversary/strategy export, the explicit engine does have some
support for this, but some parts are still work in progress. For the
cases that do work, you should be able to use the -exportadv which
normally works for the sparse engine. If this is not working, can you
tell me which class of property you are using? Perhaps the code is
already implemented for the adversary export but not in the public
release yet.

Another possible work around is to generate the model with the explicit
engine, export it, and then re-import it using the sparse engine.

http://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel
http://www.prismmodelchecker.org/manual/RunningPRISM/ExplicitModelImport

This is not perfect, for example reward export/import is not yet done,
but may be another option.

Best wishes,

Dave.

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Javier Cámara]

Hi Dave,

thanks for the information. I have tried to generate the adversary using the explicit engine, and it seems to be working correctly. PRISM is not including the labels of the actions in the file it exports in this case (action labels were available when I tried exporting the adversary using the sparse engine with other examples), but I can easily look them up by exporting the transitions of the model to another file.

The type of property for which I am generating the adversary is a reachability reward maximization.

Javier

> <mailto:prismmodelchecker+unsub...@googlegroups.com>.

[Dave Parker]

Good to hear, Javier.

Actually, I just added support for including actions when exporting
adversaries using the explicit engine.

Currently, it's just in the very latest version of the code, in our
subversion repository:

http://www.prismmodelchecker.org/wiki/Developers/UsingSubversion

Best wishes,

Dave.

> <http://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel>
>
> http://www.prismmodelchecker.org/manual/RunningPRISM/ExplicitModelImport

> > an email to prismmodelchec...@googlegroups.com <javascript:>
> > <mailto:prismmodelchec...@googlegroups.com
> <javascript:>>.

> > To post to this group, send email to prismmod...@googlegroups.com

> <javascript:>
> > <mailto:prismmod...@googlegroups.com <javascript:>>.

> > Visit this group at
> http://groups.google.com/group/prismmodelchecker

> <http://groups.google.com/group/prismmodelchecker>.

> > For more options, visit https://groups.google.com/d/optout

> <https://groups.google.com/d/optout>.

>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com

> <mailto:prismmodelchec...@googlegroups.com>.

[Javier Cámara]

Great! Thanks for letting me know, Dave.

Regards,
Javier

>     > <mailto:prismmodelchecker+unsub...@googlegroups.com

>     <javascript:>>.
>     > To post to this group, send email to prismmod...@googlegroups.com
>     <javascript:>
>     > <mailto:prismmod...@googlegroups.com <javascript:>>.
>     > Visit this group at
>     http://groups.google.com/group/prismmodelchecker
>     <http://groups.google.com/group/prismmodelchecker>.
>     > For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com

> <mailto:prismmodelchecker+unsub...@googlegroups.com>.