Switched from an option to fix deadlocks to an option to not fix the deadlocks. Hence, deadlocks are now fixed by default unless otherwise requested.

Former-commit-id: 9434215807

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<uint_fast64_t>());
                             transitionMatrixBuilder.addNextValue(currentRow, currentState, storm::utility::constantOne<ValueType>());

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<double>());
                                 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<double>());
 									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.

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

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

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<std::string> 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<storm::settings::SettingMemento> GeneralSettings::overrideFixDeadlocksSet(bool stateToSet) {
-                return this->overrideOption(fixDeadlockOptionName, stateToSet);
+            std::unique_ptr<storm::settings::SettingMemento> GeneralSettings::overrideDontFixDeadlocksSet(bool stateToSet) {
+                return this->overrideOption(dontFixDeadlockOptionName, stateToSet);
             }
             
             bool GeneralSettings::isTimeoutSet() const {

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<storm::settings::SettingMemento> overrideFixDeadlocksSet(bool stateToSet);
+                std::unique_ptr<storm::settings::SettingMemento> 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;

test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp

@@ -8,7 +8,6 @@
 #include "src/parser/AutoParser.h"
 
 TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
-    std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
 	std::shared_ptr<storm::models::AbstractModel<double>> 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<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
 	std::shared_ptr<storm::models::AbstractModel<double>> 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<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
 	std::shared_ptr<storm::models::AbstractModel<double>> 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);

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<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
+    std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false);
 
 	// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
 	storm::storage::SparseMatrix<double> 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<storm::settings::SettingMemento> unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
+    std::unique_ptr<storm::settings::SettingMemento> 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);
 }

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<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
+    std::unique_ptr<storm::settings::SettingMemento> 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<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
+    std::unique_ptr<storm::settings::SettingMemento> 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);
 }

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<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
+    std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false);
 
 	// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
 	storm::storage::SparseMatrix<double> 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<storm::settings::SettingMemento> unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
+    std::unique_ptr<storm::settings::SettingMemento> 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);
 }

test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp

@@ -7,7 +7,6 @@
 #include "src/parser/AutoParser.h"
 
 TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
-    std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
 	std::shared_ptr<storm::models::AbstractModel<double>> 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<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
 	std::shared_ptr<storm::models::AbstractModel<double>> 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);