Accelerated zeno check for MAs. Also only apply zeno check if --additional-checks is set.

src/storm-cli-utilities/model-handling.h

@@ -455,11 +455,12 @@ namespace storm {
         template <typename ValueType>
         std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseMarkovAutomaton(std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const& model) {
             auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
-
+            auto debugSettings = storm::settings::getModule<storm::settings::modules::DebugSettings>();
+            
             std::shared_ptr<storm::models::sparse::Model<ValueType>> result = model;
             model->close();
-            STORM_LOG_WARN_COND(!model->containsZenoCycle(), "MA contains a Zeno cycle. Model checking results cannot be trusted.");
-
+            STORM_LOG_WARN_COND(!debugSettings.isAdditionalChecksSet() || !model->containsZenoCycle(), "MA contains a Zeno cycle. Model checking results cannot be trusted.");
+            
             if (model->isConvertibleToCtmc()) {
                 STORM_LOG_WARN_COND(false, "MA is convertible to a CTMC, consider using a CTMC instead.");
                 result = model->convertToCtmc();

src/storm/models/sparse/MarkovAutomaton.cpp

@@ -282,9 +282,8 @@ namespace storm {
                 if (isClosed() && markovianStates.empty()) {
                     return true;
                 }
-
-                storm::storage::MaximalEndComponentDecomposition<ValueType> maxEnd(this->getTransitionMatrix(), this->getBackwardTransitions(),~markovianStates);
-                return !maxEnd.empty();
+                storm::storage::BitVector statesWithZenoCycle = storm::utility::graph::performProb0E(*this, this->getBackwardTransitions(), ~markovianStates, markovianStates);
+                return !statesWithZenoCycle.empty();
             }
 
 

src/storm/settings/modules/DebugSettings.cpp

@@ -13,6 +13,7 @@ namespace storm {
             const std::string DebugSettings::moduleName = "debug";
             const std::string DebugSettings::debugOptionName = "debug";
             const std::string DebugSettings::traceOptionName = "trace";
+            const std::string DebugSettings::additionalChecksOptionName = "additional-checks";
             const std::string DebugSettings::logfileOptionName = "logfile";
             const std::string DebugSettings::logfileOptionShortName = "l";
             const std::string DebugSettings::testOptionName = "test";
@@ -20,6 +21,7 @@ namespace storm {
             DebugSettings::DebugSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, additionalChecksOptionName, false, "If set, additional sanity checks are performed during execution.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, testOptionName, false, "Activate a test setting.").setIsAdvanced().build());
@@ -33,6 +35,10 @@ namespace storm {
                 return this->getOption(traceOptionName).getHasOptionBeenSet();
             }
             
+            bool DebugSettings::isAdditionalChecksSet() const {
+                return this->getOption(additionalChecksOptionName).getHasOptionBeenSet();
+            }
+            
             bool DebugSettings::isLogfileSet() const {
                 return this->getOption(logfileOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/DebugSettings.h

@@ -31,6 +31,13 @@ namespace storm {
                  */
                 bool isTraceSet() const;
                 
+                /*!
+                 * Retrieves whether additional checks on the input should be performed.
+                 *
+                 * @return True iff additoinal checks on the input should be performed.
+                 */
+                bool isAdditionalChecksSet() const;
+                
                 /*!
                  * Retrieves whether the logfile option was set.
                  *
@@ -60,6 +67,7 @@ namespace storm {
                 // Define the string names of the options as constants.
                 static const std::string debugOptionName;
                 static const std::string traceOptionName;
+                static const std::string additionalChecksOptionName;
                 static const std::string logfileOptionName;
                 static const std::string logfileOptionShortName;
                 static const std::string testOptionName;