diff --git a/examples/mdp/tiny/tiny.clab b/examples/mdp/tiny/tiny.clab new file mode 100644 index 000000000..c23988f1a --- /dev/null +++ b/examples/mdp/tiny/tiny.clab @@ -0,0 +1,4 @@ +0 0 3 +0 1 1 +1 0 2 +2 0 0 diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 81a224a22..8ed43e87a 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -182,7 +182,8 @@ namespace storm { void Model::printModelInformationFooterToStream(std::ostream& out) const { this->printRewardModelsInformationToStream(out); this->getStateLabeling().printLabelingInformationToStream(out); - out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl; + out << "choice labels: \t" << (this->hasChoiceLabeling() ? "yes" : "no") << std::noboolalpha << std::endl; + out << "Size in memory: " << (this->getSizeInBytes())/1024 << " kbytes" << std::endl; out << "-------------------------------------------------------------- " << std::endl; } diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 6bd71189d..b99623784 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -14,76 +14,81 @@ #include "src/utility/OsDetection.h" namespace storm { - namespace parser { + namespace parser { - using namespace storm::utility::cstring; + using namespace storm::utility::cstring; - std::shared_ptr> AutoParser::parseModel(std::string const & transitionsFilename, - std::string const & labelingFilename, - std::string const & stateRewardFilename, - std::string const & transitionRewardFilename) { + std::shared_ptr> AutoParser::parseModel(std::string const& transitionsFilename, + std::string const& labelingFilename, + std::string const& stateRewardFilename, + std::string const& transitionRewardFilename, + std::string const& choiceLabelingFilename) { - // Find and parse the model type hint. - storm::models::ModelType type = AutoParser::analyzeHint(transitionsFilename); + // Find and parse the model type hint. + storm::models::ModelType type = AutoParser::analyzeHint(transitionsFilename); - // Do the actual parsing. - std::shared_ptr> model; - switch (type) { - case storm::models::ModelType::Dtmc: { + // Do the actual parsing. + std::shared_ptr> model; + switch (type) { + case storm::models::ModelType::Dtmc: + { model.reset(new storm::models::sparse::Dtmc(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); - break; - } - case storm::models::ModelType::Ctmc: { - model.reset(new storm::models::sparse::Ctmc(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); - break; - } - case storm::models::ModelType::Mdp: { - model.reset(new storm::models::sparse::Mdp(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); - break; - } - case storm::models::ModelType::MarkovAutomaton: { - model.reset(new storm::models::sparse::MarkovAutomaton(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); - break; - } - default: - LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type which cannot be parsed."); // Unknown - } - - return model; - } - - storm::models::ModelType AutoParser::analyzeHint(std::string const & filename) { - storm::models::ModelType hintType = storm::models::ModelType::Dtmc; - - // Open the file. - MappedFile file(filename.c_str()); - - STORM_LOG_THROW(file.getDataSize() >= STORM_PARSER_AUTOPARSER_HINT_LENGTH, storm::exceptions::WrongFormatException, "File too short to be readable."); - char const* fileData = file.getData(); - - char filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1]; - memcpy(filehintBuffer, fileData, STORM_PARSER_AUTOPARSER_HINT_LENGTH); - filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH] = 0; - - // Find and read in the hint. - std::string formatString = "%" + std::to_string(STORM_PARSER_AUTOPARSER_HINT_LENGTH) + "s"; + break; + } + case storm::models::ModelType::Ctmc: + { + model.reset(new storm::models::sparse::Ctmc(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); + break; + } + case storm::models::ModelType::Mdp: + { + model.reset(new storm::models::sparse::Mdp(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename)))); + break; + } + case storm::models::ModelType::MarkovAutomaton: + { + model.reset(new storm::models::sparse::MarkovAutomaton(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); + break; + } + default: + LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type which cannot be parsed."); // Unknown + } + + return model; + } + + storm::models::ModelType AutoParser::analyzeHint(std::string const & filename) { + storm::models::ModelType hintType = storm::models::ModelType::Dtmc; + + // Open the file. + MappedFile file(filename.c_str()); + + STORM_LOG_THROW(file.getDataSize() >= STORM_PARSER_AUTOPARSER_HINT_LENGTH, storm::exceptions::WrongFormatException, "File too short to be readable."); + char const* fileData = file.getData(); + + char filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1]; + memcpy(filehintBuffer, fileData, STORM_PARSER_AUTOPARSER_HINT_LENGTH); + filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH] = 0; + + // Find and read in the hint. + std::string formatString = "%" + std::to_string(STORM_PARSER_AUTOPARSER_HINT_LENGTH) + "s"; char hint[STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1]; - #ifdef WINDOWS - sscanf_s(filehintBuffer, formatString.c_str(), hint, STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1); - #else - sscanf(filehintBuffer, formatString.c_str(), hint); - #endif - for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); - - // Check if the hint value is known and store the appropriate enum value. - if (strcmp(hint, "DTMC") == 0) hintType = storm::models::ModelType::Dtmc; - else if (strcmp(hint, "CTMC") == 0) hintType = storm::models::ModelType::Ctmc; - else if (strcmp(hint, "MDP") == 0) hintType = storm::models::ModelType::Mdp; - else if (strcmp(hint, "MA") == 0) hintType = storm::models::ModelType::MarkovAutomaton; +#ifdef WINDOWS + sscanf_s(filehintBuffer, formatString.c_str(), hint, STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1); +#else + sscanf(filehintBuffer, formatString.c_str(), hint); +#endif + for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); + + // Check if the hint value is known and store the appropriate enum value. + if (strcmp(hint, "DTMC") == 0) hintType = storm::models::ModelType::Dtmc; + else if (strcmp(hint, "CTMC") == 0) hintType = storm::models::ModelType::Ctmc; + else if (strcmp(hint, "MDP") == 0) hintType = storm::models::ModelType::Mdp; + else if (strcmp(hint, "MA") == 0) hintType = storm::models::ModelType::MarkovAutomaton; else STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unable to find model hint in explicit input."); - return hintType; - } + return hintType; + } - } // namespace parser + } // namespace parser } // namespace storm diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 7d624e9b6..1a4f2d2a3 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -41,12 +41,16 @@ namespace storm { * @param labelingFilename The path and name of the file containing the labels for the states of the model. * @param stateRewardFilename The path and name of the file that contains the state reward of the model. This file is optional. * @param transitionRewardFilename The path and name of the file that contains the transition rewards of the model. This file is optional. + * @param choiceLabelingFilename The path and name of the file that contains the choice labeling of the model. This file is optional. + * Note: this file is only meaningful for certain models (currently only MDPs). If the model is not of a type for which this input + * is meaningful, this file will not be parsed. * @return A shared_ptr containing the resulting model. */ - static std::shared_ptr> parseModel(std::string const & transitionsFilename, - std::string const & labelingFilename, - std::string const & stateRewardFilename = "", - std::string const & transitionRewardFilename = ""); + static std::shared_ptr> parseModel(std::string const& transitionsFilename, + std::string const& labelingFilename, + std::string const& stateRewardFilename = "", + std::string const& transitionRewardFilename = "", + std::string const& choiceLabelingFilename = ""); private: // Define the maximal length of a hint in the file. diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 8f3e8028d..56c055c92 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -8,47 +8,55 @@ #include "src/parser/NondeterministicSparseTransitionParser.h" #include "src/parser/AtomicPropositionLabelingParser.h" #include "src/parser/SparseStateRewardParser.h" +#include "src/parser/SparseChoiceLabelingParser.h" namespace storm { - namespace parser { + namespace parser { - NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { + NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename, std::string const& choiceLabelingFilename) { - // Parse the transitions. - storm::storage::SparseMatrix transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename))); + // Parse the transitions. + storm::storage::SparseMatrix transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename))); - uint_fast64_t stateCount = transitions.getColumnCount(); + uint_fast64_t stateCount = transitions.getColumnCount(); - // Parse the state labeling. - storm::models::sparse::StateLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename))); + // Parse the state labeling. + storm::models::sparse::StateLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename))); - // Only parse state rewards if a file is given. - boost::optional> stateRewards; - if (stateRewardFilename != "") { - stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename); - } + // Only parse state rewards if a file is given. + boost::optional> stateRewards; + if (!stateRewardFilename.empty()) { + stateRewards = std::move(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename)); + } - // Only parse transition rewards if a file is given. - boost::optional> transitionRewards; - if (transitionRewardFilename != "") { - transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions); - } + // Only parse transition rewards if a file is given. + boost::optional> transitionRewards; + if (!transitionRewardFilename.empty()) { + transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions)); + } - // Construct the result. - Result result(std::move(transitions), std::move(labeling)); - result.stateRewards = stateRewards; - result.transitionRewards = transitionRewards; + // Only parse choice labeling if a file is given. + boost::optional> choiceLabeling; + if (!choiceLabelingFilename.empty()) { + choiceLabeling = std::move(storm::parser::SparseChoiceLabelingParser::parseChoiceLabeling(transitions.getRowGroupIndices(), choiceLabelingFilename)); + } - return result; - } + // Construct the result. + Result result(std::move(transitions), std::move(labeling)); + result.stateRewards = std::move(stateRewards); + result.transitionRewards = std::move(transitionRewards); + result.choiceLabeling = std::move(choiceLabeling); + + return result; + } + + storm::models::sparse::Mdp NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename, std::string const& choiceLabelingFilename) { + Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename); - storm::models::sparse::Mdp NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { - Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename); - std::unordered_map> rewardModels; rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); - return storm::models::sparse::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::optional>>()); - } + return storm::models::sparse::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), std::move(parserResult.choiceLabeling)); + } - } /* namespace parser */ + } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/NondeterministicModelParser.h b/src/parser/NondeterministicModelParser.h index d982064cd..9777609ca 100644 --- a/src/parser/NondeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -60,6 +60,11 @@ namespace storm { * Optional rewards for each transition. */ boost::optional> transitionRewards; + + /*! + * Optional choice labeling. + */ + boost::optional> choiceLabeling; }; /*! @@ -75,9 +80,10 @@ namespace storm { * @param labelingFilename The path and name of the file containing the labels for the states of the model. * @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional. * @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional. + * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional. * @return The parsed Mdp. */ - static storm::models::sparse::Mdp parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = ""); + static storm::models::sparse::Mdp parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = "", std::string const& choiceLabelingFilename = ""); private: @@ -92,9 +98,10 @@ namespace storm { * @param labelingFilename The path and name of the file containing the labels for the states of the model. * @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional. * @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional. + * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional. * @return The parsed model encapsulated in a Result structure. */ - static Result parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = ""); + static Result parseNondeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "", std::string const& choiceLabelingFilename = ""); }; diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index 364c364b0..30560445c 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -1,9 +1,3 @@ -/*! - * SparseStateRewardParser.cpp - * - * Created on: 23.12.2012 - * Author: Christian Dehnert - */ #include #include "src/parser/SparseStateRewardParser.h" @@ -43,7 +37,7 @@ namespace storm { // Iterate over states. while (buf[0] != '\0') { - // Parse state number and reward value. + // Parse state. state = checked_strtol(buf, &buf); // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). @@ -58,6 +52,7 @@ namespace storm { throw storm::exceptions::OutOfRangeException() << "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\""; } + // Parse reward value. reward = checked_strtod(buf, &buf); if (reward < 0.0) { diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index f3331d516..fd63cd780 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -33,6 +33,7 @@ namespace storm { const std::string GeneralSettings::propertyOptionShortName = "prop"; const std::string GeneralSettings::transitionRewardsOptionName = "transrew"; const std::string GeneralSettings::stateRewardsOptionName = "staterew"; + const std::string GeneralSettings::choiceLabelingOptionName = "choicelab"; const std::string GeneralSettings::counterexampleOptionName = "counterexample"; const std::string GeneralSettings::counterexampleOptionShortName = "cex"; const std::string GeneralSettings::dontFixDeadlockOptionName = "nofixdl"; @@ -84,6 +85,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); std::vector engines = {"sparse", "hybrid", "dd"}; @@ -193,6 +196,14 @@ namespace storm { return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString(); } + bool GeneralSettings::isChoiceLabelingSet() const { + return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet(); + } + + std::string GeneralSettings::getChoiceLabelingFilename() const { + return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString(); + } + bool GeneralSettings::isCounterexampleSet() const { return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index f10035c71..f4c69d835 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -10,39 +10,42 @@ namespace storm { enum class LpSolverType; enum class MinMaxTechnique; } - + namespace settings { namespace modules { - + /*! * This class represents the general settings. */ class GeneralSettings : public ModuleSettings { - public: + public: // An enumeration of all engines. - enum class Engine { Sparse, Hybrid, Dd }; - + + enum class Engine { + Sparse, Hybrid, Dd + }; + /*! * Creates a new set of general settings that is managed by the given manager. * * @param settingsManager The responsible manager. */ GeneralSettings(storm::settings::SettingsManager& settingsManager); - + /*! * Retrieves whether the help option was set. * * @return True if the help option was set. */ bool isHelpSet() const; - - /*! + + /*! * Retrieves whether the version option was set. * * @return True if the version option was set. */ bool isVersionSet() const; - + /*! * Retrieves the name of the module for which to show the help or "all" to indicate that the full help * needs to be shown. @@ -50,56 +53,56 @@ namespace storm { * @return The name of the module for which to show the help or "all". */ std::string getHelpModuleName() const; - + /*! * Retrieves whether the verbose option was set. * * @return True if the verbose option was set. */ bool isVerboseSet() const; - + /*! * Retrieves the precision to use for numerical operations. * * @return The precision to use for numerical operations. */ double getPrecision() const; - + /*! * Retrieves whether the export-to-dot option was set. * * @return True if the export-to-dot option was set. */ bool isExportDotSet() const; - + /*! * Retrieves the name in which to write the model in dot format, if the export-to-dot option was set. * * @return The name of the file in which to write the exported model. */ std::string getExportDotFilename() const; - + /*! * Retrieves whether the config option was set. * * @return True if the config option was set. */ bool isConfigSet() const; - + /*! * Retrieves the name of the file that is to be scanned for settings. * * @return The name of the file that is to be scanned for settings. */ std::string getConfigFilename() const; - + /*! * Retrieves whether the explicit option was set. * * @return True if the explicit option was set. */ bool isExplicitSet() const; - + /*! * Retrieves the name of the file that contains the transitions if the model was given using the explicit * option. @@ -115,14 +118,14 @@ namespace storm { * @return The name of the file that contains the state labeling. */ std::string getLabelingFilename() const; - + /*! * Retrieves whether the symbolic option was set. * * @return True if the symbolic option was set. */ bool isSymbolicSet() const; - + /*! * Retrieves the name of the file that contains the symbolic model specification if the model was given * using the symbolic option. @@ -130,14 +133,14 @@ namespace storm { * @return The name of the file that contains the symbolic model specification. */ std::string getSymbolicModelFilename() const; - + /*! * Retrieves whether the property option was set. * * @return True if the property option was set. */ bool isPropertySet() const; - + /*! * Retrieves the property specified with the property option. * @@ -159,14 +162,14 @@ namespace storm { * @return The name of the file that contains the transition rewards. */ std::string getTransitionRewardsFilename() const; - + /*! * Retrieves whether the state reward option was set. * * @return True if the state reward option was set. */ bool isStateRewardsSet() const; - + /*! * Retrieves the name of the file that contains the state rewards if the model was given using the * explicit option. @@ -174,7 +177,22 @@ namespace storm { * @return The name of the file that contains the state rewards. */ std::string getStateRewardsFilename() const; - + + /*! + * Retrieves whether the choice labeling option was set. + * + * @return True iff the choice labeling option was set. + */ + bool isChoiceLabelingSet() const; + + /*! + * Retrieves the name of the file that contains the choice labeling + * if the model was given using the explicit option. + * + * @return The name of the file that contains the choice labeling. + */ + std::string getChoiceLabelingFilename() const; + /*! * Retrieves whether the counterexample option was set. * @@ -189,7 +207,7 @@ namespace storm { * @return The name of the file to which the counterexample is to be written. */ std::string getCounterexampleFilename() const; - + /*! * Retrieves whether the dont-fix-deadlocks option was set. * @@ -205,7 +223,7 @@ namespace storm { * @return The memento that will eventually restore the original value. */ std::unique_ptr overrideDontFixDeadlocksSet(bool stateToSet); - + /*! * Overrides the option to enable the PRISM compatibility mode by setting it to the specified value. As * soon as the returned memento goes out of scope, the original value is restored. @@ -214,14 +232,14 @@ namespace storm { * @return The memento that will eventually restore the original value. */ std::unique_ptr overridePrismCompatibilityMode(bool stateToSet); - + /*! * Retrieves whether the timeout option was set. * * @return True if the timeout option was set. */ bool isTimeoutSet() const; - + /*! * Retrieves the time after which the computation has to be aborted in case the timeout option was set. * @@ -235,42 +253,42 @@ namespace storm { * @return The selected convergence criterion. */ storm::solver::EquationSolverType getEquationSolver() const; - + /*! * Retrieves whether a equation solver has been set. * * @return True iff an equation solver has been set. */ bool isEquationSolverSet() const; - + /*! * Retrieves the selected LP solver. * * @return The selected LP solver. */ storm::solver::LpSolverType getLpSolver() const; - + /*! * Retrieves whether the export-to-dot option was set. * * @return True if the export-to-dot option was set. */ bool isConstantsSet() const; - + /*! * Retrieves the string that defines the constants of a symbolic model (given via the symbolic option). * * @return The string that defines the constants of a symbolic model. */ std::string getConstantDefinitionString() const; - + /*! * Retrieves whether statistics are to be shown for counterexample generation. * * @return True iff statistics are to be shown for counterexample generation. */ bool isShowStatisticsSet() const; - + /*! * Retrieves whether the option to perform bisimulation minimization is set. * @@ -284,21 +302,21 @@ namespace storm { * @return True iff the option was set. */ bool isCudaSet() const; - + /*! * Retrieves the selected engine. * * @return The selected engine. */ Engine getEngine() const; - + /*! * Retrieves whether the PRISM compatibility mode was enabled. * * @return True iff the PRISM compatibility mode was enabled. */ bool isPrismCompatibilityEnabled() const; - + #ifdef STORM_HAVE_CARL /*! * Retrieves whether the option enabling parametric model checking is set. @@ -307,21 +325,21 @@ namespace storm { */ bool isParametricSet() const; #endif - /*! - * Retrieves whether a min/max equation solving technique has been set. - * - * @return True iff an equation solving technique has been set. - */ - bool isMinMaxEquationSolvingTechniqueSet() const; - - /*! - * Retrieves the selected min/max equation solving technique. - * - * @return The selected min/max equation solving technique. - */ - storm::solver::MinMaxTechnique getMinMaxEquationSolvingTechnique() const; - - + /*! + * Retrieves whether a min/max equation solving technique has been set. + * + * @return True iff an equation solving technique has been set. + */ + bool isMinMaxEquationSolvingTechniqueSet() const; + + /*! + * Retrieves the selected min/max equation solving technique. + * + * @return The selected min/max equation solving technique. + */ + storm::solver::MinMaxTechnique getMinMaxEquationSolvingTechnique() const; + + bool check() const override; // The name of the module. @@ -331,7 +349,7 @@ namespace storm { // Define the string names of the options as constants. static const std::string helpOptionName; static const std::string helpOptionShortName; - static const std::string versionOptionName; + static const std::string versionOptionName; static const std::string verboseOptionName; static const std::string verboseOptionShortName; static const std::string precisionOptionName; @@ -347,6 +365,7 @@ namespace storm { static const std::string propertyOptionShortName; static const std::string transitionRewardsOptionName; static const std::string stateRewardsOptionName; + static const std::string choiceLabelingOptionName; static const std::string counterexampleOptionName; static const std::string counterexampleOptionShortName; static const std::string dontFixDeadlockOptionName; @@ -366,13 +385,13 @@ namespace storm { static const std::string cudaOptionName; static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; - static const std::string minMaxEquationSolvingTechniqueOptionName; + static const std::string minMaxEquationSolvingTechniqueOptionName; #ifdef STORM_HAVE_CARL static const std::string parametricOptionName; #endif }; - + } // namespace modules } // namespace settings } // namespace storm diff --git a/src/utility/storm.h b/src/utility/storm.h index b54ee42d6..41ccaf68b 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -75,8 +75,8 @@ namespace storm { template - std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::optional(), boost::optional const& transitionRewardsFile = boost::optional()) { - return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : ""); + std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::optional(), boost::optional const& transitionRewardsFile = boost::optional(), boost::optional const& choiceLabelingFile = boost::optional()) { + return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } template @@ -380,7 +380,7 @@ namespace storm { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); - std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional()); + std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional()); // Preprocess the model if needed. model = preprocessModel(model, formulas);