Browse Source

Output relevant events for better debugging

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
0a1ed0270a
  1. 1
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  2. 17
      src/storm-dft/storage/dft/DFT.cpp
  3. 6
      src/storm-dft/storage/dft/DFT.h

1
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@ -44,6 +44,7 @@ namespace storm {
this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents); this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents);
// Mark top level element as relevant // Mark top level element as relevant
this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true); this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true);
STORM_LOG_DEBUG("Relevant events: " << this->dft.getRelevantEventsString());
if (this->relevantEvents.empty()) { if (this->relevantEvents.empty()) {
// Only interested in top level event -> introduce unique failed state // Only interested in top level event -> introduce unique failed state
this->uniqueFailedState = true; this->uniqueFailedState = true;

17
src/storm-dft/storage/dft/DFT.cpp

@ -874,6 +874,23 @@ namespace storm {
} }
} }
template<typename ValueType>
std::string DFT<ValueType>::getRelevantEventsString() const {
std::stringstream stream;
bool first = true;
for (auto const& elem : mElements) {
if (elem->isRelevant()) {
if (first) {
first = false;
} else {
stream << ", ";
}
stream << elem->name() << " [" << elem->id() << "]";
}
}
return stream.str();
}
template<typename ValueType> template<typename ValueType>
void DFT<ValueType>::writeStatsToStream(std::ostream& stream) const { void DFT<ValueType>::writeStatsToStream(std::ostream& stream) const {
// Count individual types of elements // Count individual types of elements

6
src/storm-dft/storage/dft/DFT.h

@ -325,6 +325,12 @@ namespace storm {
*/ */
void setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const; void setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const;
/*!
* Get a string containing the list of all relevant events.
* @return String containing all relevant events.
*/
std::string getRelevantEventsString() const;
private: private:
std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> getSortedParentAndDependencyIds(size_t index) const; std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> getSortedParentAndDependencyIds(size_t index) const;

Loading…
Cancel
Save