Max number of text lines in PRISM model?

[Mridu Nanda]

Hi,

I have been having trouble with verifying properties on large models. Large, in this case, refers to the number of lines in the .prism file, not the number of states. 

For example when I have a model of ~7000 lines, I get a log output that looks like:

Type:        MDP
States:      4620 (330 initial)
Transitions: Infinity
Choices:     Infinity

Transition matrix: 158560 nodes (2 terminal), Infinity minterms, vars: 63r/63c/995nd

...

Building sparse matrix (transitions)...
Error: Out of memory

After playing around with my code, it seems like the threshold number of lines is somewhere around 3000? Is there a way to increase the number of lines of code that a PRISM model will parse? Digging into the source code led me to this header file, which is maybe relevant? But toggling the MAXROWS const is not changing my code's behavior.. 

The original post where I encountered this problem is here: https://groups.google.com/g/prismmodelchecker/c/V_HrEmS2_ww.

I would really appreciate any help in solving this issue!

Thanks,

Mridu

[Dave Parker]

Hi Mridu,

This looks unusually inefficient. The numbers 63r/63c/995nd refer to the
number of varibles used in the symbolic (BDD-based) representation of
the model and are very large given the relatively small state space.

Firstly, depending on what type of model checking you are doing, it
could well be better to use the "explicit" model checking engine (-ex)
for such a small model. Have you tried that?

If you do need to stick with the (default) symbolic engine... The
63r/63c relate to the model variables. Do you have more variables than
you need? Or larger ranges than you need? The 995nd relates to the
number of distinct action names in your MDP, which is quite high (and
likely leading to the "infinite" size reported in your other message).
If there are actions that do not need names (e.g. for synchronisation
between modules, or for strategy export), then can you remove the names?

Best wishes,

Dave

On 18/07/2023 05:23, Mridu Nanda wrote:
> Hi,
>
> I have been having trouble with verifying properties on large models.
> Large, in this case, refers to the number of lines in the .prism file,
> not the number of states.
>
> For example when I have a model of ~7000 lines, I get a log output that
> looks like:
> Type:        MDP
> States:      4620 (330 initial)
> Transitions: Infinity
> Choices:     Infinity
>
> Transition matrix: 158560 nodes (2 terminal), Infinity minterms, vars:
> 63r/63c/995nd
>
> ...
> Building sparse matrix (transitions)...
> Error: Out of memory
>
> After playing around with my code, it seems like the threshold number of
> lines is somewhere around 3000? Is there a way to increase the number of
> lines of code that a PRISM model will parse? Digging into the source
> code led me to this

> <https://github.com/prismmodelchecker/prism/blob/8d13bee9cc64793d37093d127aaea6ab46cb9c71/prism/ext/lpsolve55/src/lp_solve_5.5/bfp/bfp_LUSOL/LUSOL/lusolmain.h#L6> header file, which is maybe relevant? But toggling the MAXROWS const is not changing my code's behavior..

>
> The original post where I encountered this problem is
> here: https://groups.google.com/g/prismmodelchecker/c/V_HrEmS2_ww.
>
> I would really appreciate any help in solving this issue!
> Thanks,
> Mridu
>
>

> --
> 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/6e59c2e2-abfb-4cd2-bcd0-3698029f4faen%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/6e59c2e2-abfb-4cd2-bcd0-3698029f4faen%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Mridu Nanda]

Hi Prof. Parker,

Thanks for your response! I will try to reduce the number of named actions to solve the Infinity transition message. I assume this will also solve the out of memory error?

However, in the meantime, is there a way to increase the upper bound on the number of named actions that I model? Via memory allocation or some other constant in the source code? Or is this engine dependent?

Thanks again for all your help!

Mridu

[Dave Parker]

There is no specific limit, just an impact on memory usage.

As mentioned, I would suggest trying the explicit engine.

Best wishes,

Dave

> <https://github.com/prismmodelchecker/prism/blob/8d13bee9cc64793d37093d127aaea6ab46cb9c71/prism/ext/lpsolve55/src/lp_solve_5.5/bfp/bfp_LUSOL/LUSOL/lusolmain.h#L6 <https://github.com/prismmodelchecker/prism/blob/8d13bee9cc64793d37093d127aaea6ab46cb9c71/prism/ext/lpsolve55/src/lp_solve_5.5/bfp/bfp_LUSOL/LUSOL/lusolmain.h#L6>> header file, which is maybe relevant? But toggling the MAXROWS const is not changing my code's behavior..

> >
> > The original post where I encountered this problem is
> > here: https://groups.google.com/g/prismmodelchecker/c/V_HrEmS2_ww

> <https://groups.google.com/g/prismmodelchecker/c/V_HrEmS2_ww>.

> >
> > I would really appreciate any help in solving this issue!
> > Thanks,
> > Mridu
> >
> >
> > --
> > 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/6e59c2e2-abfb-4cd2-bcd0-3698029f4faen%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/6e59c2e2-abfb-4cd2-bcd0-3698029f4faen%40googlegroups.com> <https://groups.google.com/d/msgid/prismmodelchecker/6e59c2e2-abfb-4cd2-bcd0-3698029f4faen%40googlegroups.com?utm_medium=email&utm_source=footer <https://groups.google.com/d/msgid/prismmodelchecker/6e59c2e2-abfb-4cd2-bcd0-3698029f4faen%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
> --
> 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/28a4e198-c69f-4fa6-a898-5c40081fce24n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/28a4e198-c69f-4fa6-a898-5c40081fce24n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Mridu Nanda]

Hi Prof. Parker,

Using the explicit engine did not resolve the issue.. now the model is stuck on the building stage. Would increasing the amount of CUDD memory help? I currently have cudd=10g, java(heap)=32g as the memory allocation on my machine. 

Thanks again,

Mridu