add warning when computing minimal rewards on MDPs that reward values may be too low

src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@@ -212,6 +212,7 @@ namespace storm {
                 storm::dd::Bdd<DdType> infinityStates;
                 storm::dd::Bdd<DdType> transitionMatrixBdd = transitionMatrix.notZero();
                 if (dir == OptimizationDirection::Minimize) {
+                    STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops.");
                     infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates));
                 } else {
                     infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates));

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -286,6 +286,7 @@ namespace storm {
                 storm::storage::BitVector infinityStates;
                 storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
                 if (dir == OptimizationDirection::Minimize) {
+                    STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops.");
                     infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates);
                 } else {
                     infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates);

src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp

@@ -168,6 +168,7 @@ namespace storm {
                 storm::dd::Bdd<DdType> infinityStates;
                 storm::dd::Bdd<DdType> transitionMatrixBdd = transitionMatrix.notZero();
                 if (dir == OptimizationDirection::Minimize) {
+                    STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops.");
                     infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates));
                 } else {
                     infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates));

src/storm/settings/modules/GeneralSettings.cpp

@@ -19,8 +19,6 @@ namespace storm {
             const std::string GeneralSettings::moduleName = "general";
             const std::string GeneralSettings::helpOptionName = "help";
             const std::string GeneralSettings::helpOptionShortName = "h";
-            const std::string GeneralSettings::printTimeAndMemoryOptionName = "timemem";
-            const std::string GeneralSettings::printTimeAndMemoryOptionShortName = "tm";
             const std::string GeneralSettings::versionOptionName = "version";
             const std::string GeneralSettings::verboseOptionName = "verbose";
             const std::string GeneralSettings::verboseOptionShortName = "v";
@@ -36,12 +34,10 @@ namespace storm {
             const std::string GeneralSettings::parametricRegionOptionName = "parametricRegion";
             const std::string GeneralSettings::exactOptionName = "exact";
 
-
             GeneralSettings::GeneralSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, printTimeAndMemoryOptionName, false, "Prints CPU time and memory consumption at the end.").setShortName(printTimeAndMemoryOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
@@ -104,10 +100,6 @@ namespace storm {
                 return this->getOption(parametricRegionOptionName).getHasOptionBeenSet();
             }
                                 
-            bool GeneralSettings::isPrintTimeAndMemorySet() const {
-                return this->getOption(printTimeAndMemoryOptionName).getHasOptionBeenSet();
-            }
-
             bool GeneralSettings::isExactSet() const {
                 return this->getOption(exactOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/GeneralSettings.h

@@ -98,7 +98,6 @@ namespace storm {
                  * @return True iff the option was set.
                  */
                 bool isParametricSet() const;
-
                 
                 /*!
                  * Retrieves whether the option enabling parametric region model checking is set.
@@ -114,13 +113,6 @@ namespace storm {
                  */
                 bool isMinMaxEquationSolvingTechniqueSet() const;
                 
-                /*!
-                 * Retrieves whether time and memory consumption shall be printed at the end of a run.
-                 *
-                 * @return True iff the option was set.
-                 */
-                bool isPrintTimeAndMemorySet() const;
-
                 /*!
                  * Retrieves whether the option enabling exact model checking is set.
                  *

src/storm/settings/modules/ResourceSettings.cpp

@@ -13,10 +13,13 @@ namespace storm {
             const std::string ResourceSettings::moduleName = "resources";
             const std::string ResourceSettings::timeoutOptionName = "timeout";
             const std::string ResourceSettings::timeoutOptionShortName = "t";
-            
+            const std::string ResourceSettings::printTimeAndMemoryOptionName = "timemem";
+            const std::string ResourceSettings::printTimeAndMemoryOptionShortName = "tm";
+
             ResourceSettings::ResourceSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, printTimeAndMemoryOptionName, false, "Prints CPU time and memory consumption at the end.").setShortName(printTimeAndMemoryOptionShortName).build());
             }
             
             bool ResourceSettings::isTimeoutSet() const {
@@ -27,6 +30,10 @@ namespace storm {
                 return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger();
             }
             
+            bool ResourceSettings::isPrintTimeAndMemorySet() const {
+                return this->getOption(printTimeAndMemoryOptionName).getHasOptionBeenSet();
+            }
+
         }
     }
 }

src/storm/settings/modules/ResourceSettings.h

@@ -18,6 +18,13 @@ namespace storm {
                  */
                 ResourceSettings();
 
+                /*!
+                 * Retrieves whether time and memory consumption shall be printed at the end of a run.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isPrintTimeAndMemorySet() const;
+                
                 /*!
                  * Retrieves whether the timeout option was set.
                  *
@@ -39,6 +46,8 @@ namespace storm {
                 // Define the string names of the options as constants.
                 static const std::string timeoutOptionName;
                 static const std::string timeoutOptionShortName;
+                static const std::string printTimeAndMemoryOptionName;
+                static const std::string printTimeAndMemoryOptionShortName;
             };
         }
     }

src/storm/storm.cpp

@@ -6,7 +6,7 @@
 #include "storm/utility/initialize.h"
 
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/ResourceSettings.h"
 
 /*!
  * Main entry point of the executable storm.
@@ -30,7 +30,7 @@ int main(const int argc, const char** argv) {
         storm::utility::cleanUp();
         auto end = std::chrono::high_resolution_clock::now();
 
-        if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPrintTimeAndMemorySet()) {
+        if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
             storm::cli::showTimeAndMemoryStatistics(std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count());
         }
         return 0;

src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@@ -243,7 +243,9 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) {
     EXPECT_EQ(0ull, scheduler2.getChoice(3));
 }
 
-TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) {
+// Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is
+// currently not implemented and also not supported by PRISM.
+TEST(DISABLED_GmmxxMdpPrctlModelCheckerTest, TinyRewards) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm");
 
     // A parser that we use for conveniently constructing the formulas.
@@ -271,5 +273,4 @@ TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) {
     EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    
 }