s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Joachim Klein 9 years ago
parent
62f1e7d0ac
commit
453a96d80d
6 changed files with 55 additions and 6 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      prism/src/mtbdd/PM_Prob0.cc
  2. 10
      prism/src/mtbdd/PM_Prob0A.cc
  3. 11
      prism/src/mtbdd/PM_Prob0E.cc
  4. 10
      prism/src/mtbdd/PM_Prob1.cc
  5. 10
      prism/src/mtbdd/PM_Prob1A.cc
  6. 11
      prism/src/mtbdd/PM_Prob1E.cc

9
prism/src/mtbdd/PM_Prob0.cc
View File

@ -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;

10
prism/src/mtbdd/PM_Prob0A.cc
View File

@ -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;

11
prism/src/mtbdd/PM_Prob0E.cc
View File

@ -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;

10
prism/src/mtbdd/PM_Prob1.cc
View File

@ -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;

10
prism/src/mtbdd/PM_Prob1A.cc
View File

@ -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;

11
prism/src/mtbdd/PM_Prob1E.cc
View File

@ -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;

Write Preview
Loading…
Cancel
Save