Does PRISM's Java API support statistical model checking?

[Raquel Sánchez Salas]

Hi,

I know that PRISM's Java API allows us to perform probabilistic model checking, but I was wondering if it's also possible to perform statistical model checking using the same API?

Is there a way to run simulations and gather statistical results programmatically through the API, or would this require invoking PRISM's command-line interface (CLI) for statistical model checking?

Thanks in advance for any clarification.  

[Dave Parker]

Hi Raquel,

Yes, this is possible. At a high-level you can switch from probabilistic
model checking to statistical model checking by using the
Prism.modelCheckSimulator() method instead of the Prism.modelCheck()
method. If you want some information about how this is configured (e.g.
the SimulationMethod object), you can have a look at how this is done in
PrismCL.java (see method processSimulationOptions(), for example).

You can get more fine-grained control via the SimulatorEngine object.
This example from the PRISM API repo shows the basics:

https://github.com/prismmodelchecker/prism-api/blob/master/src/demos/SimulateModel.java

Please feel free to ask for further details.

Best wishes,

Dave

> Hi,
>
> I know that PRISM's Java API allows us to perform probabilistic model
> checking, but I was wondering if it's also possible to perform

> *statistical model checking* using the same API?

>
> Is there a way to run simulations and gather statistical results
> programmatically through the API, or would this require invoking PRISM's
> command-line interface (CLI) for statistical model checking?
>
> Thanks in advance for any clarification.
>

> --
> 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 view this discussion on the web, visit https://groups.google.com/d/
> msgid/prismmodelchecker/a682322b-1120-4257-a928-
> e985cc3e1f3en%40googlegroups.com <https://groups.google.com/d/msgid/
> prismmodelchecker/a682322b-1120-4257-a928-
> e985cc3e1f3en%40googlegroups.com?utm_medium=email&utm_source=footer>.