Unable to change CUDD max memory

[Kiyomi Flash]

Dear PRISM Development Team,

I am currently working on a project that utilizes PRISM for probabilistic model checking of a multi-robot fleet rescue mission. 

As my model has grown in complexity, I've been facing the state explosion problem. While trying various ways to optimize and work around this issue, I encountered an unexpected error that I believe might be a bug.

Here's a summary of the situation:

I am running PRISM version 4.7 on a Windows 11 22H2 system. The JRE version is 20.0.1 build 9. The hardware detail of my device is intel 12700h with 64GB of RAM.

The model building can run successfully when the cuddmaxmem is set as 1g (which is the default value) or 512m. There are only about 20000 states in my model so memory should not be a problem. 

When attempting to increase the CUDD max memory setting in PRISM to 2g or 3g (using the -cuddmaxmem flag), PRISM crashes with an EXCEPTION_ACCESS_VIOLATION error. I have also changed the "xmx" parameter of JVM but it does not help. 

When attempting to incerase the CUDD max memory setting to 4g or above, another error occurs, this time it saids CUDD is out of memory.

The crashes seems to originate outside the Java Virtual Machine in native code, with a problematic frame identified in msvcrt.dll. However, I'm not an expert in computer system, and I am don't have enough time to dig deeper into this problem since this is just a part of my master's dissertation.

I've attached the relevant logs and screenshots of error messages for your reference. 

I understand that everyone is busy, but I would greatly appreciate any prompt feedback or suggestions you can offer. If further details or clarifications are needed, please do not hesitate to ask.

Thank you in advance for your time and assistance. I deeply value the work you've done with PRISM, and I hope we can find a solution to this problem.

1gmaxmem:

2gmaxmem:

4gmaxmem:

Best regards,

Chuyan

2811...@student.gla.ac.uk

University of Glasgow, School of Computing Science

[Dave Parker]

Dear Kiyomi,

The log you sent does suggest that the crash is indeed caused when CUDD
is initialised, perhaps because there is not enough memory available. I
see you have also set the Java memory very high too (-Xmx50g). You
typically don't need to do both, because they provide memory for
different engines' needs (-cuddmaxmem for the symbolic engines, and Java
memory for the explicit engine). So, if you need the CUDD memory to be
higher, I suggest you try reducing the Java memory when you do so.

Best wishes,

Dave

> 1gmaxmem.png
>
> 2gmaxmem:
> 2gmaxmem.png
>
> 4gmaxmem:

> 4gmaxmem.png
>
> Best regards,
> Chuyan
>
> 2811...@student.gla.ac.uk
> University of Glasgow, School of Computing Science
>

> --
> 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/fa1f0383-8a03-4e2e-86c1-e62394b809c2n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/fa1f0383-8a03-4e2e-86c1-e62394b809c2n%40googlegroups.com?utm_medium=email&utm_source=footer>.