Beautified output of option system. Enabled command line interface of counterexample generation.

Former-commit-id: cecc5e85b3

CMakeLists.txt

@@ -348,9 +348,9 @@ target_link_libraries(storm-performance-tests ltl2dstar)
 if (ENABLE_GUROBI)
     message (STATUS "StoRM - Linking with Gurobi")
 	include_directories("${GUROBI_ROOT}/include")
-    target_link_libraries(storm "gurobi55")
-    target_link_libraries(storm-functional-tests "gurobi55")
-    target_link_libraries(storm-performance-tests "gurobi55")
+    target_link_libraries(storm "gurobi56")
+    target_link_libraries(storm-functional-tests "gurobi56")
+    target_link_libraries(storm-performance-tests "gurobi56")
 endif(ENABLE_GUROBI)
 
 #############################################################

src/counterexamples/MILPMinimalLabelSetGenerator.cpp

@@ -0,0 +1,9 @@
+#include "src/settings/Settings.h"
+
+bool MILPMinimalLabelSetGeneratorOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool {
+    std::vector<std::string> techniques;
+    techniques.push_back("sat");
+    techniques.push_back("milp");
+	instance->addOption(storm::settings::OptionBuilder("MILPMinimalLabelSetGenerator", "mincmd", "", "Computes a counterexample for the given symbolic model in terms of a minimal command set.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("propertyFile", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Must be either \"milp\" or \"sat\".").setDefaultValueString("sat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());
+	return true;
+});

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -104,10 +104,10 @@ namespace storm {
                 result.problematicStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates);
                 result.problematicStates.complement();
                 result.problematicStates &= result.relevantStates;
-                LOG4CPLUS_DEBUG(logger, "Found " << phiStates.getNumberOfSetBits() << " filter states (" << phiStates.toString() << ").");
-                LOG4CPLUS_DEBUG(logger, "Found " << psiStates.getNumberOfSetBits() << " target states (" << psiStates.toString() << ").");
-                LOG4CPLUS_DEBUG(logger, "Found " << result.relevantStates.getNumberOfSetBits() << " relevant states (" << result.relevantStates.toString() << ").");
-                LOG4CPLUS_DEBUG(logger, "Found " << result.problematicStates.getNumberOfSetBits() << " problematic states (" << result.problematicStates.toString() << ").");
+                LOG4CPLUS_DEBUG(logger, "Found " << phiStates.getNumberOfSetBits() << " filter states.");
+                LOG4CPLUS_DEBUG(logger, "Found " << psiStates.getNumberOfSetBits() << " target states.");
+                LOG4CPLUS_DEBUG(logger, "Found " << result.relevantStates.getNumberOfSetBits() << " relevant states .");
+                LOG4CPLUS_DEBUG(logger, "Found " << result.problematicStates.getNumberOfSetBits() << " problematic states.");
                 return result;
             }
             
@@ -162,6 +162,11 @@ namespace storm {
                     }
                 }
                 LOG4CPLUS_DEBUG(logger, "Found " << result.allRelevantLabels.size() << " relevant labels.");
+
+                // Finally, determine the set of labels that are known to be taken.
+                result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, result.allRelevantLabels);
+                LOG4CPLUS_DEBUG(logger, "Found " << result.knownLabels.size() << " known labels.");
+
                 return result;
             }
             
