From 06941e7c48745f9393b9ca9a41ec345f8e28a416 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Apr 2020 17:38:23 +0200 Subject: [PATCH] Setting 'dft-statistics' prints information about intermediate approximation results --- CHANGELOG.md | 1 + src/storm-dft-cli/storm-dft.cpp | 5 +++-- .../modelchecker/dft/DFTModelChecker.cpp | 22 ++++++++++++++----- .../settings/modules/DftIOSettings.cpp | 9 ++++---- .../settings/modules/DftIOSettings.h | 7 +++--- 5 files changed, 30 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2c11fea31..51a33bc11 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,7 @@ Version 1.5.x - Scheduler export: Properly handle models with end components. Added export in .json format. - CMake: Search for Gurobi prefers new versions - Tests: Enabled tests for permissive schedulers +- `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics. ## Version 1.5.1 (2020/03) - Jani models are now parsed using exact arithmetic. diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 87338ff30..f7a5093a7 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -40,9 +40,10 @@ void processOptions() { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); } - // DFT statistics - if (dftIOSettings.isDisplayStatsSet()) { + // Show statistics about DFT (number of gates, etc.) + if (dftIOSettings.isShowDftStatisticsSet()) { dft->writeStatsToStream(std::cout); + std::cout << std::endl; } // Export to json diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 00fe1d0d9..241027e8f 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -13,6 +13,7 @@ #include "storm-dft/api/storm-dft.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" +#include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" @@ -305,6 +306,8 @@ namespace storm { storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { explorationTimer.start(); + auto ioSettings = storm::settings::getModule(); + auto dftIOSettings = storm::settings::getModule(); // Find symmetries std::map>> emptySymmetry; @@ -355,12 +358,12 @@ namespace storm { STORM_LOG_DEBUG("Getting model for lower bound..."); model = builder.getModelApproximation(true, !probabilityFormula); // We only output the info from the lower bound as the info for the upper bound is the same - if (printInfo) { + if (printInfo && dftIOSettings.isShowDftStatisticsSet()) { + std::cout << "Model in iteration " << (iteration + 1) << ":" << std::endl; model->printModelInformationToStream(std::cout); } buildingTimer.stop(); - auto ioSettings = storm::settings::getModule(); if (ioSettings.isExportExplicitSet()) { std::vector parameterNames; // TODO fill parameter names @@ -388,24 +391,33 @@ namespace storm { << approxResult.second); approxResult.second = newResult[0]; - ++iteration; STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second); - STORM_LOG_DEBUG("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); totalTimer.stop(); - printTimings(); + if (printInfo && dftIOSettings.isShowDftStatisticsSet()) { + std::cout << "Result after iteration " << (iteration + 1) << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")" << std::endl; + printTimings(); + std::cout << std::endl; + } else { + STORM_LOG_DEBUG("Result after iteration " << (iteration + 1) << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); + } + totalTimer.start(); STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); + ++iteration; } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); //STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); + if (printInfo) { + model->printModelInformationToStream(std::cout); + } dft_results results; results.push_back(approxResult); return results; diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp index 662fd0f34..fca700e5a 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.cpp +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -26,7 +26,8 @@ namespace storm { const std::string DftIOSettings::maxValueOptionName = "max"; const std::string DftIOSettings::exportToJsonOptionName = "export-json"; const std::string DftIOSettings::exportToSmtOptionName = "export-smt"; - const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats"; + const std::string DftIOSettings::dftStatisticsOptionName = "dft-statistics"; + const std::string DftIOSettings::dftStatisticsOptionShortName = "dftstats"; DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { @@ -62,7 +63,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the smtlib2 file to export to.").build()) .build()); - this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dftStatisticsOptionName, false, "Sets whether to display DFT statistics if available.").setShortName(dftStatisticsOptionShortName).build()); } bool DftIOSettings::isDftFileSet() const { @@ -136,8 +137,8 @@ namespace storm { return this->getOption(exportToSmtOptionName).getArgumentByName("filename").getValueAsString(); } - bool DftIOSettings::isDisplayStatsSet() const { - return this->getOption(displayStatsOptionName).getHasOptionBeenSet(); + bool DftIOSettings::isShowDftStatisticsSet() const { + return this->getOption(dftStatisticsOptionName).getHasOptionBeenSet(); } void DftIOSettings::finalize() { diff --git a/src/storm-dft/settings/modules/DftIOSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h index 60369b36e..37a5fb464 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -130,11 +130,11 @@ namespace storm { std::string getExportSmtFilename() const; /*! - * Retrieves whether statistics for the DFT should be displayed. + * Retrieves whether statistics about the DFT analysis should be displayed. * * @return True if the statistics option was set. */ - bool isDisplayStatsSet() const; + bool isShowDftStatisticsSet() const; bool check() const override; void finalize() override; @@ -157,7 +157,8 @@ namespace storm { static const std::string maxValueOptionName; static const std::string exportToJsonOptionName; static const std::string exportToSmtOptionName; - static const std::string displayStatsOptionName; + static const std::string dftStatisticsOptionName; + static const std::string dftStatisticsOptionShortName; };