diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 77b37684e..fc1170cd9 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -10,6 +10,7 @@ #include "src/storage/expressions/ExpressionManager.h" #include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/generator/PrismNextStateGenerator.h" #include "src/generator/PrismStateLabelingGenerator.h" @@ -84,17 +85,17 @@ namespace storm { } template - ExplicitPrismModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { this->preserveFormula(formula); } template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 7ff84ef22..944a7c3f9 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -4,6 +4,8 @@ #include "../utility/storm.h" #include "src/settings/modules/DebugSettings.h" +#include "src/settings/modules/IOSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/exceptions/OptionParserException.h" #include "src/utility/storm-version.h" @@ -205,12 +207,10 @@ namespace storm { storm::utility::initializeFileLogging(); } - storm::settings::modules::MarkovChainSettings const& settings = storm::settings::getModule(); - // If we have to build the model from a symbolic representation, we need to parse the representation first. boost::optional program; - if (settings.isSymbolicSet()) { - std::string const& programFile = settings.getSymbolicModelFilename(); + if (storm::settings::getModule().isSymbolicSet()) { + std::string const& programFile = storm::settings::getModule().getSymbolicModelFilename(); program = storm::parseProgram(programFile); } @@ -228,7 +228,7 @@ namespace storm { } std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); - if (settings.isSymbolicSet()) { + if (storm::settings::getModule().isSymbolicSet()) { #ifdef STORM_HAVE_CARL if (storm::settings::getModule().isParametricSet()) { buildAndCheckSymbolicModel(program.get(), formulas, true); @@ -238,7 +238,8 @@ namespace storm { #ifdef STORM_HAVE_CARL } #endif - } else if (settings.isExplicitSet()) { + } else if (storm::settings::getModule().isExplicitSet()) { + STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use explicit input models with this engine."); buildAndCheckExplicitModel(formulas, true); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f1febc74e..5745caa62 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -164,7 +164,7 @@ namespace storm { template void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - storm::settings::modules::MarkovChainSettings const& settings = storm::settings::getModule(); + storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); 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() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 853b5c3e1..2f2cb33d1 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -15,6 +15,7 @@ #include "src/utility/storm-version.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/CounterexampleGeneratorSettings.h" #include "src/settings/modules/CuddSettings.h" @@ -489,12 +490,17 @@ namespace storm { return dynamic_cast(mutableManager().getModule(storm::settings::modules::MarkovChainSettings::moduleName)); } + storm::settings::modules::IOSettings& mutableIOSettings() { + return dynamic_cast(mutableManager().getModule(storm::settings::modules::IOSettings::moduleName)); + } + void initializeAll(std::string const& name, std::string const& executableName) { storm::settings::mutableManager().setName(name, executableName); // Register all known settings modules. storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 5b0141045..0efdcd2fd 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -13,6 +13,7 @@ namespace storm { namespace settings { namespace modules { class MarkovChainSettings; + class IOSettings; class ModuleSettings; } class Option; @@ -272,6 +273,14 @@ namespace storm { */ storm::settings::modules::MarkovChainSettings& mutableMarkovChainSettings(); + /*! + * Retrieves the IO settings in a mutable form. This is only meant to be used for debug purposes or very + * rare cases where it is necessary. + * + * @return An object that allows accessing and modifying the IO settings. + */ + storm::settings::modules::IOSettings& mutableIOSettings(); + } // namespace settings } // namespace storm diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp index 6c245d3b2..b2dbb0ddc 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" namespace storm { namespace settings { @@ -48,7 +48,7 @@ namespace storm { bool CounterexampleGeneratorSettings::check() const { // Ensure that the model was given either symbolically or explicitly. - STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified symbolically."); + STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified symbolically."); if (isMinimalCommandSetGenerationSet()) { STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect."); diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp new file mode 100644 index 000000000..ae11caa7b --- /dev/null +++ b/src/settings/modules/IOSettings.cpp @@ -0,0 +1,151 @@ +#include "src/settings/modules/IOSettings.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/SettingMemento.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" +#include "src/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string IOSettings::moduleName = "io"; + const std::string IOSettings::exportDotOptionName = "exportdot"; + const std::string IOSettings::exportMatOptionName = "exportmat"; + const std::string IOSettings::explicitOptionName = "explicit"; + const std::string IOSettings::explicitOptionShortName = "exp"; + const std::string IOSettings::symbolicOptionName = "symbolic"; + const std::string IOSettings::symbolicOptionShortName = "s"; + const std::string IOSettings::explorationOrderOptionName = "explorder"; + const std::string IOSettings::explorationOrderOptionShortName = "eo"; + const std::string IOSettings::transitionRewardsOptionName = "transrew"; + const std::string IOSettings::stateRewardsOptionName = "staterew"; + const std::string IOSettings::choiceLabelingOptionName = "choicelab"; + const std::string IOSettings::constantsOptionName = "constants"; + const std::string IOSettings::constantsOptionShortName = "const"; + const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; + const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; + + IOSettings::IOSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportMatOptionName, "", "If given, the loaded model will be written to the specified file in the mat format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + + std::vector explorationOrders = {"dfs", "bfs"}; + this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition 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 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, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); + } + + bool IOSettings::isExportDotSet() const { + return this->getOption(exportDotOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportDotFilename() const { + return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool IOSettings::isExplicitSet() const { + return this->getOption(explicitOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getTransitionFilename() const { + return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString(); + } + + std::string IOSettings::getLabelingFilename() const { + return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); + } + + bool IOSettings::isSymbolicSet() const { + return this->getOption(symbolicOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getSymbolicModelFilename() const { + return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool IOSettings::isExplorationOrderSet() const { + return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); + } + + storm::builder::ExplorationOrder IOSettings::getExplorationOrder() const { + std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); + if (explorationOrderAsString == "dfs") { + return storm::builder::ExplorationOrder::Dfs; + } else if (explorationOrderAsString == "bfs") { + return storm::builder::ExplorationOrder::Bfs; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); + } + + bool IOSettings::isTransitionRewardsSet() const { + return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getTransitionRewardsFilename() const { + return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool IOSettings::isStateRewardsSet() const { + return this->getOption(stateRewardsOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getStateRewardsFilename() const { + return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool IOSettings::isChoiceLabelingSet() const { + return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getChoiceLabelingFilename() const { + return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString(); + } + + std::unique_ptr IOSettings::overridePrismCompatibilityMode(bool stateToSet) { + return this->overrideOption(prismCompatibilityOptionName, stateToSet); + } + + bool IOSettings::isConstantsSet() const { + return this->getOption(constantsOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getConstantDefinitionString() const { + return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); + } + + bool IOSettings::isPrismCompatibilityEnabled() const { + return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); + } + + void IOSettings::finalize() { + } + + bool IOSettings::check() const { + // Ensure that the model was given either symbolically or explicitly. + STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both."); + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h new file mode 100644 index 000000000..eb1ced407 --- /dev/null +++ b/src/settings/modules/IOSettings.h @@ -0,0 +1,194 @@ +#ifndef STORM_SETTINGS_MODULES_IOSETTINGS_H_ +#define STORM_SETTINGS_MODULES_IOSETTINGS_H_ + +#include "storm-config.h" +#include "src/settings/modules/ModuleSettings.h" + +#include "src/builder/ExplorationOrder.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the markov chain settings. + */ + class IOSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of IO settings. + */ + IOSettings(); + + /*! + * 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 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. + * + * @return The name of the file that contains the transitions. + */ + std::string getTransitionFilename() const; + + /*! + * Retrieves the name of the file that contains the state labeling if the model was given using the + * explicit option. + * + * @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. + * + * @return The name of the file that contains the symbolic model specification. + */ + std::string getSymbolicModelFilename() const; + + /*! + * Retrieves whether the model exploration order was set. + * + * @return True if the model exploration option was set. + */ + bool isExplorationOrderSet() const; + + /*! + * Retrieves the exploration order if it was set. + * + * @return The chosen exploration order. + */ + storm::builder::ExplorationOrder getExplorationOrder() const; + + /*! + * Retrieves whether the transition reward option was set. + * + * @return True if the transition reward option was set. + */ + bool isTransitionRewardsSet() const; + + /*! + * Retrieves the name of the file that contains the transition rewards if the model was given using the + * explicit option. + * + * @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. + * + * @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; + + /*! + * 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. + * + * @param stateToSet The value that is to be set for the option. + * @return The memento that will eventually restore the original value. + */ + std::unique_ptr overridePrismCompatibilityMode(bool stateToSet); + + /*! + * 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 the PRISM compatibility mode was enabled. + * + * @return True iff the PRISM compatibility mode was enabled. + */ + bool isPrismCompatibilityEnabled() const; + + bool check() const override; + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string exportDotOptionName; + static const std::string exportMatOptionName; + static const std::string explicitOptionName; + static const std::string explicitOptionShortName; + static const std::string symbolicOptionName; + static const std::string symbolicOptionShortName; + static const std::string explorationOrderOptionName; + static const std::string explorationOrderOptionShortName; + static const std::string transitionRewardsOptionName; + static const std::string stateRewardsOptionName; + static const std::string choiceLabelingOptionName; + static const std::string constantsOptionName; + static const std::string constantsOptionShortName; + static const std::string prismCompatibilityOptionName; + static const std::string prismCompatibilityOptionShortName; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_IOSETTINGS_H_ */ diff --git a/src/settings/modules/MarkovChainSettings.cpp b/src/settings/modules/MarkovChainSettings.cpp index 389ef664b..dc8a700d6 100644 --- a/src/settings/modules/MarkovChainSettings.cpp +++ b/src/settings/modules/MarkovChainSettings.cpp @@ -17,17 +17,6 @@ namespace storm { namespace modules { const std::string MarkovChainSettings::moduleName = "markovchain"; - const std::string MarkovChainSettings::exportDotOptionName = "exportdot"; - const std::string MarkovChainSettings::exportMatOptionName = "exportmat"; - const std::string MarkovChainSettings::explicitOptionName = "explicit"; - const std::string MarkovChainSettings::explicitOptionShortName = "exp"; - const std::string MarkovChainSettings::symbolicOptionName = "symbolic"; - const std::string MarkovChainSettings::symbolicOptionShortName = "s"; - const std::string MarkovChainSettings::explorationOrderOptionName = "explorder"; - const std::string MarkovChainSettings::explorationOrderOptionShortName = "eo"; - const std::string MarkovChainSettings::transitionRewardsOptionName = "transrew"; - const std::string MarkovChainSettings::stateRewardsOptionName = "staterew"; - const std::string MarkovChainSettings::choiceLabelingOptionName = "choicelab"; const std::string MarkovChainSettings::counterexampleOptionName = "counterexample"; const std::string MarkovChainSettings::counterexampleOptionShortName = "cex"; const std::string MarkovChainSettings::dontFixDeadlockOptionName = "nofixdl"; @@ -35,42 +24,17 @@ namespace storm { const std::string MarkovChainSettings::eqSolverOptionName = "eqsolver"; const std::string MarkovChainSettings::lpSolverOptionName = "lpsolver"; const std::string MarkovChainSettings::smtSolverOptionName = "smtsolver"; - const std::string MarkovChainSettings::constantsOptionName = "constants"; - const std::string MarkovChainSettings::constantsOptionShortName = "const"; const std::string MarkovChainSettings::statisticsOptionName = "statistics"; const std::string MarkovChainSettings::statisticsOptionShortName = "stats"; const std::string MarkovChainSettings::engineOptionName = "engine"; const std::string MarkovChainSettings::engineOptionShortName = "e"; const std::string MarkovChainSettings::ddLibraryOptionName = "ddlib"; const std::string MarkovChainSettings::cudaOptionName = "cuda"; - const std::string MarkovChainSettings::prismCompatibilityOptionName = "prismcompat"; - const std::string MarkovChainSettings::prismCompatibilityOptionShortName = "pc"; const std::string MarkovChainSettings::minMaxEquationSolvingTechniqueOptionName = "minMaxEquationSolvingTechnique"; MarkovChainSettings::MarkovChainSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportMatOptionName, "", "If given, the loaded model will be written to the specified file in the mat format.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - - std::vector explorationOrders = {"dfs", "bfs"}; - this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition 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 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", "abs"}; @@ -91,8 +55,6 @@ namespace storm { std::vector smtSolvers = {"z3", "mathsat"}; this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver. Available are: z3 and mathsat.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtSolvers)).setDefaultValueString("z3").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, cudaOptionName, false, "Sets whether to use CUDA to speed up computation time.").build()); @@ -101,72 +63,6 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique. Available are: valueIteration and policyIteration.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(minMaxSolvingTechniques)).setDefaultValueString("valueIteration").build()).build()); } - bool MarkovChainSettings::isExportDotSet() const { - return this->getOption(exportDotOptionName).getHasOptionBeenSet(); - } - - std::string MarkovChainSettings::getExportDotFilename() const { - return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool MarkovChainSettings::isExplicitSet() const { - return this->getOption(explicitOptionName).getHasOptionBeenSet(); - } - - std::string MarkovChainSettings::getTransitionFilename() const { - return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString(); - } - - std::string MarkovChainSettings::getLabelingFilename() const { - return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); - } - - bool MarkovChainSettings::isSymbolicSet() const { - return this->getOption(symbolicOptionName).getHasOptionBeenSet(); - } - - std::string MarkovChainSettings::getSymbolicModelFilename() const { - return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool MarkovChainSettings::isExplorationOrderSet() const { - return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); - } - - storm::builder::ExplorationOrder MarkovChainSettings::getExplorationOrder() const { - std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); - if (explorationOrderAsString == "dfs") { - return storm::builder::ExplorationOrder::Dfs; - } else if (explorationOrderAsString == "bfs") { - return storm::builder::ExplorationOrder::Bfs; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); - } - - bool MarkovChainSettings::isTransitionRewardsSet() const { - return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); - } - - std::string MarkovChainSettings::getTransitionRewardsFilename() const { - return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool MarkovChainSettings::isStateRewardsSet() const { - return this->getOption(stateRewardsOptionName).getHasOptionBeenSet(); - } - - std::string MarkovChainSettings::getStateRewardsFilename() const { - return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool MarkovChainSettings::isChoiceLabelingSet() const { - return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet(); - } - - std::string MarkovChainSettings::getChoiceLabelingFilename() const { - return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString(); - } - bool MarkovChainSettings::isCounterexampleSet() const { return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); } @@ -183,10 +79,6 @@ namespace storm { return this->overrideOption(dontFixDeadlockOptionName, stateToSet); } - std::unique_ptr MarkovChainSettings::overridePrismCompatibilityMode(bool stateToSet) { - return this->overrideOption(prismCompatibilityOptionName, stateToSet); - } - storm::solver::EquationSolverType MarkovChainSettings::getEquationSolver() const { std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); if (equationSolverName == "gmm++") { @@ -230,14 +122,6 @@ namespace storm { } } - bool MarkovChainSettings::isConstantsSet() const { - return this->getOption(constantsOptionName).getHasOptionBeenSet(); - } - - std::string MarkovChainSettings::getConstantDefinitionString() const { - return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); - } - bool MarkovChainSettings::isShowStatisticsSet() const { return this->getOption(statisticsOptionName).getHasOptionBeenSet(); } @@ -254,11 +138,7 @@ namespace storm { this->engine = newEngine; } - bool MarkovChainSettings::isPrismCompatibilityEnabled() const { - return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); - } - - storm::solver::MinMaxTechnique MarkovChainSettings::getMinMaxEquationSolvingTechnique() const { + storm::solver::MinMaxTechnique MarkovChainSettings::getMinMaxEquationSolvingTechnique() const { std::string minMaxEquationSolvingTechnique = this->getOption(minMaxEquationSolvingTechniqueOptionName).getArgumentByName("name").getValueAsString(); if (minMaxEquationSolvingTechnique == "valueIteration") { return storm::solver::MinMaxTechnique::ValueIteration; @@ -289,11 +169,6 @@ namespace storm { } bool MarkovChainSettings::check() const { - // Ensure that the model was given either symbolically or explicitly. - STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both."); - - STORM_LOG_THROW(this->getEngine() == Engine::Sparse || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Cannot use explicit input models with this engine."); - return true; } diff --git a/src/settings/modules/MarkovChainSettings.h b/src/settings/modules/MarkovChainSettings.h index 193b47c44..f37ea2050 100644 --- a/src/settings/modules/MarkovChainSettings.h +++ b/src/settings/modules/MarkovChainSettings.h @@ -36,117 +36,6 @@ namespace storm { */ MarkovChainSettings(); - /*! - * 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 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. - * - * @return The name of the file that contains the transitions. - */ - std::string getTransitionFilename() const; - - /*! - * Retrieves the name of the file that contains the state labeling if the model was given using the - * explicit option. - * - * @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. - * - * @return The name of the file that contains the symbolic model specification. - */ - std::string getSymbolicModelFilename() const; - - /*! - * Retrieves whether the model exploration order was set. - * - * @return True if the model exploration option was set. - */ - bool isExplorationOrderSet() const; - - /*! - * Retrieves the exploration order if it was set. - * - * @return The chosen exploration order. - */ - storm::builder::ExplorationOrder getExplorationOrder() const; - - /*! - * Retrieves whether the transition reward option was set. - * - * @return True if the transition reward option was set. - */ - bool isTransitionRewardsSet() const; - - /*! - * Retrieves the name of the file that contains the transition rewards if the model was given using the - * explicit option. - * - * @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. - * - * @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. * @@ -178,15 +67,6 @@ namespace storm { */ 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. - * - * @param stateToSet The value that is to be set for the option. - * @return The memento that will eventually restore the original value. - */ - std::unique_ptr overridePrismCompatibilityMode(bool stateToSet); - /*! * Retrieves the selected equation solver. * @@ -222,20 +102,6 @@ namespace storm { */ storm::dd::DdType getDdLibraryType() 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. * @@ -262,13 +128,6 @@ namespace storm { */ void setEngine(Engine); - /*! - * Retrieves whether the PRISM compatibility mode was enabled. - * - * @return True iff the PRISM compatibility mode was enabled. - */ - bool isPrismCompatibilityEnabled() const; - /*! * Retrieves whether a min/max equation solving technique has been set. * @@ -294,17 +153,6 @@ namespace storm { Engine engine; // Define the string names of the options as constants. - static const std::string exportDotOptionName; - static const std::string exportMatOptionName; - static const std::string explicitOptionName; - static const std::string explicitOptionShortName; - static const std::string symbolicOptionName; - static const std::string symbolicOptionShortName; - static const std::string explorationOrderOptionName; - static const std::string explorationOrderOptionShortName; - 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; @@ -312,16 +160,12 @@ namespace storm { static const std::string eqSolverOptionName; static const std::string lpSolverOptionName; static const std::string smtSolverOptionName; - static const std::string constantsOptionName; - static const std::string constantsOptionShortName; static const std::string statisticsOptionName; static const std::string statisticsOptionShortName; static const std::string engineOptionName; static const std::string engineOptionShortName; static const std::string ddLibraryOptionName; static const std::string cudaOptionName; - static const std::string prismCompatibilityOptionName; - static const std::string prismCompatibilityOptionShortName; static const std::string minMaxEquationSolvingTechniqueOptionName; }; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 229f205f5..ce3662610 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -6,7 +6,7 @@ #include "src/storage/expressions/ExpressionManager.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/utility/macros.h" #include "src/utility/solver.h" #include "src/exceptions/InvalidArgumentException.h" @@ -56,7 +56,7 @@ namespace storm { // If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian // commands and issue a warning. - if (modelType == storm::prism::Program::ModelType::CTMC && storm::settings::getModule().isPrismCompatibilityEnabled()) { + if (modelType == storm::prism::Program::ModelType::CTMC && storm::settings::getModule().isPrismCompatibilityEnabled()) { bool hasProbabilisticCommands = false; for (auto& module : this->modules) { for (auto& command : module.getCommands()) { @@ -829,7 +829,7 @@ namespace storm { } if (hasLabeledMarkovianCommand) { - if (storm::settings::getModule().isPrismCompatibilityEnabled()) { + if (storm::settings::getModule().isPrismCompatibilityEnabled()) { STORM_LOG_WARN_COND(false, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics."); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics."); diff --git a/src/utility/storm.h b/src/utility/storm.h index 59f640bdf..df84e79d6 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -21,6 +21,7 @@ #include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/ParametricSettings.h" @@ -96,7 +97,7 @@ namespace storm { storm::prism::Program translatedProgram; // Get the string that assigns values to the unknown currently undefined constants in the model. - std::string constants = storm::settings::getModule().getConstantDefinitionString(); + std::string constants = storm::settings::getModule().getConstantDefinitionString(); // Customize and perform model-building. if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) { @@ -223,7 +224,7 @@ namespace storm { void generateCounterexample(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); - STORM_LOG_THROW(storm::settings::getModule().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models."); + STORM_LOG_THROW(storm::settings::getModule().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models."); std::shared_ptr> mdp = model->template as>(); @@ -233,7 +234,7 @@ namespace storm { if (useMILP) { storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, formula); + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, formula); } } else { diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index 9f1f66cf2..9e5607761 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "src/settings/SettingMemento.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" @@ -68,7 +68,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -99,7 +99,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { TEST(DdPrismModelBuilderTest_Cudd, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index 634c106ee..73675a25c 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -5,7 +5,7 @@ #include "src/parser/PrismParser.h" #include "src/builder/ExplicitPrismModelBuilder.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" TEST(ExplicitPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); @@ -37,7 +37,7 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) { TEST(ExplicitPrismModelBuilderTest, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 7a28ad892..628662788 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -13,14 +13,14 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -103,7 +103,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -172,7 +172,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { TEST(GmmxxCtmcCslModelCheckerTest, Polling) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -206,14 +206,14 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { TEST(GmmxxCtmcCslModelCheckerTest, Fms) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // No properties to check at this point. } TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 51a3a7bc9..2be79d79f 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -16,14 +16,14 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -120,7 +120,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Cudd) { TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -217,7 +217,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -296,7 +296,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Cudd) { TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -375,7 +375,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -411,7 +411,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Cudd) { TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -447,14 +447,14 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling_Sylvan) { TEST(GmmxxHybridCtmcCslModelCheckerTest, Fms) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // No properties to check at this point. } TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); @@ -542,7 +542,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Cudd) { TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index afa0e7e25..640c904c5 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -14,11 +14,11 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GeneralSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" TEST(NativeCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -94,7 +94,7 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { TEST(NativeCtmcCslModelCheckerTest, Embedded) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -156,7 +156,7 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { TEST(NativeCtmcCslModelCheckerTest, Polling) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -183,14 +183,14 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { TEST(NativeCtmcCslModelCheckerTest, Fms) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // No properties to check at this point. } TEST(NativeCtmcCslModelCheckerTest, Tandem) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 3bfa011cb..7b7fd6030 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -16,13 +16,13 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/IOSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -119,7 +119,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) { TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -216,7 +216,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) { TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -295,7 +295,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) { TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -374,7 +374,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) { TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -410,7 +410,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) { TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -446,14 +446,14 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) { TEST(NativeHybridCtmcCslModelCheckerTest, Fms) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // No properties to check at this point. } TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); @@ -543,7 +543,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) { TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. - std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");