diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 6fbb8cb00..dbd5c1994 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -502,7 +502,7 @@ namespace storm { // If the current state does not have a single choice, we equip it with a self-loop if that was // requested and issue an error otherwise. if (totalNumberOfChoices == 0) { - if (storm::settings::generalSettings().isFixDeadlocksSet()) { + if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) { // Insert empty choice labeling for added self-loop transitions. choiceLabels.push_back(boost::container::flat_set()); transitionMatrixBuilder.addNextValue(currentRow, currentState, storm::utility::constantOne()); diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 43c26f8fb..5a8057f13 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -93,7 +93,7 @@ namespace storm { uint_fast64_t row, col, lastRow = 0; double val; - bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::generalSettings().isDontFixDeadlocksSet(); bool hadDeadlocks = false; bool rowHadDiagonalEntry = false; @@ -122,7 +122,7 @@ namespace storm { if (row > 0) { for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { hadDeadlocks = true; - if (fixDeadlocks) { + if (!dontFixDeadlocks) { resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); } else { @@ -154,7 +154,7 @@ namespace storm { } for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; - if (fixDeadlocks) { + if (!dontFixDeadlocks) { resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); } else { @@ -194,7 +194,7 @@ namespace storm { } // If we encountered deadlock and did not fix them, now is the time to throw the exception. - if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; + if (dontFixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the states do not have outgoing transitions."; } // Finally, build the actual matrix, test and return it. diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index e001d2b1d..a943cfaae 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -15,7 +15,7 @@ namespace storm { MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char const* buf) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; - bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::generalSettings().isDontFixDeadlocksSet(); // Skip the format hint if it is there. buf = trimWhitespaces(buf); @@ -42,7 +42,7 @@ namespace storm { // If we have skipped some states, we need to reserve the space for the self-loop insertion in the second pass. if (source > lastsource + 1) { - if (fixDeadlocks) { + if (!dontFixDeadlocks) { result.numberOfNonzeroEntries += source - lastsource - 1; result.numberOfChoices += source - lastsource - 1; } else { @@ -157,7 +157,7 @@ namespace storm { MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char const* buf, FirstPassResult const& firstPassResult) { Result result(firstPassResult); - bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::generalSettings().isDontFixDeadlocksSet(); // Skip the format hint if it is there. buf = trimWhitespaces(buf); @@ -181,7 +181,7 @@ namespace storm { // If we have skipped some states, we need to insert self-loops if requested. if (source > lastsource + 1) { - if (fixDeadlocks) { + if (!dontFixDeadlocks) { for (uint_fast64_t index = lastsource + 1; index < source; ++index) { result.transitionMatrixBuilder.newRowGroup(currentChoice); result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1); diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 971f7cdfe..c31552561 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -100,7 +100,7 @@ namespace storm { // Initialize variables for the parsing run. uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0; double val = 0.0; - bool fixDeadlocks = storm::settings::generalSettings().isFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::generalSettings().isDontFixDeadlocksSet(); bool hadDeadlocks = false; // The first state already starts a new row group of the matrix. @@ -145,7 +145,7 @@ namespace storm { // Also begin a new rowGroup for the skipped state. for (uint_fast64_t node = lastSource + 1; node < source; node++) { hadDeadlocks = true; - if (fixDeadlocks) { + if (!dontFixDeadlocks) { matrixBuilder.newRowGroup(curRow); matrixBuilder.addNextValue(curRow, node, 1); ++curRow; @@ -174,7 +174,7 @@ namespace storm { buf = trimWhitespaces(buf); } - if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; + if (dontFixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the states do not have outgoing transitions."; // Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices. if(isRewardFile) { diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 822fa73d6..1675f1f48 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -27,8 +27,8 @@ namespace storm { const std::string GeneralSettings::transitionRewardsOptionName = "transrew"; const std::string GeneralSettings::stateRewardsOptionName = "staterew"; const std::string GeneralSettings::counterexampleOptionName = "counterexample"; - const std::string GeneralSettings::fixDeadlockOptionName = "fixDeadlocks"; - const std::string GeneralSettings::fixDeadlockOptionShortName = "fix"; + const std::string GeneralSettings::dontFixDeadlockOptionName = "nofixdl"; + const std::string GeneralSettings::dontFixDeadlockOptionShortName = "ndl"; const std::string GeneralSettings::timeoutOptionName = "timeout"; const std::string GeneralSettings::timeoutOptionShortName = "t"; const std::string GeneralSettings::eqSolverOptionName = "eqsolver"; @@ -66,7 +66,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, fixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(fixDeadlockOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); std::vector linearEquationSolver = {"gmm++", "native"}; this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") @@ -184,12 +184,12 @@ namespace storm { return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString(); } - bool GeneralSettings::isFixDeadlocksSet() const { - return this->getOption(fixDeadlockOptionName).getHasOptionBeenSet(); + bool GeneralSettings::isDontFixDeadlocksSet() const { + return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); } - std::unique_ptr GeneralSettings::overrideFixDeadlocksSet(bool stateToSet) { - return this->overrideOption(fixDeadlockOptionName, stateToSet); + std::unique_ptr GeneralSettings::overrideDontFixDeadlocksSet(bool stateToSet) { + return this->overrideOption(dontFixDeadlockOptionName, stateToSet); } bool GeneralSettings::isTimeoutSet() const { diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 460e2cdd4..faac6492c 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -208,20 +208,20 @@ namespace storm { std::string getCounterexampleFilename() const; /*! - * Retrieves whether the fix-deadlocks option was set. + * Retrieves whether the dont-fix-deadlocks option was set. * - * @return True if the fix-deadlocks option was set. + * @return True if the dont-fix-deadlocks option was set. */ - bool isFixDeadlocksSet() const; + bool isDontFixDeadlocksSet() const; /*! - * Overrides the option to fix deadlocks by setting it to the specified value. As soon as the returned - * memento goes out of scope, the original value is restored. + * Overrides the option to not fix deadlocks by setting it to the specified value. As soon as the + * returned memento goes out of scope, the original value is restored. * * @param stateToSet The value that is to be set for the fix-deadlocks option. * @return The memento that will eventually restore the original value. */ - std::unique_ptr overrideFixDeadlocksSet(bool stateToSet); + std::unique_ptr overrideDontFixDeadlocksSet(bool stateToSet); /*! * Retrieves whether the timeout option was set. @@ -296,8 +296,8 @@ namespace storm { static const std::string transitionRewardsOptionName; static const std::string stateRewardsOptionName; static const std::string counterexampleOptionName; - static const std::string fixDeadlockOptionName; - static const std::string fixDeadlockOptionShortName; + static const std::string dontFixDeadlockOptionName; + static const std::string dontFixDeadlockOptionShortName; static const std::string timeoutOptionName; static const std::string timeoutOptionShortName; static const std::string eqSolverOptionName; diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index a1caceb80..8bb9fadda 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -8,7 +8,6 @@ #include "src/parser/AutoParser.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { - std::unique_ptr deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); @@ -50,7 +49,6 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { } TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { - std::unique_ptr deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); @@ -85,7 +83,6 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { } TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { - std::unique_ptr deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp index f7e83a01d..90d059309 100644 --- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp @@ -190,9 +190,8 @@ TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) { } TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { - // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); + std::unique_ptr fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"); @@ -217,7 +216,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException); } diff --git a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp index 26869fbcd..890d709d0 100644 --- a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -186,7 +186,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) { TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); + std::unique_ptr fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false); // Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works. storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"); @@ -205,7 +205,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"), storm::exceptions::WrongFormatException); } diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp index b7323f363..db14e78cd 100644 --- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -208,7 +208,7 @@ TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) { TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); + std::unique_ptr fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra")); @@ -249,7 +249,7 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException); } diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 8534fc827..403e61db1 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -7,7 +7,6 @@ #include "src/parser/AutoParser.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { - std::unique_ptr deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); @@ -49,7 +48,6 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { - std::unique_ptr deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true); std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);