@@ -171,7 +176,9 @@ namespace storm {
              * @param env The Gurobi environment to modify.
              */
             static void setGurobiEnvironmentProperties(GRBenv* env) {
-                int error = error = GRBsetintparam(env, "OutputFlag", storm::settings::Settings::getInstance()->isSet("debug") ? 1 : 0);
+                // Enable the following line to only print the output of Gurobi if the debug flag is set.
+                // int error = error = GRBsetintparam(env, "OutputFlag", storm::settings::Settings::getInstance()->isSet("debug") ? 1 : 0);
+                int error = error = GRBsetintparam(env, "OutputFlag", 1);
             }
             
             /*!
@@ -869,7 +876,6 @@ namespace storm {
                 uint_fast64_t numberOfConstraintsCreated = 0;
                 int error = 0;
 
-                choiceInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, choiceInformation.allRelevantLabels);
                 for (auto label : choiceInformation.knownLabels) {
                     double coefficient = 1;
                     int variableIndex = variableInformation.labelToVariableIndexMap.at(label);
@@ -964,6 +970,7 @@ namespace storm {
                     }
                     
                     for (auto predecessor : predecessors) {
+                        // If the predecessor is not a relevant state, we need to skip it.
                         if (!stateInformation.relevantStates.get(predecessor)) {
                             continue;
                         }
@@ -1003,7 +1010,7 @@ namespace storm {
                     }
                     ++numberOfConstraintsCreated;
                 }
-
+                
                 // Assert that at least one initial state selects at least one action.
                 variables.clear();
                 coefficients.clear();
@@ -1034,6 +1041,11 @@ namespace storm {
                 }
                 
                 for (auto predecessor : predecessors) {
+                    // If the predecessor is not a relevant state, we need to skip it.
+                    if (!stateInformation.relevantStates.get(predecessor)) {
+                        continue;
+                    }
+                    
                     std::list<uint_fast64_t>::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(predecessor).begin();
                     for (auto relevantChoice : choiceInformation.relevantChoicesForRelevantStates.at(predecessor)) {
                         bool choiceTargetsPsiState = false;
@@ -1246,8 +1258,6 @@ namespace storm {
             
             static std::set<uint_fast64_t> getMinimalLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) {
 #ifdef STORM_HAVE_GUROBI
-                auto startTime = std::chrono::high_resolution_clock::now();
-
                 // (0) Check whether the MDP is indeed labeled.
                 if (!labeledMdp.hasChoiceLabels()) {
                     throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model.";
@@ -1298,9 +1308,6 @@ namespace storm {
                 // Display achieved probability.
                 std::pair<uint_fast64_t, double> initialStateProbabilityPair = getReachabilityProbability(environmentModelPair.first, environmentModelPair.second, labeledMdp, variableInformation);
 
-                auto endTime = std::chrono::high_resolution_clock::now();
-                std::cout << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
-                
                 // (4.6) Shutdown Gurobi.
                 destroyGurobiModelAndEnvironment(environmentModelPair.first, environmentModelPair.second);
                 
@@ -1311,6 +1318,65 @@ namespace storm {
 #endif
             }
             
+            /*!
+             * Computes a (minimally labeled) counterexample for the given model and (safety) formula. If the model satisfies the property, an exception is thrown.
+             *
+             * @param labeledMdp A labeled MDP that is the model in which to generate the counterexample.
+             * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested
+             * formula can be either an unbounded until formula or an eventually formula.
+             */
+            static void computeCounterexample(storm::models::Mdp<T> const& labeledMdp, storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
+#ifdef STORM_HAVE_GUROBI
+                std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl;
+                // First, we need to check whether the current formula is an Until-Formula.
+                storm::property::prctl::ProbabilisticBoundOperator<double> const* probBoundFormula = dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<double> const*>(formulaPtr);
+                if (probBoundFormula == nullptr) {
+                    LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.");
+                    throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.";
+                }
+                if (probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS) {
+                    LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only strict upper bounds are supported for counterexample generation.");
+                    throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only strict upper bounds are supported for counterexample generation.";
+                }
+
+                // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
+                double bound = probBoundFormula->getBound();
+                storm::property::prctl::AbstractPathFormula<double> const& pathFormula = probBoundFormula->getPathFormula();
+                storm::storage::BitVector phiStates;
+                storm::storage::BitVector psiStates;
+                storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
+                try {
+                    storm::property::prctl::Until<double> const& untilFormula = dynamic_cast<storm::property::prctl::Until<double> const&>(pathFormula);
+                    
+                    phiStates = untilFormula.getLeft().check(modelchecker);
+                    psiStates = untilFormula.getRight().check(modelchecker);
+                } catch (std::bad_cast const& e) {
+                    // If the nested formula was not an until formula, it remains to check whether it's an eventually formula.
+                    try {
+                        storm::property::prctl::Eventually<double> const& eventuallyFormula = dynamic_cast<storm::property::prctl::Eventually<double> const&>(pathFormula);
+                        
+                        phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
+                        psiStates = eventuallyFormula.getChild().check(modelchecker);
+                    } catch (std::bad_cast const& e) {
+                        // If the nested formula is neither an until nor a finally formula, we throw an exception.
+                        throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
+                    }
+                }
+                
+                // Delegate the actual computation work to the function of equal name.
+                auto startTime = std::chrono::high_resolution_clock::now();
+                std::set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, true, true);
+                auto endTime = std::chrono::high_resolution_clock::now();
+                std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
+
+                std::cout << std::endl << "-------------------------------------------" << std::endl;
+                
+                // FIXME: Return the DTMC that results from applying the max scheduler in the MDP restricted to the computed label set.
+#else
+                throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Gurobi.";
+#endif
+            }
+            
         };
         
     } // namespace counterexamples

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1165,11 +1165,60 @@ namespace storm {
                 // (9) Return the resulting command set after undefining the constants.
                 storm::utility::ir::undefineUndefinedConstants(program);
                 
-                endTime = std::chrono::high_resolution_clock::now();
-                std::cout << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms (" << iterations << " iterations)." << std::endl;
-                
                 return commandSet;
                 
+#else
+                throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Z3.";
+#endif
+            }
+            
+            static void computeCounterexample(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp,  storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
+#ifdef STORM_HAVE_Z3
+                std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl;
+                // First, we need to check whether the current formula is an Until-Formula.
+                storm::property::prctl::ProbabilisticBoundOperator<double> const* probBoundFormula = dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<double> const*>(formulaPtr);
+                if (probBoundFormula == nullptr) {
+                    LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.");
+                    throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.";
+                }
+                if (probBoundFormula->getComparisonOperator() != storm::property::ComparisonType::LESS) {
+                    LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only strict upper bounds are supported for counterexample generation.");
+                    throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only strict upper bounds are supported for counterexample generation.";
+                }
+                
+                // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
+                double bound = probBoundFormula->getBound();
+                storm::property::prctl::AbstractPathFormula<double> const& pathFormula = probBoundFormula->getPathFormula();
+                storm::storage::BitVector phiStates;
+                storm::storage::BitVector psiStates;
+                storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
+                try {
+                    storm::property::prctl::Until<double> const& untilFormula = dynamic_cast<storm::property::prctl::Until<double> const&>(pathFormula);
+                    
+                    phiStates = untilFormula.getLeft().check(modelchecker);
+                    psiStates = untilFormula.getRight().check(modelchecker);
+                } catch (std::bad_cast const& e) {
+                    // If the nested formula was not an until formula, it remains to check whether it's an eventually formula.
+                    try {
+                        storm::property::prctl::Eventually<double> const& eventuallyFormula = dynamic_cast<storm::property::prctl::Eventually<double> const&>(pathFormula);
+                        
+                        phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
+                        psiStates = eventuallyFormula.getChild().check(modelchecker);
+                    } catch (std::bad_cast const& e) {
+                        // If the nested formula is neither an until nor a finally formula, we throw an exception.
+                        throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
+                    }
+                }
+                
+                // Delegate the actual computation work to the function of equal name.
+                auto startTime = std::chrono::high_resolution_clock::now();
+                std::set<uint_fast64_t> usedLabelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, true);
+                auto endTime = std::chrono::high_resolution_clock::now();
+                std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
+                
+                std::cout << std::endl << "-------------------------------------------" << std::endl;
+                
+                // FIXME: Return the DTMC that results from applying the max scheduler in the MDP restricted to the computed label set.
 #else
                 throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Z3.";
 #endif

src/settings/ArgumentBuilder.h

@@ -79,12 +79,12 @@ namespace storm {
 #define PPCAT(A, B) PPCAT_NX(A, B)
 #define MACROaddValidationFunction(funcName, funcType) 	ArgumentBuilder& PPCAT(addValidationFunction, funcName) (storm::settings::Argument< funcType >::userValidationFunction_t userValidationFunction) { \
 				if (this->argumentType != ArgumentType::funcName) { \
-					throw storm::exceptions::IllegalFunctionCallException() << "Tried adding a Validation-Function for a \"" << ArgumentTypeHelper::toString(ArgumentType::funcName) << "\" Argument, but this Argument is configured to be of Type \"" << ArgumentTypeHelper::toString(this->argumentType) << "\"."; \
+					throw storm::exceptions::IllegalFunctionCallException() << "Unable to add a validation function for a \"" << ArgumentTypeHelper::toString(ArgumentType::funcName) << "\" argument, because this argument is of type \"" << ArgumentTypeHelper::toString(this->argumentType) << "\"."; \
 				} \
 				( PPCAT(this->userValidationFunction_, funcName) ).push_back(userValidationFunction); \
 				std::string errorMessageTarget = ""; \
 				if (this->hasDefaultValue && !this->validateDefaultForEach(errorMessageTarget)) { \
-					throw storm::exceptions::IllegalArgumentValueException() << "Tried adding a Validation-Function for an Argument which has a Default Value set which is rejected by this Validation-Function:\r\n" << errorMessageTarget; \
+					throw storm::exceptions::IllegalArgumentValueException() << "Unable to add a validation function for an argument that has a default value which is rejected by this validation function:\r\n" << errorMessageTarget << "."; \
 				} \
 				return *this; \
 			}
