Browse Source

Added error handling of gates with restricton as child and changed order of topoSort and rank computation to ensure that rank is only computed for acyclic DFTs

main
Alexander Bork 6 years ago
parent
commit
d31fae859f
  1. 8
      src/storm-dft/builder/DFTBuilder.cpp

8
src/storm-dft/builder/DFTBuilder.cpp

@ -26,6 +26,9 @@ namespace storm {
if (itFind != mElements.end()) { if (itFind != mElements.end()) {
// Child found // Child found
DFTElementPointer childElement = itFind->second; DFTElementPointer childElement = itFind->second;
STORM_LOG_THROW(!childElement->isRestriction(), storm::exceptions::WrongFormatException,
"Restictor " << childElement->name() << " is not allowed as child of gate "
<< gate->name());
if(!childElement->isDependency()) { if(!childElement->isDependency()) {
gate->pushBackChild(childElement); gate->pushBackChild(childElement);
childElement->addParent(gate); childElement->addParent(gate);
@ -83,13 +86,12 @@ namespace storm {
} }
// Sort elements topologically // Sort elements topologically
DFTElementVector elems = topoSort();
// compute rank // compute rank
for (auto& elem : mElements) {
for (auto &elem : mElements) {
computeRank(elem.second); computeRank(elem.second);
} }
DFTElementVector elems = topoSort();
// Set ids // Set ids
size_t id = 0; size_t id = 0;
for(DFTElementPointer e : elems) { for(DFTElementPointer e : elems) {

Loading…
Cancel
Save