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..
> --
> 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>.