From 47a05fc1b07cdf68d0ed27a6a4f1288b223fefd2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 17 Oct 2013 22:19:24 +0200 Subject: [PATCH] Beautified output of option system. Enabled command line interface of counterexample generation. Former-commit-id: cecc5e85b39c31f04932a75ab3b23dfb003eeea5 --- CMakeLists.txt | 6 +- .../MILPMinimalLabelSetGenerator.cpp | 9 ++ .../MILPMinimalLabelSetGenerator.h | 90 ++++++++++++++++--- .../SMTMinimalCommandSetGenerator.h | 55 +++++++++++- src/settings/ArgumentBuilder.h | 12 +-- src/settings/ArgumentType.h | 4 +- src/settings/ArgumentTypeInferationHelper.h | 44 ++++----- src/settings/ArgumentValidators.h | 8 +- src/settings/Option.h | 48 +++++----- src/settings/OptionBuilder.h | 20 ++--- src/settings/Settings.cpp | 40 ++++----- src/settings/Settings.h | 16 ++-- src/storm.cpp | 74 +++++++-------- src/utility/StormOptions.cpp | 44 +++++---- 14 files changed, 297 insertions(+), 173 deletions(-) create mode 100644 src/counterexamples/MILPMinimalLabelSetGenerator.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 83f581951..9bb6e10da 100644 --- a/CMakeLists.txt +++ b/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) ############################################################# diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.cpp b/src/counterexamples/MILPMinimalLabelSetGenerator.cpp new file mode 100644 index 000000000..8699353fe --- /dev/null +++ b/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 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; +}); diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 7f15b3975..81c20a68d 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/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::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 getMinimalLabelSet(storm::models::Mdp 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 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(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 const& labeledMdp, storm::property::prctl::AbstractPrctlFormula 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 const* probBoundFormula = dynamic_cast 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 const& pathFormula = probBoundFormula->getPathFormula(); + storm::storage::BitVector phiStates; + storm::storage::BitVector psiStates; + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + try { + storm::property::prctl::Until const& untilFormula = dynamic_cast 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 const& eventuallyFormula = dynamic_cast 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 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(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 diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 0d873b846..ff7bbd8b7 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/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(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 const& labeledMdp, storm::property::prctl::AbstractPrctlFormula 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 const* probBoundFormula = dynamic_cast 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 const& pathFormula = probBoundFormula->getPathFormula(); + storm::storage::BitVector phiStates; + storm::storage::BitVector psiStates; + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + try { + storm::property::prctl::Until const& untilFormula = dynamic_cast 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 const& eventuallyFormula = dynamic_cast 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 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(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 diff --git a/src/settings/ArgumentBuilder.h b/src/settings/ArgumentBuilder.h index b608bee28..30350ca50 100644 --- a/src/settings/ArgumentBuilder.h +++ b/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."; } } diff --git a/src/settings/ArgumentType.h b/src/settings/ArgumentType.h index d3ea7eb77..c652f8d2f 100644 --- a/src/settings/ArgumentType.h +++ b/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."; } } } diff --git a/src/settings/ArgumentTypeInferationHelper.h b/src/settings/ArgumentTypeInferationHelper.h index dc34236e0..87b16ac12 100644 --- a/src/settings/ArgumentTypeInferationHelper.h +++ b/src/settings/ArgumentTypeInferationHelper.h @@ -45,8 +45,8 @@ namespace storm { template 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 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(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 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(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 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(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 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(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 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(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; } diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h index 32084a90c..d87d4a7d5 100644 --- a/src/settings/ArgumentValidators.h +++ b/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); diff --git a/src/settings/Option.h b/src/settings/Option.h index 3e82376b2..c7191d5b7 100644 --- a/src/settings/Option.h +++ b/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); diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h index b28411cdb..6899114e0 100644 --- a/src/settings/OptionBuilder.h +++ b/src/settings/OptionBuilder.h @@ -85,24 +85,24 @@ namespace storm { // For automatic management of newArgument's lifetime std::shared_ptr 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; diff --git a/src/settings/Settings.cpp b/src/settings/Settings.cpp index 972c8ea84..eb401dba4 100644 --- a/src/settings/Settings.cpp +++ b/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 << " "; diff --git a/src/settings/Settings.h b/src/settings/Settings.h index 2fb63fc7f..a57344da9 100644 --- a/src/settings/Settings.h +++ b/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(); } diff --git a/src/storm.cpp b/src/storm.cpp index 5fef49964..5c07c3c75 100644 --- a/src/storm.cpp +++ b/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> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, constants); - model->printModelInformationToStream(std::cout); - - // Enable the following lines to test the MinimalLabelSetGenerator. - if (model->getType() == storm::models::MDP) { - std::shared_ptr> labeledMdp = model->as>(); - - // 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 labels = storm::counterexamples::MILPMinimalLabelSetGenerator::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 labels = storm::counterexamples::MILPMinimalLabelSetGenerator::getMinimalLabelSet(*labeledMdp, ~collisionStates, deliveredStates, 0.5, true, false); - -// storm::storage::BitVector const& electedStates = labeledMdp->getLabeledStates("elected"); -// std::set labels = storm::counterexamples::MILPMinimalLabelSetGenerator::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> labeledMdp = model->as>(); + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::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 labels = storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true); + std::shared_ptr> mdp = model->as>(); - // 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 labels = storm::counterexamples::SMTMinimalCommandSetGenerator::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 labels = storm::counterexamples::SMTMinimalCommandSetGenerator::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 labels = storm::counterexamples::SMTMinimalCommandSetGenerator::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*> formulaList = storm::parser::PrctlFileParser(propertyFile); + + // Now generate the counterexamples for each formula. + for (storm::property::prctl::AbstractPrctlFormula* formulaPtr : formulaList) { + if (useMILP) { + storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(*mdp, formulaPtr); + } else { + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, constants, *mdp, formulaPtr); + } + + // Once we are done with the formula, delete it. + delete formulaPtr; + } } - } + } // Perform clean-up and terminate. cleanUp(); diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index e35d09b05..27e2ccec8 100644 --- a/src/utility/StormOptions.cpp +++ b/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 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; }); \ No newline at end of file