Browse Source

Refactored DFS search into own method

Former-commit-id: 3efbcf062f
main
Mavo 9 years ago
parent
commit
2754450f91
  1. 46
      src/storage/dft/DFT.cpp
  2. 2
      src/storage/dft/DFT.h

46
src/storage/dft/DFT.cpp

@ -82,6 +82,30 @@ namespace storm {
visitQueue.push(subTreeRoots[0]); visitQueue.push(subTreeRoots[0]);
bool consideredDependencies = false; bool consideredDependencies = false;
while (true) { while (true) {
if (consideredDependencies) {
break;
}
stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
// Consider dependencies
for (size_t idDependency : getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
visitQueue.push(dependency->id());
visitQueue.push(dependency->triggerEvent()->id());
visitQueue.push(dependency->dependentEvent()->id());
}
consideredDependencies = true;
}
assert(stateIndex = mStateVectorSize);
STORM_LOG_TRACE(generationInfo);
return generationInfo;
}
template<typename ValueType>
size_t DFT<ValueType>::performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, std::set<size_t>& visited, size_t stateIndex) const {
while (!visitQueue.empty()) { while (!visitQueue.empty()) {
size_t id = visitQueue.front(); size_t id = visitQueue.front();
visitQueue.pop(); visitQueue.pop();
@ -114,28 +138,8 @@ namespace storm {
} }
} }
if (consideredDependencies) {
break;
}
// Consider dependencies
for (size_t idDependency : getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
visitQueue.push(dependency->id());
visitQueue.push(dependency->triggerEvent()->id());
visitQueue.push(dependency->dependentEvent()->id());
return stateIndex;
} }
consideredDependencies = true;
}
assert(stateIndex = mStateVectorSize);
STORM_LOG_TRACE(generationInfo);
return generationInfo;
}
template<typename ValueType> template<typename ValueType>
std::string DFT<ValueType>::getElementsString() const { std::string DFT<ValueType>::getElementsString() const {

2
src/storage/dft/DFT.h

@ -127,6 +127,8 @@ namespace storm {
DFTStateGenerationInfo buildStateGenerationInfo(std::vector<size_t> const& subTreeRoots, std::vector<std::vector<size_t>> const& symmetries) const; DFTStateGenerationInfo buildStateGenerationInfo(std::vector<size_t> const& subTreeRoots, std::vector<std::vector<size_t>> const& symmetries) const;
size_t performStateGenerationInfoDFS(DFTStateGenerationInfo& generationInfo, std::queue<size_t>& visitQueue, std::set<size_t>& visited, size_t stateIndex) const;
size_t stateVectorSize() const { size_t stateVectorSize() const {
return mStateVectorSize; return mStateVectorSize;
} }

Loading…
Cancel
Save