Browse Source

some further changes

Former-commit-id: ad72bbef36
tempestpy_adaptions
sjunges 9 years ago
parent
commit
b74cd564e4
  1. 20
      src/storage/dft/DFTIsomorphism.h
  2. 4
      src/storage/dft/elements/DFTGate.h

20
src/storage/dft/DFTIsomorphism.h

@ -414,12 +414,27 @@ namespace storage {
if(dft.isGate(indexpair.first)) {
assert(dft.isGate(indexpair.second));
auto const& lGate = dft.getGate(indexpair.first);
auto const& rGate = dft.getGate(indexpair.second);
if(lGate->isDynamicGate()) {
std::vector<size_t> childrenLeftMapped;
for(auto const& child : lGate->children() ) {
assert(bleft.has(child->id()));
childrenLeftMapped.push_back(bijection.at(child->id()));
}
std::vector<size_t> childrenRight;
for(auto const& child : rGate->children() ) {
assert(bright.has(child->id()));
childrenRight.push_back(child->id());
}
if(childrenLeftMapped != childrenRight) {
return false;
}
} else {
std::set<size_t> childrenLeftMapped;
for(auto const& child : lGate->children() ) {
assert(bleft.has(child->id()));
childrenLeftMapped.insert(bijection.at(child->id()));
}
auto const& rGate = dft.getGate(indexpair.second);
std::set<size_t> childrenRight;
for(auto const& child : rGate->children() ) {
assert(bright.has(child->id()));
@ -428,6 +443,9 @@ namespace storage {
if(childrenLeftMapped != childrenRight) {
return false;
}
}
} else if(dft.isDependency(indexpair.first)) {
assert(dft.isDependency(indexpair.second));
auto const& lDep = dft.getDependency(indexpair.first);

4
src/storage/dft/elements/DFTGate.h

@ -35,6 +35,10 @@ namespace storm {
return true;
}
bool isDynamicGate() const {
return !isStaticGateType(this->type());
}
virtual std::string typestring() const = 0;

Loading…
Cancel
Save