From b1dc6fec060eba288f5e9c23d1f6443df6724756 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Feb 2020 15:11:38 +0100 Subject: [PATCH] Accelerated zeno check for MAs. Also only apply zeno check if --additional-checks is set. --- src/storm-cli-utilities/model-handling.h | 7 ++++--- src/storm/models/sparse/MarkovAutomaton.cpp | 5 ++--- src/storm/settings/modules/DebugSettings.cpp | 6 ++++++ src/storm/settings/modules/DebugSettings.h | 8 ++++++++ 4 files changed, 20 insertions(+), 6 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index dd0e2d586..cd57360ef 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -455,11 +455,12 @@ namespace storm { template std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { auto transformationSettings = storm::settings::getModule(); - + auto debugSettings = storm::settings::getModule(); + std::shared_ptr> 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(); diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 6e7070546..bea9278c5 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -282,9 +282,8 @@ namespace storm { if (isClosed() && markovianStates.empty()) { return true; } - - storm::storage::MaximalEndComponentDecomposition 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(); } diff --git a/src/storm/settings/modules/DebugSettings.cpp b/src/storm/settings/modules/DebugSettings.cpp index 38eb4fe7c..d117958ca 100644 --- a/src/storm/settings/modules/DebugSettings.cpp +++ b/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(); } diff --git a/src/storm/settings/modules/DebugSettings.h b/src/storm/settings/modules/DebugSettings.h index 4364b7bc7..8330e8c95 100644 --- a/src/storm/settings/modules/DebugSettings.h +++ b/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;