diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index d3eb05851..9948af256 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -25,17 +25,24 @@ template std::shared_ptr> loadDFT() { storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); - + std::shared_ptr> dft; // Build DFT from given file. if (dftIOSettings.isDftJsonFileSet()) { storm::parser::DFTJsonParser parser; STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); - return std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); + dft = std::make_shared>(parser.parseJson(dftIOSettings.getDftJsonFilename())); } else { storm::parser::DFTGalileoParser parser; STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); - return std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); + dft = std::make_shared>(parser.parseDFT(dftIOSettings.getDftFilename())); + } + + if (dftIOSettings.isDisplayStatsSet()) { + std::cout << "=============DFT Statistics==============" << std::endl; + dft->writeStatsToStream(std::cout); + std::cout << "=========================================" << std::endl; } + return dft; } /*! diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp index cf656333d..8704cd036 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.cpp +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -26,6 +26,8 @@ namespace storm { const std::string DftIOSettings::maxValueOptionName = "max"; const std::string DftIOSettings::transformToGspnOptionName = "gspn"; const std::string DftIOSettings::exportToJsonOptionName = "export-json"; + const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats"; + DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) @@ -40,6 +42,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build()); + } bool DftIOSettings::isDftFileSet() const { @@ -109,6 +113,10 @@ namespace storm { return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); } + bool DftIOSettings::isDisplayStatsSet() const { + return this->getOption(displayStatsOptionName).getHasOptionBeenSet(); + } + void DftIOSettings::finalize() { } @@ -121,3 +129,4 @@ namespace storm { } // namespace modules } // namespace settings } // namespace storm + diff --git a/src/storm-dft/settings/modules/DftIOSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h index 8a8fbcdd1..f57f9ed44 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -121,6 +121,13 @@ namespace storm { * @return The name of the json file to export to. */ std::string getExportJsonFilename() const; + + /*! + * Retrieves whether statistics for the DFT should be displayed. + * + * @return True if the statistics option was set. + */ + bool isDisplayStatsSet() const; bool check() const override; void finalize() override; @@ -143,7 +150,8 @@ namespace storm { static const std::string maxValueOptionName; static const std::string transformToGspnOptionName; static const std::string exportToJsonOptionName; - + static const std::string displayStatsOptionName; + }; } // namespace modules diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index b21338c74..6f5db6a44 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -378,7 +378,35 @@ namespace storm { STORM_LOG_TRACE(newDft.getElementsString()); return newDft.optimize(); } - + + template + size_t DFT::nrDynamicElements() const { + size_t noDyn = 0; + for (auto const& elem : mElements) { + switch (elem->type()) { + case DFTElementType::AND: + case DFTElementType::OR: + case DFTElementType::VOT: + case DFTElementType::BE: + case DFTElementType::CONSTF: + case DFTElementType::CONSTS: + break; + case DFTElementType::PAND: + case DFTElementType::SPARE: + case DFTElementType::POR: + case DFTElementType::SEQ: + case DFTElementType::MUTEX: + case DFTElementType::PDEP: + noDyn += 1; + break; + default: + STORM_LOG_ASSERT(false, "DFT element type " << elem->type() << " not known."); + break; + } + } + return noDyn; + } + template std::string DFT::getElementsString() const { std::stringstream stream; @@ -766,6 +794,13 @@ namespace storm { std::sort(outgoingDeps.begin(), outgoingDeps.end()); return std::make_tuple(parents, ingoingDeps, outgoingDeps); } + + template + void DFT::writeStatsToStream(std::ostream& stream) const { + stream << "Number of BEs: " << nrBasicElements() << std::endl; + stream << "Number of dynamic elements: " << nrDynamicElements() << std::endl; + stream << "Number of elements: " << nrElements() << std::endl; + } // Explicitly instantiate the class. template class DFT; diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 304018d97..20c42fdb8 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -89,6 +89,8 @@ namespace storm { size_t nrBasicElements() const { return mNrOfBEs; } + + size_t nrDynamicElements() const; size_t getTopLevelIndex() const { return mTopLevelIndex; @@ -275,6 +277,8 @@ namespace storm { return mLayoutInfo.at(id); } + void writeStatsToStream(std::ostream& stream) const; + private: std::tuple, std::vector, std::vector> getSortedParentAndDependencyIds(size_t index) const;