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

dd_*.cc: Argument checking, if any DdNode is NULL return NULL 

This allows nesting of DD_ functions in the presence of CUDD memory errors.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10487 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 11 years ago
parent
f559e0adb8
commit
4dfcd39fd1
5 changed files with 88 additions and 29 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. 24
      prism/src/dd/dd_abstr.cc
  2. 38
      prism/src/dd/dd_basics.cc
  3. 23
      prism/src/dd/dd_matrix.cc
  4. 24
      prism/src/dd/dd_term.cc
  5. 8
      prism/src/dd/dd_vars.cc

24
prism/src/dd/dd_abstr.cc
View File

@ -40,7 +40,9 @@ int num_vars
)
{
DdNode *cube, *res;
if (dd == NULL) return NULL;
cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
if (cube == NULL) return NULL;
Cudd_Ref(cube);
@ -64,7 +66,9 @@ int num_vars
)
{
DdNode *cube, *res;
if (dd == NULL) return NULL;
cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
if (cube == NULL) return NULL;
Cudd_Ref(cube);
@ -88,7 +92,9 @@ int num_vars
)
{
DdNode *cube, *res;
if (dd == NULL) return NULL;
cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
if (cube == NULL) return NULL;
Cudd_Ref(cube);
@ -112,7 +118,9 @@ int num_vars
)
{
DdNode *cube, *res;
if (dd == NULL) return NULL;
cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
if (cube == NULL) return NULL;
Cudd_Ref(cube);
@ -136,7 +144,9 @@ int num_vars
)
{
DdNode *cube, *res;
if (dd == NULL) return NULL;
cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
if (cube == NULL) return NULL;
Cudd_Ref(cube);
@ -160,7 +170,9 @@ int num_vars
)
{
DdNode *cube, *res;
if (dd == NULL) return NULL;
cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
if (cube == NULL) return NULL;
Cudd_Ref(cube);

38
prism/src/dd/dd_basics.cc
View File

@ -102,6 +102,8 @@ DdNode *DD_Not(DdManager *ddman, DdNode *dd)
{
DdNode *res;
if (dd == NULL) return NULL;
res = Cudd_addCmpl(ddman, dd);
if (res == NULL) return NULL;
Cudd_Ref(res);
@ -116,6 +118,9 @@ DdNode *DD_Or(DdManager *ddman, DdNode *dd1, DdNode *dd2)
{
DdNode *res;
if (dd1 == NULL) return NULL;
if (dd2 == NULL) return NULL;
res = Cudd_addApply(ddman, Cudd_addOr, dd1, dd2);
if (res == NULL) return NULL;
Cudd_Ref(res);
@ -129,16 +134,10 @@ DdNode *DD_Or(DdManager *ddman, DdNode *dd1, DdNode *dd2)
DdNode *DD_And(DdManager *ddman, DdNode *dd1, DdNode *dd2)
{
DdNode *n1 = DD_Not(ddman, dd1);
if (n1 == NULL) return NULL;
DdNode *n2 = DD_Not(ddman, dd2);
if (n2 == NULL) return NULL;
if (dd1 == NULL) return NULL;
if (dd2 == NULL) return NULL;
DdNode *o = DD_Or(ddman, n1, n2);
if (o == NULL) return NULL;
return DD_Not(ddman, o);
return DD_Not(ddman, DD_Or(ddman, DD_Not(ddman, dd1), DD_Not(ddman, dd2)));
}
//------------------------------------------------------------------------------
@ -147,6 +146,9 @@ DdNode *DD_Xor(DdManager *ddman, DdNode *dd1, DdNode *dd2)
{
DdNode *res;
if (dd1 == NULL) return NULL;
if (dd2 == NULL) return NULL;
res = Cudd_addApply(ddman, Cudd_addXor, dd1, dd2);
if (res == NULL) return NULL;
Cudd_Ref(res);
@ -160,10 +162,10 @@ DdNode *DD_Xor(DdManager *ddman, DdNode *dd1, DdNode *dd2)
DdNode *DD_Implies(DdManager *ddman, DdNode *dd1, DdNode *dd2)
{
DdNode *n1 = DD_Not(ddman, dd1);
if (n1 == NULL) return NULL;
if (dd1 == NULL) return NULL;
if (dd2 == NULL) return NULL;
return DD_Or(ddman, n1, dd2);
return DD_Or(ddman, DD_Not(ddman, dd1), dd2);
}
//------------------------------------------------------------------------------
@ -172,6 +174,9 @@ DdNode *DD_Apply(DdManager *ddman, int op, DdNode *dd1, DdNode *dd2)
{
DdNode *res;
if (dd1 == NULL) return NULL;
if (dd2 == NULL) return NULL;
switch (op) {
case APPLY_PLUS: res = Cudd_addApply(ddman, Cudd_addPlus, dd1, dd2); break;
case APPLY_MINUS: res = Cudd_addApply(ddman, Cudd_addMinus, dd1, dd2); break;
@ -204,6 +209,8 @@ DdNode *DD_MonadicApply(DdManager *ddman, int op, DdNode *dd)
{
DdNode *res;
if (dd == NULL) return NULL;
switch (op) {
case APPLY_FLOOR: res = Cudd_addMonadicApply(ddman, Cudd_addFloor, dd); break;
case APPLY_CEIL: res = Cudd_addMonadicApply(ddman, Cudd_addCeil, dd); break;
@ -222,6 +229,9 @@ DdNode *DD_Restrict(DdManager *ddman, DdNode *dd, DdNode *cube)
{
DdNode *res;
if (dd == NULL) return NULL;
if (cube == NULL) return NULL;
res = Cudd_addRestrict(ddman, dd, cube);
if (res == NULL) return NULL;
Cudd_Ref(res);
@ -237,6 +247,10 @@ DdNode *DD_ITE(DdManager *ddman, DdNode *dd1, DdNode *dd2, DdNode *dd3)
{
DdNode *res;
if (dd1 == NULL) return NULL;
if (dd2 == NULL) return NULL;
if (dd3 == NULL) return NULL;
res = Cudd_addIte(ddman, dd1, dd2, dd3);
if (res == NULL) return NULL;
Cudd_Ref(res);

23
prism/src/dd/dd_matrix.cc
View File

@ -51,7 +51,9 @@ double value
{
DdNode *tmp, *tmp2, *f, *tmp_f, *g, *res;
int i;
if (dd == NULL) return NULL;
// build a 0-1 ADD to store position of element of the vector
f = DD_Constant(ddman, 1);
if (f == NULL) return NULL;
@ -103,7 +105,9 @@ double value
{
DdNode *tmp, *tmp2, *f, *tmp_f, *g, *res;
int i;
if (dd == NULL) return NULL;
// build a 0-1 ADD to store position of element of the matrix
f = DD_Constant(ddman, 1);
if (f == NULL) return NULL;
@ -174,7 +178,9 @@ double value
{
DdNode *tmp, *tmp2, *f, *tmp_f, *g, *res;
int i;
if (dd == NULL) return NULL;
// build a 0-1 ADD to store position of element of the matrix
f = DD_Constant(ddman, 1);
if (f == NULL) return NULL;
@ -257,6 +263,8 @@ long x
int *inputs;
double val;
if (dd == NULL) return NULL;
// create array to store 0's & 1's used to query DD
inputs = new int[Cudd_ReadSize(ddman)];
@ -313,7 +321,10 @@ int method
)
{
DdNode *res;
if (dd1 == NULL) return NULL;
if (dd2 == NULL) return NULL;
if (method == MM_CMU) {
res = Cudd_addTimesPlus(ddman, dd1, dd2, vars, num_vars);
}
@ -348,7 +359,9 @@ int num_vars
{
int i, *permut;
DdNode *res;
if (dd == NULL) return NULL;
permut = new int[Cudd_ReadSize(ddman)];
for (i = 0; i < Cudd_ReadSize(ddman); i++) {
permut[i] = i;

24
prism/src/dd/dd_term.cc
View File

@ -43,7 +43,9 @@ double threshold
)
{
DdNode *tmp, *tmp2;
if (dd == NULL) return NULL;
tmp = Cudd_addBddThreshold(ddman, dd, threshold);
if (tmp == NULL) return NULL;
Cudd_Ref(tmp);
@ -65,7 +67,9 @@ double threshold
)
{
DdNode *tmp, *tmp2;
if (dd == NULL) return NULL;
tmp = Cudd_addBddStrictThreshold(ddman, dd, threshold);
if (tmp == NULL) return NULL;
Cudd_Ref(tmp);
@ -111,6 +115,9 @@ double threshold
)
{
DdNode* res;
if (dd == NULL) return NULL;
res = DD_Threshold(ddman, dd, threshold);
if (res == NULL) return NULL;
return DD_Not(ddman, res);
@ -126,6 +133,9 @@ double threshold
)
{
DdNode* res;
if (dd == NULL) return NULL;
res = DD_StrictThreshold(ddman, dd, threshold);
if (res == NULL) return NULL;
return DD_Not(ddman, res);
@ -155,6 +165,8 @@ double upper
{
DdNode *tmp, *tmp2;
if (dd == NULL) return NULL;
tmp = Cudd_addBddInterval(ddman, dd, lower, upper);
if (tmp == NULL) return NULL;
Cudd_Ref(tmp);
@ -177,7 +189,9 @@ int places
)
{
DdNode *res;
if (dd == NULL) return NULL;
res = Cudd_addRoundOff(ddman, dd, places);
if (res == NULL) return NULL;
Cudd_Ref(res);
@ -262,7 +276,9 @@ int num_vars
{
int i;
DdNode *ptr, *next_ptr, *filter, *res;
if (dd == NULL) return NULL;
// construct filter to get first non-zero element
ptr = dd;
filter = DD_Constant(ddman, 1);

8
prism/src/dd/dd_vars.cc
View File

@ -45,7 +45,9 @@ int num_vars
{
int i, *permut;
DdNode *res;
if (dd == NULL) return NULL;
permut = new int[Cudd_ReadSize(ddman)];
for (i = 0; i < Cudd_ReadSize(ddman); i++) {
permut[i] = i;
@ -79,7 +81,9 @@ int num_vars
)
{
DdNode *res;
if (dd == NULL) return NULL;
res = Cudd_addSwapVariables(ddman, dd, old_vars, new_vars, num_vars);
if (res != NULL) Cudd_Ref(res);
Cudd_RecursiveDeref(ddman, dd);

Write Preview
Loading…
Cancel
Save