sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

let's fill them hashtables (I mean there were there anyway, so we could as well use 'em)

tempestpy_adaptions
dehnert 8 years ago
parent
9e8d6eee90
commit
33cdee94dc
4 changed files with 37 additions and 12 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. 12
      src/storm/storage/dd/cudd/InternalCuddAdd.cpp
  2. 13
      src/storm/storage/dd/cudd/InternalCuddBdd.cpp
  3. 12
      src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
  4. 12
      src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp

12
src/storm/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -386,13 +386,17 @@ namespace storm {
thenOffset = 1;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
std::shared_ptr<Odd> elseNode = createOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
@ -401,7 +405,9 @@ namespace storm {
uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
}
}
}

13
src/storm/storage/dd/cudd/InternalCuddBdd.cpp
View File

@ -355,14 +355,19 @@ namespace storm {
thenOffset = 1 - thenOffset;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
DdNode const* thenDdNode = Cudd_T_const(dd);
@ -375,7 +380,9 @@ namespace storm {
std::shared_ptr<Odd> elseNode = createOddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = createOddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
}
}
}

12
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -570,13 +570,17 @@ namespace storm {
thenOffset = 1;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
std::shared_ptr<Odd> elseNode = createOddRec(mtbdd_regular(mtbdd_getlow(dd)), currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
@ -585,7 +589,9 @@ namespace storm {
uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
}
}
}

12
src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp
View File

@ -337,14 +337,18 @@ namespace storm {
thenOffset = 1 - thenOffset;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, complement, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
BDD thenDdNode = sylvan_high(dd);
@ -357,7 +361,9 @@ namespace storm {
std::shared_ptr<Odd> elseNode = createOddRec(bdd_regular(elseDdNode), elseComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = createOddRec(bdd_regular(thenDdNode), thenComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
}
}
}

Write Preview
Loading…
Cancel
Save