From 453a96d80dbd1e9d63a27efdef4fb6522efcd8d4 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 11 Jul 2017 13:06:19 +0000 Subject: [PATCH] MTBDD Prob0/1 computations: 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@12007 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/mtbdd/PM_Prob0.cc | 9 ++++++++- prism/src/mtbdd/PM_Prob0A.cc | 10 +++++++++- prism/src/mtbdd/PM_Prob0E.cc | 11 ++++++++++- prism/src/mtbdd/PM_Prob1.cc | 10 +++++++++- prism/src/mtbdd/PM_Prob1A.cc | 10 +++++++++- prism/src/mtbdd/PM_Prob1E.cc | 11 ++++++++++- 6 files changed, 55 insertions(+), 6 deletions(-) diff --git a/prism/src/mtbdd/PM_Prob0.cc b/prism/src/mtbdd/PM_Prob0.cc index 5a0c250a..a2fbc796 100644 --- a/prism/src/mtbdd/PM_Prob0.cc +++ b/prism/src/mtbdd/PM_Prob0.cc @@ -80,14 +80,19 @@ jlong __jlongpointer psi // psi(b2) Cudd_Ref(sol); tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, 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, cvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b1); - tmp = DD_And(ddman, b1, tmp); + tmp = DD_And(ddman, b1, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b2); tmp = DD_Or(ddman, b2, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); if (tmp == sol) { done = true; @@ -96,10 +101,12 @@ jlong __jlongpointer psi // psi(b2) sol = tmp; } sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars); + if (sol == NULL) return ptr_to_jlong(NULL); // actual answer is states NOT reachable Cudd_Ref(reach); sol = DD_And(ddman, reach, DD_Not(ddman, sol)); + if (sol == NULL) return ptr_to_jlong(NULL); // stop clock time_taken = (double)(util_cpu_time() - start1)/1000; diff --git a/prism/src/mtbdd/PM_Prob0A.cc b/prism/src/mtbdd/PM_Prob0A.cc index 6ea78874..b0a81030 100644 --- a/prism/src/mtbdd/PM_Prob0A.cc +++ b/prism/src/mtbdd/PM_Prob0A.cc @@ -86,16 +86,22 @@ jlong __jlongpointer psi // psi(b2) Cudd_Ref(sol); tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, 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, cvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); tmp = DD_ThereExists(ddman, tmp, ndvars, num_ndvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b1); - tmp = DD_And(ddman, b1, tmp); + tmp = DD_And(ddman, b1, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b2); tmp = DD_Or(ddman, b2, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); if (tmp == sol) { done = true; @@ -104,10 +110,12 @@ jlong __jlongpointer psi // psi(b2) sol = tmp; } sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars); + if (sol == NULL) return ptr_to_jlong(NULL); // actual answer is states NOT reachable Cudd_Ref(reach); sol = DD_And(ddman, reach, DD_Not(ddman, sol)); + if (sol == NULL) return ptr_to_jlong(NULL); // stop clock time_taken = (double)(util_cpu_time() - start1)/1000; diff --git a/prism/src/mtbdd/PM_Prob0E.cc b/prism/src/mtbdd/PM_Prob0E.cc index 73d6eb64..e08fff07 100644 --- a/prism/src/mtbdd/PM_Prob0E.cc +++ b/prism/src/mtbdd/PM_Prob0E.cc @@ -88,18 +88,25 @@ jlong __jlongpointer psi // psi(b2) Cudd_Ref(sol); tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, 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, cvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(mask); tmp = DD_Or(ddman, tmp, mask); + if (tmp == NULL) return ptr_to_jlong(NULL); tmp = DD_ForAll(ddman, tmp, ndvars, num_ndvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b1); - tmp = DD_And(ddman, b1, tmp); + tmp = DD_And(ddman, b1, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b2); tmp = DD_Or(ddman, b2, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); if (tmp == sol) { done = true; @@ -108,10 +115,12 @@ jlong __jlongpointer psi // psi(b2) sol = tmp; } sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars); + if (sol == NULL) return ptr_to_jlong(NULL); // actual answer is states NOT reachable Cudd_Ref(reach); sol = DD_And(ddman, reach, DD_Not(ddman, sol)); + if (sol == NULL) return ptr_to_jlong(NULL); // stop clock time_taken = (double)(util_cpu_time() - start1)/1000; diff --git a/prism/src/mtbdd/PM_Prob1.cc b/prism/src/mtbdd/PM_Prob1.cc index da6312a3..79d4ba37 100644 --- a/prism/src/mtbdd/PM_Prob1.cc +++ b/prism/src/mtbdd/PM_Prob1.cc @@ -82,16 +82,22 @@ jlong __jlongpointer _no // no Cudd_Ref(sol); tmp = DD_PermuteVariables(ddman, sol, rvars, cvars, 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, cvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b1); - tmp = DD_And(ddman, b1, tmp); + tmp = DD_And(ddman, b1, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b2); tmp = DD_And(ddman, DD_Not(ddman, b2), tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(no); tmp = DD_Or(ddman, no, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); if (tmp == sol) { done = true; @@ -100,10 +106,12 @@ jlong __jlongpointer _no // no sol = tmp; } sol = DD_PermuteVariables(ddman, sol, cvars, rvars, num_cvars); + if (sol == NULL) return ptr_to_jlong(NULL); // actual answer is states NOT reachable Cudd_Ref(reach); sol = DD_And(ddman, reach, DD_Not(ddman, sol)); + if (sol == NULL) return ptr_to_jlong(NULL); // stop clock time_taken = (double)(util_cpu_time() - start1)/1000; diff --git a/prism/src/mtbdd/PM_Prob1A.cc b/prism/src/mtbdd/PM_Prob1A.cc index 16e1fdab..668467ba 100644 --- a/prism/src/mtbdd/PM_Prob1A.cc +++ b/prism/src/mtbdd/PM_Prob1A.cc @@ -81,11 +81,13 @@ jlong __jlongpointer psi // psi(b2) Cudd_Ref(reach); Cudd_Ref(no); notno = DD_And(ddman, reach, DD_Not(ddman, no)); + if (notno == NULL) return ptr_to_jlong(NULL); // greatest fixed point loop Cudd_Ref(b2); Cudd_Ref(notno); sol = DD_Or(ddman, b2, notno); + if (sol == NULL) return ptr_to_jlong(NULL); done = false; iters = 0; @@ -96,17 +98,23 @@ jlong __jlongpointer psi // psi(b2) Cudd_Ref(sol); tmp = DD_SwapVariables(ddman, sol, rvars, cvars, num_rvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(trans01); tmp = DD_ForAll(ddman, DD_Implies(ddman, trans01, tmp), cvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(mask); tmp = DD_Or(ddman, tmp, mask); + if (tmp == NULL) return ptr_to_jlong(NULL); tmp = DD_ForAll(ddman, tmp, ndvars, num_ndvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(notno); - tmp = DD_And(ddman, notno, tmp); + tmp = DD_And(ddman, notno, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b2); tmp = DD_Or(ddman, b2, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); if (tmp == sol) { done = true; diff --git a/prism/src/mtbdd/PM_Prob1E.cc b/prism/src/mtbdd/PM_Prob1E.cc index 1bb8b542..9cb9b5ff 100644 --- a/prism/src/mtbdd/PM_Prob1E.cc +++ b/prism/src/mtbdd/PM_Prob1E.cc @@ -82,6 +82,7 @@ jlong __jlongpointer _no // no Cudd_Ref(reach); Cudd_Ref(no); u = DD_And(ddman, reach, DD_Not(ddman, no)); + if (u == NULL) return ptr_to_jlong(NULL); //u = DD_Constant(ddman, 1); u_done = false; iters = 0; @@ -98,21 +99,29 @@ jlong __jlongpointer _no // no Cudd_Ref(u); tmp = DD_SwapVariables(ddman, u, rvars, cvars, num_rvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(trans01); tmp = DD_ForAll(ddman, DD_Implies(ddman, trans01, tmp), cvars, num_cvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(v); tmp2 = DD_SwapVariables(ddman, v, rvars, cvars, num_rvars); + if (tmp2 == NULL) return ptr_to_jlong(NULL); Cudd_Ref(trans01); tmp2 = DD_ThereExists(ddman, DD_And(ddman, tmp2, trans01), cvars, num_cvars); + if (tmp2 == NULL) return ptr_to_jlong(NULL); tmp = DD_And(ddman, tmp, tmp2); + if (tmp == NULL) return ptr_to_jlong(NULL); tmp = DD_ThereExists(ddman, tmp, ndvars, num_ndvars); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b1); - tmp = DD_And(ddman, b1, tmp); + tmp = DD_And(ddman, b1, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); Cudd_Ref(b2); tmp = DD_Or(ddman, b2, tmp); + if (tmp == NULL) return ptr_to_jlong(NULL); if (tmp == v) { v_done = true;