Problem with running PRISM

[Mohammad Abdulaziz]

Hi Everyone,

I am trying to check the attached model (which has 59049 states) using PRISM, and, unfortunately, it is taking a very long time (2952.987 secs on my machine) using the explicit engine to build the model. It also cannot check the specification in simple.pctl in 4 hours. I also tried running PRISM in the sparse and the hybrid modes, and it does not even finish building the model in 4 hours. I am wondering if I am making some mistake in configuring PRISM as the PRISM manual page states the explicit engine can handle one tenth of what the hybrid engine can handle, which is 10e7-10e8 states. I run PRISM with the following options:

prism --nopre --{explicit|sparse} --javamaxmem 4g --cuddmaxmem 4g --valiter --epsilon 0.05  simple.nm simple.pctl

Is there a configuration which would be capable of handling this model more efficiently?

best,

Mohammad

[Dave Parker]

Hi Mohammad,

The problem here is the sheer size of the model file. Parsing and model
construction from that is very slow for any engine.

Seeing as the model is (presumably!) automatically generated, and very
simple in structure (one module, one variable), it would be better to
generate "explicit" files that list all the models states/transitions
instead, and import them. See here:

https://prismmodelchecker.org/manual/RunningPRISM/ExplicitModelImport

and here for the file formats:

https://prismmodelchecker.org/manual/Appendices/ExplicitModelFiles

This is still not as efficient as a normal, structured model in the
PRISM modelling language. But if this is the format of your model, then
this should be faster than what you were doing.

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 view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/8c07bda8-5fe7-43d8-a587-192a26f9f200n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/8c07bda8-5fe7-43d8-a587-192a26f9f200n%40googlegroups.com?utm_medium=email&utm_source=footer>.