From 7f66e8b286cc5db7fac542170bab208b16a03cc9 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 11 Jul 2017 13:06:37 +0000 Subject: [PATCH] MTBDD Reachability computation: Gracefully handle CUDD out-of-memory We check after each DD operation whether the returned DdNode* is NULL and abort the computation. The NULL return value is then caught in the JDD.ptrToNode() method, which raises a CuddOutOfMemoryException. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12008 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/mtbdd/PM_Reachability.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/prism/src/mtbdd/PM_Reachability.cc b/prism/src/mtbdd/PM_Reachability.cc index ae4e8d91..39be70c0 100644 --- a/prism/src/mtbdd/PM_Reachability.cc +++ b/prism/src/mtbdd/PM_Reachability.cc @@ -76,6 +76,7 @@ jlong __jlongpointer s // start state iters = 0; Cudd_Ref(init); reach = DD_PermuteVariables(ddman, init, rvars, cvars, num_rvars); + if (reach == NULL) return ptr_to_jlong(NULL); while (!done) { iters++; @@ -89,11 +90,15 @@ jlong __jlongpointer s // start state // perform iteration Cudd_Ref(reach); tmp = DD_PermuteVariables(ddman, reach, cvars, rvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(trans01); tmp = DD_And(ddman, tmp, trans01); + if (tmp == NULL) return ptr_to_jlong(NULL); tmp = DD_ThereExists(ddman, tmp, rvars, num_rvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(reach); tmp = DD_Or(ddman, reach, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); // check convergence if (tmp == reach) { done = true; @@ -107,6 +112,7 @@ jlong __jlongpointer s // start state } } reach = DD_PermuteVariables(ddman, reach, cvars, rvars, num_cvars); + if (reach == NULL) return ptr_to_jlong(NULL); } else { // initialise @@ -129,15 +135,20 @@ jlong __jlongpointer s // start state // perform iteration Cudd_Ref(frontier); tmp = DD_PermuteVariables(ddman, frontier, cvars, rvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(trans01); tmp = DD_And(ddman, tmp, trans01); + if (tmp == NULL) return ptr_to_jlong(NULL); tmp = DD_ThereExists(ddman, tmp, rvars, num_rvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(reach); tmp = DD_Or(ddman, reach, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_RecursiveDeref(ddman, frontier); Cudd_Ref(tmp); Cudd_Ref(reach); frontier = DD_And(ddman, tmp, DD_Not(ddman, reach)); + if (frontier) return ptr_to_jlong(NULL); // check convergence if (frontier == Cudd_ReadZero(ddman)) { done = true; @@ -151,6 +162,7 @@ jlong __jlongpointer s // start state } } reach = DD_PermuteVariables(ddman, reach, cvars, rvars, num_cvars); + if (reach == NULL) return ptr_to_jlong(NULL); Cudd_RecursiveDeref(ddman, frontier); }