Large models

[Mridu Nanda]

I have a model with ~10^11 states and 10^11 transitions. The model took about 45 minutes to construct, and has run overnight (about 13 hours). I just got the following error message:

#

# A fatal error has been detected by the Java Runtime Environment:

#

# SIGSEGV (0xb) at pc=0x00007ff7b7dab296, pid=13026, tid=13037

#

# JRE version: OpenJDK Runtime Environment (11.0.15+10) (build 11.0.15+10-Ubuntu-0ubuntu0.18.04.1)

# Java VM: OpenJDK 64-Bit Server VM (11.0.15+10-Ubuntu-0ubuntu0.18.04.1, mixed mode, sharing, tiered, compressed oops, g1 gc, linux-amd64)

# Problematic frame:

# C [libdd.so+0x30296] Cudd_EqualSupNormRel+0x26

#

# Core dump will be written. Default location: Core dumps may be processed with "/usr/share/apport/apport -p%p -s%s -c%c -d%d -P%P -u%u -g%g -- %E" (or dumping to /home/users/mn207/monitoring/prism_codegen/experiments/correctness/scripts/core.13026)

#

# If you would like to submit a bug report, please visit:

# Unknown

# The crash happened outside the Java Virtual Machine in native code.

# See problematic frame for where to report the bug.

#

--------------- S U M M A R Y ------------

Command Line: -Xmx1g -Xss4m -Djava.awt.headless=true -Djava.library.path=/home/users/mn207/prism/lib prism.PrismCL -cuddmaxmem 2g /home/users/mn207/monitoring/prism_codegen/experiments/correctness/simulations/6_sites_5_users/not_inline/config_0.prism /home/users/mn207/monitoring/prism_codegen/prop_share.props -prop 1 -heuristic speed

Host: Intel(R) Xeon(R) CPU E5640 @ 2.67GHz, 16 cores, 29G, Ubuntu 18.04.6 LTS

Time: Fri Jul 29 05:57:18 2022 EDT elapsed time: 49463.181236 seconds (0d 13h 44m 23s)

--------------- T H R E A D ---------------

Current thread (0x00007ff810017000): JavaThread "main" [_thread_in_native, id=13037, stack(0x00007ff815834000,0x00007ff815c35000)]

Stack: [0x00007ff815834000,0x00007ff815c35000], sp=0x00007ff815c32c50, free space=4091k

Native frames: (J=compiled Java code, A=aot compiled Java code, j=interpreted, Vv=VM code, C=native code)

C [libdd.so+0x30296] Cudd_EqualSupNormRel+0x26

Java frames: (J=compiled Java code, j=interpreted, Vv=VM code)

j mtbdd.PrismMTBDD.PM_NondetUntil(JJJJIJIJIJJZ)J+0

j mtbdd.PrismMTBDD.NondetUntil(Ljdd/JDDNode;Lodd/ODDNode;Ljdd/JDDNode;Ljdd/JDDVars;Ljdd/JDDVars;Ljdd/JDDVars;Ljdd/JDDNode;Ljdd/JDDNode;Z)Ljdd/JDDNode;+55

j prism.NondetModelChecker.computeUntilProbs(Ljdd/JDDNode;Ljdd/JDDNode;Ljdd/JDDNode;Ljdd/JDDNode;Ljdd/JDDNode;Z)Lprism/StateValues;+1217

j prism.NondetModelChecker.checkProbUntil(Ljdd/JDDNode;Ljdd/JDDNode;ZZ)Lprism/StateValues;+256

j prism.NondetModelChecker.checkProbUntil(Lparser/ast/ExpressionTemporal;ZZLjdd/JDDNode;)Lprism/StateValues;+68

j prism.NondetModelChecker.checkProbPathFormulaSimple(Lparser/ast/Expression;ZZLjdd/JDDNode;)Lprism/StateValues;+124

j prism.NondetModelChecker.checkProbPathFormula(Lparser/ast/Expression;ZZLjdd/JDDNode;)Lprism/StateValues;+55

j prism.NondetModelChecker.checkExpressionProb(Lparser/ast/ExpressionProb;ZLjdd/JDDNode;)Lprism/StateValues;+177

j prism.NondetModelChecker.checkExpressionProb(Lparser/ast/ExpressionProb;Ljdd/JDDNode;)Lprism/StateValues;+4

j prism.NondetModelChecker.checkExpression(Lparser/ast/Expression;Ljdd/JDDNode;)Lprism/StateValues;+33

j prism.StateModelChecker.checkExpressionFilter(Lparser/ast/ExpressionFilter;Ljdd/JDDNode;)Lprism/StateValues;+362

j prism.StateModelChecker.checkExpression(Lparser/ast/Expression;Ljdd/JDDNode;)Lprism/StateValues;+270

j prism.NonProbModelChecker.checkExpression(Lparser/ast/Expression;Ljdd/JDDNode;)Lprism/StateValues;+49

j prism.NondetModelChecker.checkExpression(Lparser/ast/Expression;Ljdd/JDDNode;)Lprism/StateValues;+108

j prism.StateModelChecker.check(Lparser/ast/Expression;)Lprism/Result;+93

j prism.Prism.modelCheck(Lparser/ast/PropertiesFile;Lparser/ast/Property;)Lprism/Result;+640

j prism.PrismCL.run([Ljava/lang/String;)V+881

j prism.PrismCL.go([Ljava/lang/String;)V+2

j prism.PrismCL.main([Ljava/lang/String;)V+25

v ~StubRoutines::call_stub

I understand that this is a large model. However I am running it on a computing cluster, so thought it should be able to run to completion. Right now I had CUDD set to 2g and JVM set to 1g. My machine has a lot more memory, so would increasing the memory available to CUUD/JVM solve my problems? Or is it an intrinsic problem with the number of states in the model itself? 

In other words, should larger machines be able to handle more states/transitions, or is it an intrinsic limitation in PRISM itself?

With regards to compressing my model, I have already eliminated all my extra variables, and reduced the variables' ranges. Are the number of transitions solely dependent on the number of variables, or is there a way to decrease the number of transitions independently? If so, could you please provide a brief example to help me understand.

Thanks so much,

Mridu