@@ -98,12 +98,12 @@ namespace storm {
 
 #define MACROsetDefaultValue(funcName, funcType) ArgumentBuilder& PPCAT(setDefaultValue, funcName) (funcType const& defaultValue) { \
 				if (this->argumentType != ArgumentType::funcName) { \
-					throw storm::exceptions::IllegalFunctionCallException() << "Tried adding a default Value for a \"" << ArgumentTypeHelper::toString(ArgumentType::String) << "\" Argument, but the Argument \"" << this->argumentName << "\" is configured to be of Type \"" << ArgumentTypeHelper::toString(this->argumentType) << "\"."; \
+					throw storm::exceptions::IllegalFunctionCallException() << "Unable to add a default value for a \"" << ArgumentTypeHelper::toString(ArgumentType::String) << "\" argument, because the argument \"" << this->argumentName << "\" is of type \"" << ArgumentTypeHelper::toString(this->argumentType) << "\"."; \
 				} \
 				PPCAT(this->defaultValue_, funcName) = defaultValue; \
 				std::string errorMessageTarget = ""; \
 				if (!this->validateDefaultForEach(errorMessageTarget)) { \
-					throw storm::exceptions::IllegalArgumentValueException() << "Tried adding a default Value for the Argument \"" << this->argumentName << "\", but a Validation Function rejected it:\r\n" << errorMessageTarget; \
+					throw storm::exceptions::IllegalArgumentValueException() << "Unable to add a default value for the argument \"" << this->argumentName << "\", but a validation function rejected it:\r\n" << errorMessageTarget << "."; \
 				} \
 				this->hasDefaultValue = true; \
 				return *this; \
@@ -117,7 +117,7 @@ namespace storm {
 
 			ArgumentBase* build() {
 				if (this->hasBeenBuild) {
-					throw storm::exceptions::IllegalFunctionCallException() << "Called build() on an instance of ArgumentBuilder which has already build an Instance.";
+					throw storm::exceptions::IllegalFunctionCallException() << "Called build() on an instance of ArgumentBuilder that has already built an instance.";
 				}	
 				this->hasBeenBuild = true;
 				switch (this->argumentType) {
@@ -246,7 +246,7 @@ namespace storm {
 						}
 						break;
 					default: {
-						throw storm::exceptions::InternalTypeErrorException() << "Error: Missing Case in ArgumentBuilder's switch/case Code.";
+						throw storm::exceptions::InternalTypeErrorException() << "Missing case in ArgumentBuilder.";
 					}
 				}
 				

src/settings/ArgumentType.h

@@ -43,8 +43,8 @@ namespace storm {
 					return argumentTypeBoolean;
 					break;
 				default: {
-					LOG4CPLUS_ERROR(logger, "ArgumentTypeHelper::toString: Missing Case in ArgumentTypeHelper's switch/case Code.");
-					throw storm::exceptions::InternalTypeErrorException() << "Missing a Switch Case in the ArgumentTypeHelper!\n" << "It seems there is a new ArgumentType, but it was not added to the Helper Class!";
+					LOG4CPLUS_ERROR(logger, "ArgumentTypeHelper::toString: Missing case in ArgumentTypeHelper.");
+					throw storm::exceptions::InternalTypeErrorException() << "Missing case in ArgumentTypeHelper.";
 					}
 				}
 			}

src/settings/ArgumentTypeInferationHelper.h

@@ -45,8 +45,8 @@ namespace storm {
 		template <typename T> 
 		ArgumentType ArgumentTypeInferation::inferToEnumType() {
 			// "Missing Template Specialization Case in ArgumentTypeInferation"
-			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToEnumType: Missing a Template Specialization Case in the ArgumentTypeInferationHelper! It seems you tried to use a new, non-standard Type as a Settings Parameter-Type!");
-			throw storm::exceptions::InternalTypeErrorException() << "Missing a Template Specialization Case in the ArgumentTypeInferationHelper!\n" << "It seems you tried to use a new, non-standard Type as a Settings Parameter-Type!";
+			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToEnumType: Missing a template specialization case in the ArgumentTypeInferationHelper.");
+			throw storm::exceptions::InternalTypeErrorException() << "Missing a template specialization case in the ArgumentTypeInferationHelper.";
 
 			return ArgumentType::Invalid;
 		}
@@ -72,16 +72,16 @@ namespace storm {
 		 */
 		template <typename T> 
 		std::string ArgumentTypeInferation::inferToString(ArgumentType argumentType, T value) {
-			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToString: inferToString was called on a non-string Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-			throw storm::exceptions::InternalTypeErrorException() << "inferToString was called on a non-string Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToString: Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+			throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 
 			return std::string();
 		}
 
 		template <> inline std::string ArgumentTypeInferation::inferToString<std::string>(ArgumentType argumentType, std::string value) {
 			if (argumentType != ArgumentType::String) {
-				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToString: inferToString was called on a string Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-				throw storm::exceptions::InternalTypeErrorException() << "inferToString was called on a string Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToString: Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
+				throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToString on a non-string template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
 			}
 			return value;
 		}
@@ -91,16 +91,16 @@ namespace storm {
 		 */
 		template <typename T> 
 		int_fast64_t ArgumentTypeInferation::inferToInteger(ArgumentType argumentType, T value) {
-			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToInteger: inferToInteger was called on a non-int_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-			throw storm::exceptions::InternalTypeErrorException() << "inferToInteger was called on a non-int_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToInteger: Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+			throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 
 			return 0;
 		}
 
 		template <> inline int_fast64_t ArgumentTypeInferation::inferToInteger<int_fast64_t>(ArgumentType argumentType, int_fast64_t value) {
 			if (argumentType != ArgumentType::Integer) {
-				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToInteger: inferToInteger was called on a int_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-				throw storm::exceptions::InternalTypeErrorException() << "inferToInteger was called on an int_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToInteger: Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
+				throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToInteger on a non-int_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
 			}
 			return value;
 		}
@@ -110,16 +110,16 @@ namespace storm {
 		 */
 		template <typename T> 
 		uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType argumentType, T value) {
-			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToUnsignedInteger: inferToUnsignedInteger was called on a non-uint_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-			throw storm::exceptions::InternalTypeErrorException() << "inferToUnsignedInteger was called on a non-uint_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToUnsignedInteger: Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+			throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 
 			return 0;
 		}
 
 		template <> inline uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<uint_fast64_t>(ArgumentType argumentType, uint_fast64_t value) {
 			if (argumentType != ArgumentType::UnsignedInteger) {
-				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToUnsignedInteger: inferToUnsignedInteger was called on a uint_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-				throw storm::exceptions::InternalTypeErrorException() << "inferToUnsignedInteger was called on an uint_fast64_t Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToUnsignedInteger: Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+				throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToUnsignedInteger on a non-uint_fast64_t template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 			}
 			return value;
 		}
@@ -129,16 +129,16 @@ namespace storm {
 		 */
 		template <typename T> 
 		double ArgumentTypeInferation::inferToDouble(ArgumentType argumentType, T value) {
-			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToDouble: inferToDouble was called on a non-double Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-			throw storm::exceptions::InternalTypeErrorException() << "inferToDouble was called on a non-double Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToDouble: Unable to perform inferToDouble on a non-double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+			throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToDouble on a non-double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 
 			return 0.0;
 		}
 
 		template <> inline double ArgumentTypeInferation::inferToDouble<double>(ArgumentType argumentType, double value) {
 			if (argumentType != ArgumentType::Double) {
-				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToDouble: inferToDouble was called on a double Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-				throw storm::exceptions::InternalTypeErrorException() << "inferToDouble was called on a double Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToDouble: Unable to perform inferToDouble on a double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+				throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToDouble on a double template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 			}
 			return value;
 		}
@@ -148,16 +148,16 @@ namespace storm {
 		 */
 		template <typename T> 
 		bool ArgumentTypeInferation::inferToBoolean(ArgumentType argumentType, T value) {
-			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToBoolean: inferToBoolean was called on a non-bool Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-			throw storm::exceptions::InternalTypeErrorException() << "inferToBoolean was called on a non-bool Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+			LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToBoolean: Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+			throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 
 			return false;
 		}
 
 		template <> inline bool ArgumentTypeInferation::inferToBoolean<bool>(ArgumentType argumentType, bool value) {
 			if (argumentType != ArgumentType::Boolean) {
-				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToBoolean: inferToBoolean was called on a bool Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!");
-				throw storm::exceptions::InternalTypeErrorException() << "inferToBoolean was called on a bool Template Object to cast to " << ArgumentTypeHelper::toString(argumentType) << "!";
+				LOG4CPLUS_ERROR(logger, "ArgumentTypeInferation::inferToBoolean: Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".");
+				throw storm::exceptions::InternalTypeErrorException() << "Unable to perform inferToBoolean on a non-bool template object to cast to " << ArgumentTypeHelper::toString(argumentType) << ".";
 			}
 			return value;
 		}

src/settings/ArgumentValidators.h

@@ -88,12 +88,12 @@ namespace storm {
 					bool upperBoundCondition = (value <= upperBound);
 					if (!lowerBoundCondition) { 
 						std::ostringstream stream;
-						stream << " Lower Bound Condition not met: " << lowerBound << " is not <= " << value;
+						stream << " lower bound condition not met: " << lowerBound << " is not smaller or equal than " << value << ".";
 						errorMessageTarget.append(stream.str());
 					}
 					if (!upperBoundCondition) { 
 						std::ostringstream stream;
-						stream << " Upper Bound Condition not met: " << value << " is not <= " << upperBound; 
+						stream << " upper bound condition not met: " << value << " is not smaller or equal than " << upperBound << ".";
 						errorMessageTarget.append(stream.str());
 					}
 					return (lowerBoundCondition && upperBoundCondition);
@@ -106,12 +106,12 @@ namespace storm {
 					bool upperBoundCondition = (value < upperBound);
 					if (!lowerBoundCondition) { 
 						std::ostringstream stream;
-						stream << " Lower Bound Condition not met: " << lowerBound << " is not < " << value;
+						stream << " lower bound condition not met: " << lowerBound << " is not smaller than " << value << ".";
 						errorMessageTarget.append(stream.str());
 					}
 					if (!upperBoundCondition) { 
 						std::ostringstream stream;
-						stream << " Upper Bound Condition not met: " << value << " is not < " << upperBound; 
+						stream << " upper bound condition not met: " << value << " is not smaller than < " << upperBound << ".";
 						errorMessageTarget.append(stream.str());
 					}
 					return (lowerBoundCondition && upperBoundCondition);

src/settings/Option.h

@@ -84,25 +84,25 @@ namespace storm {
 
 			void unify(Option& other) {
 				if (this->getLongName().compare(other.getLongName()) != 0) {
-					LOG4CPLUS_ERROR(logger, "Option::unify: Could not unify Option \"" << getLongName() << "\" because the Names are different (\"" << getLongName() << "\" vs. \"" << other.getLongName() << "\")!");
-					throw storm::exceptions::OptionUnificationException() << "Could not unify Option \"" << getLongName() << "\" because the Names are different (\"" << getLongName() << "\" vs. \"" << other.getLongName() << "\")!";
+					LOG4CPLUS_ERROR(logger, "Option::unify: Unable to unify option \"" << getLongName() << "\" because of mismatching names (\"" << getLongName() << "\" and \"" << other.getLongName() << "\").");
+					throw storm::exceptions::OptionUnificationException() << "Unable to unify option \"" << getLongName() << "\" because of mismatching names (\"" << getLongName() << "\" and \"" << other.getLongName() << "\").";
 				}
 				if (this->getShortName().compare(other.getShortName()) != 0) {
-					LOG4CPLUS_ERROR(logger, "Option::unify: Could not unify Option \"" << getLongName() << "\" because the Shortnames are different (\"" << getShortName() << "\" vs. \"" << other.getShortName() << "\")!");
-					throw storm::exceptions::OptionUnificationException() << "Could not unify Option \"" << getLongName() << "\" because the Shortnames are different (\"" << getShortName() << "\" vs. \"" << other.getShortName() << "\")!";
+					LOG4CPLUS_ERROR(logger, "Option::unify: Unable to unify option \"" << getLongName() << "\" because of mismatching names (\"" << getShortName() << "\" and \"" << other.getShortName() << "\").");
+					throw storm::exceptions::OptionUnificationException() << "Unable to unify option \"" << getLongName() << "\" because of mismatching names (\"" << getShortName() << "\" and \"" << other.getShortName() << "\").";
 				}
 
 				if (this->getArgumentCount() != other.getArgumentCount()) {
-					LOG4CPLUS_ERROR(logger, "Option::unify: Could not unify Option \"" << getLongName() << "\" because the Argument Counts are different!");
-					throw storm::exceptions::OptionUnificationException() << "Could not unify Option \"" << getLongName() << "\" because the Argument Counts are different!";
+					LOG4CPLUS_ERROR(logger, "Option::unify: Unable to unify option \"" << getLongName() << "\" because of mismatching argument numbers.");
+					throw storm::exceptions::OptionUnificationException() << "Unable to unify option \"" << getLongName() << "\" because of mismatching argument numbers.";
 				}
 				for(size_t i = 0; i != this->arguments.size(); i++) {
 					ArgumentBase* A = this->arguments.at(i).get();
 					ArgumentBase* B = other.arguments.at(i).get();
 
 					if (A->getArgumentType() != B->getArgumentType()) {
-						LOG4CPLUS_ERROR(logger, "Option::unify: Could not unify Option \"" << getLongName() << "\" because the Argument Types at Index " << i << " are different!");
-						throw storm::exceptions::OptionUnificationException() << "Could not unify Option \"" << getLongName() << "\" because the Argument Types at Index " << i << " are different!";
+						LOG4CPLUS_ERROR(logger, "Option::unify: Unable to unify option \"" << getLongName() << "\" because of mismatching argument types at index " << i << ".");
+						throw storm::exceptions::OptionUnificationException() << "Unable to unify option \"" << getLongName() << "\" because of mismatching argument types at index " << i << ".";
 					}
 
 					switch (A->getArgumentType()) {
@@ -123,7 +123,7 @@ namespace storm {
 							break;
 						default:
 							LOG4CPLUS_ERROR(logger, "Option::unify: Missing Case in ArgumentBuilder's switch/case Code.");
-							throw storm::exceptions::InternalTypeErrorException() << "Missing Case in ArgumentBuilder's switch/case Code.";
+							throw storm::exceptions::InternalTypeErrorException() << "Missing case in Option.";
 					}
 				}
 
@@ -139,7 +139,7 @@ namespace storm {
 			ArgumentBase& getArgument(uint_fast64_t argumentIndex) const {
 				if (argumentIndex >= getArgumentCount()) {
 					LOG4CPLUS_ERROR(logger, "Option::getArgument: argumentIndex out of bounds!");
-					throw storm::exceptions::IllegalArgumentException() << "Option::getArgument(): argumentIndex out of bounds!";
+					throw storm::exceptions::IllegalArgumentException() << "Option::getArgument(): index of argument is out of bounds.";
 				}
 				return *this->arguments.at(argumentIndex).get();
 			}
@@ -152,8 +152,8 @@ namespace storm {
 				auto argumentIterator = this->argumentNameMap.find(storm::utility::StringHelper::stringToLower(argumentName));
 
 				if (argumentIterator == this->argumentNameMap.end()) {
-					LOG4CPLUS_ERROR(logger, "Option::getArgumentByName: The Option \"" << this->getLongName() << "\" does not contain an Argument with Name \"" << argumentName << "\"!");
-					throw storm::exceptions::IllegalArgumentException() << "The Option \"" << this->getLongName() << "\" does not contain an Argument with Name \"" << argumentName << "\"!";
+					LOG4CPLUS_ERROR(logger, "Option::getArgumentByName: Unable to retrieve unknown argument \"" << argumentName << "\" of option \"" << this->getLongName() << "\".");
+					throw storm::exceptions::IllegalArgumentException() << "Unable to retrieve unknown argument \"" << argumentName << "\" of option \"" << this->getLongName() << "\".";
 				}
 
 				return *argumentIterator->second.get();
@@ -201,25 +201,25 @@ namespace storm {
 
 			void validateFields() const {
 				if (longName.empty()) {
-					LOG4CPLUS_ERROR(logger, "Option::validateFields: Tried constructing an Option with an empty longName field!");
-					throw storm::exceptions::IllegalArgumentException() << "Tried constructing an Option with an empty longName field!";
+					LOG4CPLUS_ERROR(logger, "Option::validateFields: Unable to construct an option with empty name.");
+					throw storm::exceptions::IllegalArgumentException() << "Unable to construct an option with empty name.";
 				}
 
 				if (moduleName.empty()) {
-					LOG4CPLUS_ERROR(logger, "Option::validateFields: Tried constructing an Option with an empty moduleName field!");
-					throw storm::exceptions::IllegalArgumentException() << "Tried constructing an Option with an empty moduleName field!";
+					LOG4CPLUS_ERROR(logger, "Option::validateFields: Unable to construct an option with empty module.");
+					throw storm::exceptions::IllegalArgumentException() << "Unable to construct an option with empty module.";
 				}
 
 				bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !std::isalpha(c); }) != longName.end();
 				bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !std::isalpha(c); }) != shortName.end();
 
 				if (longNameContainsNonAlpha) {
-					LOG4CPLUS_ERROR(logger, "Option::validateFields: Tried constructing an Option with a longName that contains non-alpha characters!");
-					throw storm::exceptions::IllegalArgumentException() << "Tried constructing an Option with a longName that contains non-alpha characters!";
+					LOG4CPLUS_ERROR(logger, "Option::validateFields: Unable to construct an option with a illegal name.");
+					throw storm::exceptions::IllegalArgumentException() << "Unable to construct an option with a illegal name.";
 				}
 				if (shortNameContainsNonAlpha) {
-					LOG4CPLUS_ERROR(logger, "Option::validateFields: Tried constructing an Option with a shortName that contains non-alpha characters!");
-					throw storm::exceptions::IllegalArgumentException() << "Tried constructing an Option with a shortName that contains non-alpha characters!";
+					LOG4CPLUS_ERROR(logger, "Option::validateFields: Unable to construct an option with a illegal name.");
+					throw storm::exceptions::IllegalArgumentException() << "Unable to construct an option with a illegal name.";
 				}
 			}
 
@@ -234,13 +234,13 @@ namespace storm {
 					//}
 
 					if (!isCurrentArgumentOptional && lastEntryWasOptional) {
-						LOG4CPLUS_ERROR(logger, "Option::isArgumentsVectorValid: The Argument Vector specified for Option \"" << getLongName() << "\" is invalid! It contains a non-optional argument AFTER an optional argument.");
-						throw storm::exceptions::IllegalArgumentException() << "The Argument Vector specified for Option \"" << getLongName() << "\" is invalid! It contains a non-optional argument AFTER an optional argument.";
+						LOG4CPLUS_ERROR(logger, "Option::isArgumentsVectorValid: The argument vector specified for option \"" << getLongName() << "\" is invalid, because it contains a non-optional argument after an optional one.");
+						throw storm::exceptions::IllegalArgumentException() << "The argument vector specified for option \"" << getLongName() << "\" is invalid, because it contains a non-optional argument after an optional one.";
 					}
 					std::string lowerArgumentName = storm::utility::StringHelper::stringToLower(i->get()->getArgumentName());
 					if (argumentNameSet.find(lowerArgumentName) != argumentNameSet.end()) {
-						LOG4CPLUS_ERROR(logger, "Option::isArgumentsVectorValid: The Argument Vector specified for Option \"" << getLongName() << "\" is invalid!\nIt contains two arguments with the same name.");
-						throw storm::exceptions::IllegalArgumentException() << "The Argument Vector specified for Option \"" << getLongName() << "\" is invalid!\nIt contains two arguments with the same name.";
+						LOG4CPLUS_ERROR(logger, "Option::isArgumentsVectorValid: The argument vector specified for option \"" << getLongName() << "\" is invalid, because it contains two arguments with the same name.");
+						throw storm::exceptions::IllegalArgumentException() << "The argument vector specified for option \"" << getLongName() << "\" is invalid, because it contains two arguments with the same name.";
 					}
 					argumentNameSet.insert(lowerArgumentName);
 

src/settings/OptionBuilder.h

@@ -85,24 +85,24 @@ namespace storm {
 				// For automatic management of newArgument's lifetime
 				std::shared_ptr<ArgumentBase> argumentPtr(newArgument);
 				if (this->isBuild) {
-					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Called addArgument() on an instance of OptionBuilder which has already build an Instance.");
-					throw storm::exceptions::IllegalFunctionCallException() << "Called addArgument() on an instance of OptionBuilder which has already build an Instance.";
+					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Illegal call to addArgument() on an instance of OptionBuilder that has already built an instance.");
+					throw storm::exceptions::IllegalFunctionCallException() << "Illegal call to addArgument() on an instance of OptionBuilder that has already built an instance.";
 				}
 
 				if (newArgument->getArgumentType() == ArgumentType::Invalid) {
-					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Could not add Argument to Option \"" << getLongName() << "\" because its Type is Invalid!");
-					throw storm::exceptions::InternalTypeErrorException() << "Could not add Argument to Option \"" << getLongName() << "\" because its Type is Invalid!";
+					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Unable to add argument to option \"" << getLongName() << "\" because its type is invalid.");
+					throw storm::exceptions::InternalTypeErrorException() << "Unable to add argument to option \"" << getLongName() << "\" because its type is invalid.";
 				}
 				
 				if (!newArgument->getIsOptional() && (this->arguments.size() > 0) && (this->arguments.at(this->arguments.size() - 1).get()->getIsOptional())) {
-					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Could not add Non-Optional Argument to Option \"" << getLongName() << "\" because it already contains an optional argument! Please note that after an optional argument has been added only arguments which are also optional can be appended.");
-					throw storm::exceptions::IllegalArgumentException() << "Could not add Non-Optional Argument to Option \"" << getLongName() << "\" because it already contains an optional argument! Please note that after an optional argument has been added only arguments which are also optional can be appended.";
+					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Unable to add a non-optional argument to option \"" << getLongName() << "\", because it already contains an optional argument.");
+					throw storm::exceptions::IllegalArgumentException() << "Unable to add non-optional argument to option \"" << getLongName() << "\", because it already contains an optional argument.";
 				}
 
 				std::string lowerArgumentName = storm::utility::StringHelper::stringToLower(newArgument->getArgumentName());
 				if (argumentNameSet.find(lowerArgumentName) != argumentNameSet.end()) {
-					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Could not add Argument with Name \"" << newArgument->getArgumentName() << "\" to Option \"" << getLongName() << "\" because it already contains an argument with the same name! Please note that all argument names must be unique in its respective option.");
-					throw storm::exceptions::IllegalArgumentException() << "Could not add Argument with Name \"" << newArgument->getArgumentName() << "\" to Option \"" << getLongName() << "\" because it already contains an argument with the same name! Please note that all argument names must be unique in its respective option.";
+					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Unable to add argument with name \"" << newArgument->getArgumentName() << "\" to option \"" << getLongName() << "\", because it already contains an argument with the same name.");
+					throw storm::exceptions::IllegalArgumentException() << "Unable to add argument with name \"" << newArgument->getArgumentName() << "\" to option \"" << getLongName() << "\", because it already contains an argument with the same name.";
 				}
 				argumentNameSet.insert(lowerArgumentName);
 
@@ -113,8 +113,8 @@ namespace storm {
 
 			Option* build() {
 				if (this->isBuild) {
-					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Called build() on an instance of OptionBuilder which has already build an Instance.");
-					throw storm::exceptions::IllegalFunctionCallException() << "Called build() on an instance of OptionBuilder which has already build an Instance.";
+					LOG4CPLUS_ERROR(logger, "OptionBuilder::addArgument: Illegal call to build() on an instance of OptionBuilder that has already built an instance.");
+					throw storm::exceptions::IllegalFunctionCallException() << "Illegal call to build() on an instance of OptionBuilder that has already built an instance.";
 				}
 
 				this->isBuild = true;

src/settings/Settings.cpp

@@ -51,22 +51,22 @@ void storm::settings::Settings::handleAssignment(std::string const& longOptionNa
 	uint_fast64_t givenArgsCount = arguments.size();
 
 	if (givenArgsCount > option->getArgumentCount()) {
-		LOG4CPLUS_ERROR(logger, "Settings::handleAssignment: Could not parse Arguments for Option \"" << longOptionName << "\": " << arguments.size() << " Arguments given, but max. " << option->getArgumentCount() << " Arguments expected.");
-		throw storm::exceptions::OptionParserException() << "Could not parse Arguments for Option \"" << longOptionName << "\": " << arguments.size() << " Arguments given, but max. " << option->getArgumentCount() << " Arguments expected.";
+		LOG4CPLUS_ERROR(logger, "Settings::handleAssignment: Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but expected no more than " << option->getArgumentCount() << ".");
+		throw storm::exceptions::OptionParserException() << "Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but expected no more than " << option->getArgumentCount() << ".";
 	}
 
 	for (uint_fast64_t i = 0; i < option->getArgumentCount(); ++i) {
 		if (i < givenArgsCount) {
 			storm::settings::fromStringAssignmentResult_t assignmentResult = option->getArgument(i).fromStringValue(arguments.at(i));
 			if (!assignmentResult.first) {
-				LOG4CPLUS_ERROR(logger, "Settings::handleAssignment: Could not parse Arguments for Option \"" << longOptionName << "\": Argument " << option->getArgument(i).getArgumentName() << " rejected the given Value \"" << arguments.at(i) << "\" with Message:\r\n" << assignmentResult.second);
-				throw storm::exceptions::OptionParserException() << "Could not parse Arguments for Option \"" << longOptionName << "\": Argument " << option->getArgument(i).getArgumentName() << " rejected the given Value \"" << arguments.at(i) << "\" with Message:\r\n" << assignmentResult.second;
+				LOG4CPLUS_ERROR(logger, "Settings::handleAssignment: Unable to parse arguments for option \"" << longOptionName << "\": argument " << option->getArgument(i).getArgumentName() << " rejected the given value \"" << arguments.at(i) << "\" with message:\r\n" << assignmentResult.second << ".");
+				throw storm::exceptions::OptionParserException() << "Unable to parse arguments for option \"" << longOptionName << "\": argument " << option->getArgument(i).getArgumentName() << " rejected the given value \"" << arguments.at(i) << "\" with message:\r\n" << assignmentResult.second << ".";
 			}
 		} else {
 			// There is no given value for this argument, only optional
 			if (!option->getArgument(i).getIsOptional()) {
-				LOG4CPLUS_ERROR(logger, "Settings::handleAssignment: Could not parse Arguments for Option \"" << longOptionName << "\": " << arguments.size() << " Arguments given, but more Arguments were expected.");
-				throw storm::exceptions::OptionParserException() << "Could not parse Arguments for Option \"" << longOptionName << "\": " << arguments.size() << " Arguments given, but more Arguments were expected.";
+				LOG4CPLUS_ERROR(logger, "Settings::handleAssignment: Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but more arguments were expected.");
+				throw storm::exceptions::OptionParserException() << "Unable to parse arguments for option \"" << longOptionName << "\": " << arguments.size() << " arguments given, but more arguments were expected.";
 			} else {
 				option->getArgument(i).setFromDefaultValue();
 			}
@@ -136,8 +136,8 @@ void storm::settings::Settings::parseCommandLine(int const argc, char const * co
 				// Short Option
 				std::string nextShortOptionName = storm::utility::StringHelper::stringToLower(nextOption.substr(1, nextOption.size() - 1));
 				if (!this->containsShortName(nextShortOptionName)) {
-					LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Found an unknown ShortName for an Option: \"" << nextShortOptionName << "\".");
-					throw storm::exceptions::OptionParserException() << "Found an unknown ShortName for an Option: \"" << nextShortOptionName << "\".";
+					LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Unknown option name  \"" << nextShortOptionName << "\".");
+					throw storm::exceptions::OptionParserException() << "Unknown option name \"" << nextShortOptionName << "\".";
 				} else {
 					longOptionName = this->getByShortName(nextShortOptionName).getLongName();
 					optionActive = true;
@@ -146,8 +146,8 @@ void storm::settings::Settings::parseCommandLine(int const argc, char const * co
 				// Long Option
 				std::string nextLongOptionName = storm::utility::StringHelper::stringToLower(nextOption.substr(2, nextOption.size() - 2));
 				if (!this->containsLongName(nextLongOptionName)) {
-					LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Found an unknown LongName for an Option: \"" << nextLongOptionName << "\".");
-					throw storm::exceptions::OptionParserException() << "Found an unknown LongName for an Option: \"" << nextLongOptionName << "\".";
+					LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Unknown option name \"" << nextLongOptionName << "\".");
+					throw storm::exceptions::OptionParserException() << "Unknown option name \"" << nextLongOptionName << "\".";
 				} else {
 					longOptionName = this->getByLongName(nextLongOptionName).getLongName();
 					optionActive = true;
@@ -158,16 +158,16 @@ void storm::settings::Settings::parseCommandLine(int const argc, char const * co
 			argCache.push_back(stringArgv.at(i));
 		} else {
 			// No Option active and this is no option.
-			LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Found a stray argument while parsing a given configuration: \"" << stringArgv.at(i) << "\" is neither a known Option nor preceeded by an Option.");
-			throw storm::exceptions::OptionParserException() << "Found a stray argument while parsing a given configuration: \"" << stringArgv.at(i) << "\" is neither a known Option nor preceeded by an Option.";
+			LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Found stray argument while parsing a given configuration, \"" << stringArgv.at(i) << "\" is neither a known option nor preceeded by an option.");
+			throw storm::exceptions::OptionParserException() << "Found stray argument while parsing a given configuration; \"" << stringArgv.at(i) << "\" is neither a known option nor preceeded by an option.";
 		}
 	}
 
 	for (auto it = this->options.cbegin(); it != this->options.cend(); ++it) {
 		if (!it->second.get()->getHasOptionBeenSet()) {
 			if (it->second.get()->getIsRequired()) {
-				LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Option \"" << it->second.get()->getLongName() << "\" is marked as required, but was not set!");
-				throw storm::exceptions::OptionParserException() << "Option \"" << it->second.get()->getLongName() << "\" is marked as required, but was not set!";
+				LOG4CPLUS_ERROR(logger, "Settings::parseCommandLine: Missing required option \"" << it->second.get()->getLongName() << "\".");
+				throw storm::exceptions::OptionParserException() << "Missing required option \"" << it->second.get()->getLongName() << "\".";
 			} else {
 				// Set defaults on optional values
 				for (uint_fast64_t i = 0; i < it->second.get()->getArgumentCount(); ++i) {
@@ -188,19 +188,19 @@ bool storm::settings::Settings::registerNewModule(ModuleRegistrationFunction_t r
 		//LOG4CPLUS_DEBUG(logger, "Settings::registerNewModule: Successfully executed a registrationFunction");
 	} catch (storm::exceptions::IllegalArgumentException e) {
 		//LOG4CPLUS_ERROR(logger, "Settings::registerNewModule: Internal Error while setting up available Options!" << std::endl << "IllegalArgumentException: " << e.what() << ".");
-		std::cout << "Internal Error while setting up available Options!" << std::endl << "IllegalArgumentException: " << e.what() << "." << std::endl;
+		std::cout << "Internal Error while setting up available options." << std::endl << "IllegalArgumentException: " << e.what() << "." << std::endl;
 		return false;
 	} catch (storm::exceptions::IllegalArgumentValueException e) {
 		//LOG4CPLUS_ERROR(logger, "Settings::registerNewModule: Internal Error while setting up available Options!" << std::endl << "IllegalArgumentValueException: " << e.what() << ".");
-		std::cout << "Internal Error while setting up available Options!" << std::endl << "IllegalArgumentValueException: " << e.what() << "." << std::endl;
+		std::cout << "Internal Error while setting up available options." << std::endl << "IllegalArgumentValueException: " << e.what() << "." << std::endl;
 		return false;
 	} catch (storm::exceptions::IllegalFunctionCallException e) {
 		//LOG4CPLUS_ERROR(logger, "Settings::registerNewModule: Internal Error while setting up available Options!" << std::endl << "IllegalFunctionCallException: " << e.what() << ".");
-		std::cout << "Internal Error while setting up available Options!" << std::endl << "IllegalFunctionCallException: " << e.what() << "." << std::endl;
+		std::cout << "Internal Error while setting up available options." << std::endl << "IllegalFunctionCallException: " << e.what() << "." << std::endl;
 		return false;
 	} catch (std::exception e) {
 		//LOG4CPLUS_ERROR(logger, "Settings::registerNewModule: Internal Error while setting up available Options!" << std::endl << "std::exception: " << e.what() << ".");
-		std::cout << "Internal Error while setting up available Options!" << std::endl << "std::exception: " << e.what() << "." << std::endl;
+		std::cout << "Internal Error while setting up available options." << std::endl << "std::exception: " << e.what() << "." << std::endl;
 		return false;
 	}
 	return result;
@@ -229,7 +229,7 @@ storm::settings::Settings& storm::settings::Settings::addOption(Option* option)
 		if (!(shortNameIterator == this->shortNames.end())) {
 			// There exists an option which uses the same shortname
 			//LOG4CPLUS_ERROR(logger, "Settings::addOption: Error: The Option \"" << shortNameIterator->second << "\" from Module \"" << this->options.find(shortNameIterator->second)->second.get()->getModuleName() << "\" uses the same ShortName as the Option \"" << option->getLongName() << "\" from Module \"" << option->getModuleName() << "\"!");
-			throw storm::exceptions::OptionUnificationException() << "Error: The Option \"" << shortNameIterator->second << "\" from Module \"" << this->options.find(shortNameIterator->second)->second.get()->getModuleName() << "\" uses the same ShortName as the Option \"" << option->getLongName() << "\" from Module \"" << option->getModuleName() << "\"!";
+			throw storm::exceptions::OptionUnificationException() << "Error: The option \"" << shortNameIterator->second << "\" of module \"" << this->options.find(shortNameIterator->second)->second.get()->getModuleName() << "\" uses the same name as option \"" << option->getLongName() << "\" of module \"" << option->getModuleName() << "\".";
 		}
 		
 		// Copy Shared_ptr
@@ -296,7 +296,7 @@ std::string storm::settings::Settings::getHelpText() const {
 		for (auto i = 0; i < o.getArgumentCount(); ++i) {
 			ArgumentBase const& a = o.getArgument(i);
 			std::string const& argumentName = a.getArgumentName();
-			ss << delimiter << delimiter << "Arg " << (i+1) << ": " << argumentName;
+			ss << delimiter << delimiter << delimiter << delimiter << "argument <" << (i+1) << "> - " << argumentName;
 			// Fill up the remaining space after the argument Name
 			for (uint_fast64_t i = argumentName.size(); i < argumentNameMaxSize; ++i) {
 				ss << " ";

src/settings/Settings.h

@@ -222,8 +222,8 @@ namespace settings {
 			Option& getByLongName(std::string const& longName) const {
 				auto longNameIterator = this->options.find(storm::utility::StringHelper::stringToLower(longName));
 				if (longNameIterator == this->options.end()) {
-					LOG4CPLUS_ERROR(logger, "Settings::getByLongName: This program does not contain an Option named \"" << longName << "\"!");
-					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an Option named \"" << longName << "\"!";
+					LOG4CPLUS_ERROR(logger, "Settings::getByLongName: This program does not contain an option named \"" << longName << "\".");
+					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\".";
 				}
 				return *longNameIterator->second.get();
 			}
@@ -236,8 +236,8 @@ namespace settings {
 			Option* getPtrByLongName(std::string const& longName) const {
 				auto longNameIterator = this->options.find(storm::utility::StringHelper::stringToLower(longName));
 				if (longNameIterator == this->options.end()) {
-					LOG4CPLUS_ERROR(logger, "Settings::getPtrByLongName: This program does not contain an Option named \"" << longName << "\"!");
-					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an Option named \"" << longName << "\"!";
+					LOG4CPLUS_ERROR(logger, "Settings::getPtrByLongName: This program does not contain an option named \"" << longName << "\".");
+					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << longName << "\".";
 				}
 				return longNameIterator->second.get();
 			}
@@ -250,8 +250,8 @@ namespace settings {
 			Option& getByShortName(std::string const& shortName) const {
 				auto shortNameIterator = this->shortNames.find(storm::utility::StringHelper::stringToLower(shortName));
 				if (shortNameIterator == this->shortNames.end()) {
-					LOG4CPLUS_ERROR(logger, "Settings::getByShortName: This program does not contain an Option named \"" << shortName << "\"!");
-					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an Option with ShortName \"" << shortName << "\"!";
+					LOG4CPLUS_ERROR(logger, "Settings::getByShortName: This program does not contain an option named \"" << shortName << "\".");
+					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\"";
 				}
 				return *(this->options.find(shortNameIterator->second)->second.get());
 			}
@@ -264,8 +264,8 @@ namespace settings {
 			Option* getPtrByShortName(std::string const& shortName) const {
 				auto shortNameIterator = this->shortNames.find(storm::utility::StringHelper::stringToLower(shortName));
 				if (shortNameIterator == this->shortNames.end()) {
-					LOG4CPLUS_ERROR(logger, "Settings::getPtrByShortName: This program does not contain an Option named \"" << shortName << "\"!");
-					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an Option with ShortName \"" << shortName << "\"!";
+					LOG4CPLUS_ERROR(logger, "Settings::getPtrByShortName: This program does not contain an option named \"" << shortName << "\".");
+					throw storm::exceptions::IllegalArgumentException() << "This program does not contain an option named \"" << shortName << "\".";
 				}
 				return this->options.find(shortNameIterator->second)->second.get();
 			}

src/storm.cpp

@@ -331,55 +331,41 @@ int main(const int argc, const char* argv[]) {
                 delete modelchecker;
             }
 		} else if (s->isSet("symbolic")) {
-			std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString();
-			std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString();
+            // First, we build the model using the given symbolic model description and constant definitions.
+            std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString();
+            std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString();
             storm::ir::Program program = storm::parser::PrismParserFromFile(programFile);
-			std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, constants);
-			model->printModelInformationToStream(std::cout);
-
-            // Enable the following lines to test the MinimalLabelSetGenerator.
-            if (model->getType() == storm::models::MDP) {
-                std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
-            
-                // Build stuff for coin example.
-//                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
-//                storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
-//                storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
-//                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true, true);
-
-//                storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff");
-//                storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered");
-//                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, ~collisionStates, deliveredStates, 0.5, true, false);
-
-//                storm::storage::BitVector const& electedStates = labeledMdp->getLabeledStates("elected");
-//                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), electedStates, 0.5, true, true);
-            }
-            
-            // Enable the following lines to test the SMTMinimalCommandSetGenerator.
-            if (model->getType() == storm::models::MDP) {
-                std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
+            std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, constants);
+            model->printModelInformationToStream(std::cout);
+
+            if (s->isSet("mincmd")) {
+                if (model->getType() != storm::models::MDP) {
+                    LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP.");
+                    throw storm::exceptions::InternalTypeErrorException() << "Minimal command counterexample generation is only supported for models of type MDP.";
+                }
                 
-                // Build stuff for coin example.
-//                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
-//                storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
-//                storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
-//                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
+                std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
                 
-                // Build stuff for csma example.
-//                storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff");
-//                storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered");
-//                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, ~collisionStates, deliveredStates, 0.5, true);
+                // Determine whether we are required to use the MILP-version or the SAT-version.
+                bool useMILP = s->getOptionByLongName("mincmd").getArgumentByName("method").getValueAsString() == "milp";
                 
-                // Build stuff for firewire example.
-//                storm::storage::BitVector const& electedStates = labeledMdp->getLabeledStates("elected");
-//                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), electedStates, 0.5, true);
-
-                // Build stuff for wlan example.
-//                storm::storage::BitVector const& oneCollisionStates = labeledMdp->getLabeledStates("oneCollision");
-//                storm::storage::BitVector const& twoCollisionStates = labeledMdp->getLabeledStates("twoCollisions");
-//                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), twoCollisionStates, 0.1, true);
+                // Now parse the property file and receive the list of parsed formulas.
+                std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString();
+                std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = storm::parser::PrctlFileParser(propertyFile);
+
+                // Now generate the counterexamples for each formula.
+                for (storm::property::prctl::AbstractPrctlFormula<double>* formulaPtr : formulaList) {
+                    if (useMILP) {
+                        storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(*mdp, formulaPtr);
+                    } else {
+                        storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr);
+                    }
+                    
+                    // Once we are done with the formula, delete it.
+                    delete formulaPtr;
+                }
             }
-		}
+        }
 
         // Perform clean-up and terminate.
 		cleanUp();

src/utility/StormOptions.cpp

@@ -1,24 +1,38 @@
 #include "src/utility/StormOptions.h"
 
 bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* settings) -> bool {
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "help", "h", "Shows all available Options, Arguments and Descriptions").build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "verbose", "v", "Be verbose").build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "debug", "", "Be very verbose (intended for debugging)").build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "trace", "", "Be extremly verbose (intended for debugging, heavy performance impacts)").build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "logfile", "l", "If specified, the log output will also be written to this file").addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the File to write to").build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the File to read from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from Transition- and Labeling Files").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the File to read the transition system from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the File to read the labeling from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "symbolic", "", "Parse the given PRISM File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prismFileName", "The path and name of the File to read the PRISM Model from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build());
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "help", "h", "Shows all available options, arguments and descriptions.").build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "verbose", "v", "Be verbose.").build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "debug", "", "Be very verbose (intended for debugging).").build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "trace", "", "Be extremly verbose (intended for debugging, heavy performance impacts).").build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "logfile", "l", "If specified, the log output will also be written to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("logFileName", "The path and name of the file to write to.").build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "configfile", "c", "If specified, this file will be read and parsed for additional configuration settings.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("configFileName", "The path and name of the file from which to read.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "explicit", "", "Explicit parsing from transition- and labeling files.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionFileName", "The path and name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("labelingFileName", "The path and name of the file from which to read the labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "symbolic", "", "Parse the given symbolic model file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("symbolicFileName", "The path and name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Performs model checking for the PRCTL formulas given in the file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The file from which to read the PRCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Performs model checking for the CSL formulas given in the file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The file from which to read the CSL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Performs model checking for the LTL formulas given in the file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the transition rewards are read from this file and added to the explicit model. Note that this requires an explicit model.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The file from which to read the rransition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the state rewards are read from this file and added to the explicit model. Note that this requires an explicit model.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+    
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "If the model contains deadlock states, setting this option will insert self-loops for these states.").build());
+    
 	std::vector<std::string> matrixLibrarys;
 	matrixLibrarys.push_back("gmm++");
 	matrixLibrarys.push_back("native");
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "matrixLibrary", "m", "Which matrix library is to be used in numerical solving").addArgument(storm::settings::ArgumentBuilder::createStringArgument("matrixLibraryName", "Name of a buildin Library").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(matrixLibrarys)).setDefaultValueString("gmm++").build()).build());
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "matrixLibrary", "m", "Sets which matrix library is preferred for numerical operations.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("matrixLibraryName", "The name of a matrix library. Valid values are gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(matrixLibrarys)).setDefaultValueString("gmm++").build()).build());
 
 	return true;
 });