Setting 'dft-statistics' prints information about intermediate approximation results

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.

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

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<storm::settings::modules::IOSettings>();
+            auto dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
 
             // Find symmetries
             std::map<size_t, std::vector<std::vector<size_t>>> 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<storm::settings::modules::IOSettings>();
                     if (ioSettings.isExportExplicitSet()) {
                         std::vector<std::string> 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<ValueType>(approxResult.first) &&
                                     !storm::utility::isInfinity<ValueType>(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;

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() {

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;
 
             };