From effadc5cca878beab2cd9749c415a3380396706f Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 22 Mar 2016 13:31:09 +0100 Subject: [PATCH] Split into general settings and markov chain settings Former-commit-id: 619a2e36227e957df81b5aeeca911f6dbd307041 --- src/builder/DdPrismModelBuilder.cpp | 4 +- src/builder/ExplicitPrismModelBuilder.cpp | 10 +- src/cli/cli.cpp | 8 +- src/cli/entrypoints.h | 14 +- .../SMTMinimalCommandSetGenerator.h | 4 +- .../SparseDtmcEliminationModelChecker.cpp | 4 +- .../DeterministicSparseTransitionParser.cpp | 4 +- .../MarkovAutomatonSparseTransitionParser.cpp | 6 +- ...NondeterministicSparseTransitionParser.cpp | 4 +- src/settings/SettingsManager.cpp | 8 +- src/settings/SettingsManager.h | 22 +- .../CounterexampleGeneratorSettings.cpp | 4 +- src/settings/modules/GeneralSettings.cpp | 270 -------------- src/settings/modules/GeneralSettings.h | 295 +--------------- src/settings/modules/GlpkSettings.cpp | 6 +- .../modules/GmmxxEquationSolverSettings.cpp | 6 +- src/settings/modules/GurobiSettings.cpp | 6 +- src/settings/modules/MarkovChainSettings.cpp | 302 ++++++++++++++++ src/settings/modules/MarkovChainSettings.h | 332 ++++++++++++++++++ .../modules/NativeEquationSolverSettings.cpp | 6 +- src/solver/MinMaxLinearEquationSolver.cpp | 4 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 4 +- .../BisimulationDecomposition.cpp | 4 +- src/storage/prism/Program.cpp | 6 +- src/utility/solver.cpp | 12 +- src/utility/storm.h | 23 +- .../builder/DdPrismModelBuilderTest.cpp | 8 +- .../builder/ExplicitPrismModelBuilderTest.cpp | 6 +- .../GmmxxCtmcCslModelCheckerTest.cpp | 11 +- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 21 +- .../NativeCtmcCslModelCheckerTest.cpp | 11 +- .../NativeHybridCtmcCslModelCheckerTest.cpp | 21 +- ...eterministicSparseTransitionParserTest.cpp | 6 +- ...kovAutomatonSparseTransitionParserTest.cpp | 6 +- ...eterministicSparseTransitionParserTest.cpp | 6 +- 35 files changed, 765 insertions(+), 699 deletions(-) create mode 100644 src/settings/modules/MarkovChainSettings.cpp create mode 100644 src/settings/modules/MarkovChainSettings.h diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 7fcb209d0..208666bb7 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -20,7 +20,7 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/storage/dd/Bdd.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" namespace storm { namespace builder { @@ -1081,7 +1081,7 @@ namespace storm { if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. - if (!storm::settings::getModule().isDontFixDeadlocksSet()) { + if (!storm::settings::getModule().isDontFixDeadlocksSet()) { STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); uint_fast64_t count = 0; diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index eba19054f..77b37684e 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -9,7 +9,7 @@ #include "src/storage/expressions/ExpressionManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/generator/PrismNextStateGenerator.h" #include "src/generator/PrismStateLabelingGenerator.h" @@ -84,17 +84,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; @@ -386,7 +386,7 @@ namespace storm { // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { - if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { + if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { if (options.buildCommandLabels) { // Insert empty choice labeling for added self-loop transitions. choiceLabels.get().push_back(boost::container::flat_set()); diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 6b517e410..7ff84ef22 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -205,7 +205,7 @@ namespace storm { storm::utility::initializeFileLogging(); } - storm::settings::modules::GeneralSettings const& settings = storm::settings::getModule(); + 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; @@ -216,8 +216,8 @@ namespace storm { // Then proceed to parsing the property (if given), since the model we are building may depend on the property. std::vector> parsedFormulas; - if (settings.isPropertySet()) { - std::string properties = settings.getProperty(); + if (storm::settings::getModule().isPropertySet()) { + std::string properties = storm::settings::getModule().getProperty(); if(program) { parsedFormulas = storm::parseFormulasForProgram(properties, program.get()); @@ -230,7 +230,7 @@ namespace storm { if (settings.isSymbolicSet()) { #ifdef STORM_HAVE_CARL - if (settings.isParametricSet()) { + if (storm::settings::getModule().isParametricSet()) { buildAndCheckSymbolicModel(program.get(), formulas, true); } else { #endif diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 3e2ee0670..f1febc74e 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -114,7 +114,7 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - if (storm::settings::getModule().getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) { + if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::AbstractionRefinement) { verifySymbolicModelWithAbstractionRefinementEngine(program, formulas, onlyInitialStatesRelevant); } else { storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel(program, formulas); @@ -130,7 +130,7 @@ namespace storm { // Verify the model, if a formula was given. if (!formulas.empty()) { if (modelFormulasPair.model->isSparseModel()) { - if (storm::settings::getModule().isCounterexampleSet()) { + if (storm::settings::getModule().isCounterexampleSet()) { // If we were requested to generate a counterexample, we now do so for each formula. for (auto const &formula : modelFormulasPair.formulas) { generateCounterexample(program, modelFormulasPair.model->as>(), formula); @@ -139,7 +139,7 @@ namespace storm { verifySparseModel(modelFormulasPair.model->as>(), modelFormulasPair.formulas, onlyInitialStatesRelevant); } } else if (modelFormulasPair.model->isSymbolicModel()) { - if (storm::settings::getModule().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { + if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as>(), modelFormulasPair.formulas, onlyInitialStatesRelevant); } else { @@ -155,18 +155,18 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - if (storm::settings::getModule().getDdLibraryType() == storm::dd::DdType::CUDD) { + if (storm::settings::getModule().getDdLibraryType() == storm::dd::DdType::CUDD) { buildAndCheckSymbolicModel(program, formulas, onlyInitialStatesRelevant); - } else if (storm::settings::getModule().getDdLibraryType() == storm::dd::DdType::Sylvan) { + } else if (storm::settings::getModule().getDdLibraryType() == storm::dd::DdType::Sylvan) { buildAndCheckSymbolicModel(program, formulas, onlyInitialStatesRelevant); } } template void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - storm::settings::modules::GeneralSettings const& settings = storm::settings::getModule(); + storm::settings::modules::MarkovChainSettings const& settings = storm::settings::getModule(); - STORM_LOG_THROW(storm::settings::getModule().isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); + 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); // Preprocess the model if needed. diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index ed84d7b10..048808763 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -12,7 +12,7 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/solver/GmmxxMinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/utility/counterexamples.h" #include "src/utility/prism.h" @@ -1729,7 +1729,7 @@ namespace storm { // Compute and emit the time measurements if the corresponding flag was set. totalTime = std::chrono::high_resolution_clock::now() - totalClock; - if (storm::settings::getModule().isShowStatisticsSet()) { + if (storm::settings::getModule().isShowStatisticsSet()) { std::cout << std::endl; std::cout << "Time breakdown:" << std::endl; std::cout << " * time for setup: " << std::chrono::duration_cast(totalSetupTime).count() << "ms" << std::endl; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 1b6cbda98..ac3254dd4 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -7,7 +7,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/SettingsManager.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" @@ -330,7 +330,7 @@ namespace storm { std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); - if (storm::settings::getModule().isShowStatisticsSet()) { + if (storm::settings::getModule().isShowStatisticsSet()) { std::chrono::high_resolution_clock::duration sccDecompositionTime = sccDecompositionEnd - sccDecompositionStart; std::chrono::milliseconds sccDecompositionTimeInMilliseconds = std::chrono::duration_cast(sccDecompositionTime); std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index efc91643a..db63f509f 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -14,7 +14,7 @@ #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/adapters/CarlAdapter.h" #include "src/utility/macros.h" @@ -88,7 +88,7 @@ namespace storm { uint_fast64_t row, col, lastRow = 0; double val; - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); bool hadDeadlocks = false; bool rowHadDiagonalEntry = false; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 7ea2dd611..5a9fcfb84 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -1,7 +1,7 @@ #include "MarkovAutomatonSparseTransitionParser.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" #include "src/parser/MappedFile.h" @@ -17,7 +17,7 @@ namespace storm { typename MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char const* buf) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); // Skip the format hint if it is there. buf = trimWhitespaces(buf); @@ -160,7 +160,7 @@ namespace storm { typename MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char const* buf, FirstPassResult const& firstPassResult) { Result result(firstPassResult); - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); // Skip the format hint if it is there. buf = trimWhitespaces(buf); diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 2f40a7425..2186b4929 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -4,7 +4,7 @@ #include "src/parser/MappedFile.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/OutOfRangeException.h" @@ -96,7 +96,7 @@ namespace storm { // Initialize variables for the parsing run. uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0; double val = 0.0; - bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); bool hadDeadlocks = false; // The first state already starts a new row group of the matrix. diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index bb1883209..853b5c3e1 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -14,6 +14,7 @@ #include "src/exceptions/OptionParserException.h" #include "src/utility/storm-version.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/CounterexampleGeneratorSettings.h" #include "src/settings/modules/CuddSettings.h" @@ -484,8 +485,8 @@ namespace storm { return SettingsManager::manager(); } - storm::settings::modules::GeneralSettings& mutableGeneralSettings() { - return dynamic_cast(mutableManager().getModule(storm::settings::modules::GeneralSettings::moduleName)); + storm::settings::modules::MarkovChainSettings& mutableMarkovChainSettings() { + return dynamic_cast(mutableManager().getModule(storm::settings::modules::MarkovChainSettings::moduleName)); } void initializeAll(std::string const& name, std::string const& executableName) { @@ -493,6 +494,7 @@ namespace storm { // Register all known settings modules. storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); @@ -508,4 +510,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 69d91899f..5b0141045 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -12,19 +12,7 @@ namespace storm { namespace settings { namespace modules { - class GeneralSettings; - class DebugSettings; - class CounterexampleGeneratorSettings; - class CuddSettings; - class SylvanSettings; - class GmmxxEquationSolverSettings; - class NativeEquationSolverSettings; - class BisimulationSettings; - class GlpkSettings; - class GurobiSettings; - class TopologicalValueIterationEquationSolverSettings; - class ParametricSettings; - class SparseDtmcEliminationModelCheckerSettings; + class MarkovChainSettings; class ModuleSettings; } class Option; @@ -277,14 +265,14 @@ namespace storm { } /*! - * Retrieves the general settings in a mutable form. This is only meant to be used for debug purposes or very + * Retrieves the markov chain 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 general settings. + * @return An object that allows accessing and modifying the markov chain settings. */ - storm::settings::modules::GeneralSettings& mutableGeneralSettings(); + storm::settings::modules::MarkovChainSettings& mutableMarkovChainSettings(); } // namespace settings } // namespace storm -#endif /* STORM_SETTINGS_SETTINGSMANAGER_H_ */ \ No newline at end of file +#endif /* STORM_SETTINGS_SETTINGSMANAGER_H_ */ diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp index 79b57e756..6c245d3b2 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/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 0b477d667..778c2a705 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -24,43 +24,14 @@ namespace storm { const std::string GeneralSettings::verboseOptionShortName = "v"; const std::string GeneralSettings::precisionOptionName = "precision"; const std::string GeneralSettings::precisionOptionShortName = "eps"; - const std::string GeneralSettings::exportDotOptionName = "exportdot"; - const std::string GeneralSettings::exportMatOptionName = "exportmat"; const std::string GeneralSettings::configOptionName = "config"; const std::string GeneralSettings::configOptionShortName = "c"; - const std::string GeneralSettings::explicitOptionName = "explicit"; - const std::string GeneralSettings::explicitOptionShortName = "exp"; - const std::string GeneralSettings::symbolicOptionName = "symbolic"; - const std::string GeneralSettings::symbolicOptionShortName = "s"; - const std::string GeneralSettings::explorationOrderOptionName = "explorder"; - const std::string GeneralSettings::explorationOrderOptionShortName = "eo"; const std::string GeneralSettings::propertyOptionName = "prop"; 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"; - const std::string GeneralSettings::dontFixDeadlockOptionShortName = "ndl"; const std::string GeneralSettings::timeoutOptionName = "timeout"; const std::string GeneralSettings::timeoutOptionShortName = "t"; - const std::string GeneralSettings::eqSolverOptionName = "eqsolver"; - const std::string GeneralSettings::lpSolverOptionName = "lpsolver"; - const std::string GeneralSettings::smtSolverOptionName = "smtsolver"; - const std::string GeneralSettings::constantsOptionName = "constants"; - const std::string GeneralSettings::constantsOptionShortName = "const"; - const std::string GeneralSettings::statisticsOptionName = "statistics"; - const std::string GeneralSettings::statisticsOptionShortName = "stats"; const std::string GeneralSettings::bisimulationOptionName = "bisimulation"; const std::string GeneralSettings::bisimulationOptionShortName = "bisim"; - const std::string GeneralSettings::engineOptionName = "engine"; - const std::string GeneralSettings::engineOptionShortName = "e"; - const std::string GeneralSettings::ddLibraryOptionName = "ddlib"; - const std::string GeneralSettings::cudaOptionName = "cuda"; - const std::string GeneralSettings::prismCompatibilityOptionName = "prismcompat"; - const std::string GeneralSettings::prismCompatibilityOptionShortName = "pc"; - const std::string GeneralSettings::minMaxEquationSolvingTechniqueOptionName = "minMaxEquationSolvingTechnique"; #ifdef STORM_HAVE_CARL const std::string GeneralSettings::parametricOptionName = "parametric"; @@ -69,69 +40,17 @@ namespace storm { GeneralSettings::GeneralSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build()); - 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, versionOptionName, false, "Prints the version information.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).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, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).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, propertyOptionName, false, "Specifies the formulas to be checked on the model.").setShortName(propertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula or filename", "The formula or the file containing the formulas.").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, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).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"}; - this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, ar}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); - - std::vector linearEquationSolver = {"gmm++", "native"}; - this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build()); - std::vector ddLibraries = {"cudd", "sylvan"}; - this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer. Available are: cudd and sylvan.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(ddLibraries)).setDefaultValueString("cudd").build()).build()); - - std::vector lpSolvers = {"gurobi", "glpk"}; - this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); - 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()); - - std::vector minMaxSolvingTechniques = {"policyIteration", "valueIteration"}; - this->addOption(storm::settings::OptionBuilder(moduleName, minMaxEquationSolvingTechniqueOptionName, false, "Sets which min/max linear equation solving technique is preferred.") - .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()); - #ifdef STORM_HAVE_CARL this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build()); #endif @@ -157,14 +76,6 @@ namespace storm { return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } - bool GeneralSettings::isExportDotSet() const { - return this->getOption(exportDotOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getExportDotFilename() const { - return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); - } - bool GeneralSettings::isConfigSet() const { return this->getOption(configOptionName).getHasOptionBeenSet(); } @@ -173,40 +84,6 @@ namespace storm { return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString(); } - bool GeneralSettings::isExplicitSet() const { - return this->getOption(explicitOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getTransitionFilename() const { - return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString(); - } - - std::string GeneralSettings::getLabelingFilename() const { - return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); - } - - bool GeneralSettings::isSymbolicSet() const { - return this->getOption(symbolicOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getSymbolicModelFilename() const { - return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool GeneralSettings::isExplorationOrderSet() const { - return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); - } - - storm::builder::ExplorationOrder GeneralSettings::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 GeneralSettings::isPropertySet() const { return this->getOption(propertyOptionName).getHasOptionBeenSet(); } @@ -215,50 +92,6 @@ namespace storm { return this->getOption(propertyOptionName).getArgumentByName("formula or filename").getValueAsString(); } - bool GeneralSettings::isTransitionRewardsSet() const { - return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getTransitionRewardsFilename() const { - return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool GeneralSettings::isStateRewardsSet() const { - return this->getOption(stateRewardsOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getStateRewardsFilename() const { - 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(); - } - - std::string GeneralSettings::getCounterexampleFilename() const { - return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString(); - } - - bool GeneralSettings::isDontFixDeadlocksSet() const { - return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); - } - - std::unique_ptr GeneralSettings::overrideDontFixDeadlocksSet(bool stateToSet) { - return this->overrideOption(dontFixDeadlockOptionName, stateToSet); - } - - std::unique_ptr GeneralSettings::overridePrismCompatibilityMode(bool stateToSet) { - return this->overrideOption(prismCompatibilityOptionName, stateToSet); - } - bool GeneralSettings::isTimeoutSet() const { return this->getOption(timeoutOptionName).getHasOptionBeenSet(); } @@ -267,91 +100,10 @@ namespace storm { return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger(); } - storm::solver::EquationSolverType GeneralSettings::getEquationSolver() const { - std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); - if (equationSolverName == "gmm++") { - return storm::solver::EquationSolverType::Gmmxx; - } else if (equationSolverName == "native") { - return storm::solver::EquationSolverType::Native; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); - } - - bool GeneralSettings::isEquationSolverSet() const { - return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); - } - - storm::solver::LpSolverType GeneralSettings::getLpSolver() const { - std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); - if (lpSolverName == "gurobi") { - return storm::solver::LpSolverType::Gurobi; - } else if (lpSolverName == "glpk") { - return storm::solver::LpSolverType::Glpk; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); - } - - storm::solver::SmtSolverType GeneralSettings::getSmtSolver() const { - std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString(); - if (smtSolverName == "z3") { - return storm::solver::SmtSolverType::Z3; - } else if (smtSolverName == "mathsat") { - return storm::solver::SmtSolverType::Mathsat; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'."); - } - - storm::dd::DdType GeneralSettings::getDdLibraryType() const { - std::string ddLibraryAsString = this->getOption(ddLibraryOptionName).getArgumentByName("name").getValueAsString(); - if (ddLibraryAsString == "sylvan") { - return storm::dd::DdType::Sylvan; - } else { - return storm::dd::DdType::CUDD; - } - } - - bool GeneralSettings::isConstantsSet() const { - return this->getOption(constantsOptionName).getHasOptionBeenSet(); - } - - std::string GeneralSettings::getConstantDefinitionString() const { - return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); - } - - bool GeneralSettings::isShowStatisticsSet() const { - return this->getOption(statisticsOptionName).getHasOptionBeenSet(); - } - bool GeneralSettings::isBisimulationSet() const { return this->getOption(bisimulationOptionName).getHasOptionBeenSet(); } - GeneralSettings::Engine GeneralSettings::getEngine() const { - return engine; - } - - void GeneralSettings::setEngine(Engine newEngine) { - this->engine = newEngine; - } - - bool GeneralSettings::isPrismCompatibilityEnabled() const { - return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); - } - - storm::solver::MinMaxTechnique GeneralSettings::getMinMaxEquationSolvingTechnique() const { - std::string minMaxEquationSolvingTechnique = this->getOption(minMaxEquationSolvingTechniqueOptionName).getArgumentByName("name").getValueAsString(); - if (minMaxEquationSolvingTechnique == "valueIteration") { - return storm::solver::MinMaxTechnique::ValueIteration; - } else if (minMaxEquationSolvingTechnique == "policyIteration") { - return storm::solver::MinMaxTechnique::PolicyIteration; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); - } - - bool GeneralSettings::isMinMaxEquationSolvingTechniqueSet() const { - return this->getOption(minMaxEquationSolvingTechniqueOptionName).getHasOptionBeenSet(); - } - #ifdef STORM_HAVE_CARL bool GeneralSettings::isParametricSet() const { return this->getOption(parametricOptionName).getHasOptionBeenSet(); @@ -359,33 +111,11 @@ namespace storm { #endif void GeneralSettings::finalize() { - // Finalize engine. - std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString(); - if (engineStr == "sparse") { - engine = GeneralSettings::Engine::Sparse; - } else if (engineStr == "hybrid") { - engine = GeneralSettings::Engine::Hybrid; - } else if (engineStr == "dd") { - engine = GeneralSettings::Engine::Dd; - } else if (engineStr == "abs") { - engine = GeneralSettings::Engine::AbstractionRefinement; - } else { - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'."); - } } bool GeneralSettings::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; } - - bool GeneralSettings::isCudaSet() const { - return this->getOption(cudaOptionName).getHasOptionBeenSet(); - } } // namespace modules } // namespace settings diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index cf8a9318e..1f7bf3445 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -7,17 +7,6 @@ #include "src/builder/ExplorationOrder.h" namespace storm { - namespace solver { - enum class EquationSolverType; - enum class LpSolverType; - enum class MinMaxTechnique; - enum class SmtSolverType; - } - - namespace dd { - enum class DdType; - } - namespace settings { namespace modules { @@ -26,10 +15,6 @@ namespace storm { */ class GeneralSettings : public ModuleSettings { public: - // An enumeration of all engines. - enum class Engine { - Sparse, Hybrid, Dd, AbstractionRefinement - }; /*! * Creates a new set of general settings. @@ -72,20 +57,6 @@ namespace storm { */ 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. * @@ -100,58 +71,6 @@ namespace storm { */ 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. - * - * @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 property option was set. * @@ -166,91 +85,6 @@ namespace storm { */ std::string getProperty() 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. - * - * @return True if the counterexample option was set. - */ - bool isCounterexampleSet() const; - - /*! - * Retrieves the name of the file to which the counterexample is to be written if the counterexample - * option was set. - * - * @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. - * - * @return True if the dont-fix-deadlocks option was set. - */ - bool isDontFixDeadlocksSet() const; - - /*! - * Overrides the option to not fix deadlocks by setting it to the specified value. As soon as the - * returned memento goes out of scope, the original value is restored. - * - * @param stateToSet The value that is to be set for the fix-deadlocks option. - * @return The memento that will eventually restore the original value. - */ - std::unique_ptr 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 whether the timeout option was set. * @@ -265,62 +99,6 @@ namespace storm { */ uint_fast64_t getTimeoutInSeconds() const; - /*! - * Retrieves the selected equation solver. - * - * @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 the selected SMT solver. - * - * @return The selected SMT solver. - */ - storm::solver::SmtSolverType getSmtSolver() const; - - /*! - * Retrieves the selected library for DD-related operations. - * - * @return The selected library. - */ - 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. - * - * @return True iff statistics are to be shown for counterexample generation. - */ - bool isShowStatisticsSet() const; - /*! * Retrieves whether the option to perform bisimulation minimization is set. * @@ -328,32 +106,6 @@ namespace storm { */ bool isBisimulationSet() const; - /*! - * Retrieves whether the option to use CUDA is set. - * - * @return True iff the option was set. - */ - bool isCudaSet() const; - - /*! - * Retrieves the selected engine. - * - * @return The selected engine. - */ - Engine getEngine() const; - - /*! - * Sets the engine for further usage. - */ - void setEngine(Engine); - - /*! - * 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. @@ -362,21 +114,7 @@ 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; - - + bool check() const override; void finalize() override; @@ -384,8 +122,6 @@ namespace storm { static const std::string moduleName; private: - Engine engine; - // Define the string names of the options as constants. static const std::string helpOptionName; static const std::string helpOptionShortName; @@ -394,43 +130,14 @@ namespace storm { static const std::string verboseOptionShortName; static const std::string precisionOptionName; static const std::string precisionOptionShortName; - static const std::string exportDotOptionName; - static const std::string exportMatOptionName; static const std::string configOptionName; static const std::string configOptionShortName; - 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 propertyOptionName; 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; - static const std::string dontFixDeadlockOptionShortName; static const std::string timeoutOptionName; static const std::string timeoutOptionShortName; - 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 bisimulationOptionName; static const std::string bisimulationOptionShortName; - 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; #ifdef STORM_HAVE_CARL static const std::string parametricOptionName; diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp index 824f855ed..188c196eb 100644 --- a/src/settings/modules/GlpkSettings.cpp +++ b/src/settings/modules/GlpkSettings.cpp @@ -5,7 +5,7 @@ #include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/solver/SolverSelectionOptions.h" namespace storm { @@ -35,7 +35,7 @@ namespace storm { bool GlpkSettings::check() const { if (isOutputSet() || isIntegerToleranceSet()) { - STORM_LOG_WARN_COND(storm::settings::getModule().getLpSolver() == storm::solver::LpSolverType::Glpk, "glpk is not selected as the preferred LP solver, so setting options for glpk might have no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule().getLpSolver() == storm::solver::LpSolverType::Glpk, "glpk is not selected as the preferred LP solver, so setting options for glpk might have no effect."); } return true; @@ -43,4 +43,4 @@ namespace storm { } // namespace modules } // namespace settings -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp index bfc4770f1..cc81fb6f5 100644 --- a/src/settings/modules/GmmxxEquationSolverSettings.cpp +++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/solver/SolverSelectionOptions.h" namespace storm { @@ -109,11 +109,11 @@ namespace storm { // This list does not include the precision, because this option is shared with other modules. bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "gmm++ is not selected as the preferred equation solver, so setting options for gmm++ might have no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "gmm++ is not selected as the preferred equation solver, so setting options for gmm++ might have no effect."); return true; } } // namespace modules } // namespace settings -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp index d27a6c8a0..412578fe0 100644 --- a/src/settings/modules/GurobiSettings.cpp +++ b/src/settings/modules/GurobiSettings.cpp @@ -5,7 +5,7 @@ #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -46,7 +46,7 @@ namespace storm { bool GurobiSettings::check() const { if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) { - STORM_LOG_WARN_COND(storm::settings::getModule().getLpSolver() == storm::solver::LpSolverType::Gurobi, "Gurobi is not selected as the preferred LP solver, so setting options for Gurobi might have no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule().getLpSolver() == storm::solver::LpSolverType::Gurobi, "Gurobi is not selected as the preferred LP solver, so setting options for Gurobi might have no effect."); } return true; @@ -54,4 +54,4 @@ namespace storm { } // namespace modules } // namespace settings -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/settings/modules/MarkovChainSettings.cpp b/src/settings/modules/MarkovChainSettings.cpp new file mode 100644 index 000000000..389ef664b --- /dev/null +++ b/src/settings/modules/MarkovChainSettings.cpp @@ -0,0 +1,302 @@ +#include "src/settings/modules/MarkovChainSettings.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/solver/SolverSelectionOptions.h" + +#include "src/storage/dd/DdType.h" + +#include "src/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + 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"; + const std::string MarkovChainSettings::dontFixDeadlockOptionShortName = "ndl"; + 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"}; + this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, ar}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build()); + + std::vector linearEquationSolver = {"gmm++", "native"}; + this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); + + std::vector ddLibraries = {"cudd", "sylvan"}; + this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer. Available are: cudd and sylvan.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(ddLibraries)).setDefaultValueString("cudd").build()).build()); + + std::vector lpSolvers = {"gurobi", "glpk"}; + this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); + 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()); + + std::vector minMaxSolvingTechniques = {"policyIteration", "valueIteration"}; + this->addOption(storm::settings::OptionBuilder(moduleName, minMaxEquationSolvingTechniqueOptionName, false, "Sets which min/max linear equation solving technique is preferred.") + .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(); + } + + std::string MarkovChainSettings::getCounterexampleFilename() const { + return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool MarkovChainSettings::isDontFixDeadlocksSet() const { + return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); + } + + std::unique_ptr MarkovChainSettings::overrideDontFixDeadlocksSet(bool stateToSet) { + 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++") { + return storm::solver::EquationSolverType::Gmmxx; + } else if (equationSolverName == "native") { + return storm::solver::EquationSolverType::Native; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); + } + + bool MarkovChainSettings::isEquationSolverSet() const { + return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); + } + + storm::solver::LpSolverType MarkovChainSettings::getLpSolver() const { + std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); + if (lpSolverName == "gurobi") { + return storm::solver::LpSolverType::Gurobi; + } else if (lpSolverName == "glpk") { + return storm::solver::LpSolverType::Glpk; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); + } + + storm::solver::SmtSolverType MarkovChainSettings::getSmtSolver() const { + std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString(); + if (smtSolverName == "z3") { + return storm::solver::SmtSolverType::Z3; + } else if (smtSolverName == "mathsat") { + return storm::solver::SmtSolverType::Mathsat; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'."); + } + + storm::dd::DdType MarkovChainSettings::getDdLibraryType() const { + std::string ddLibraryAsString = this->getOption(ddLibraryOptionName).getArgumentByName("name").getValueAsString(); + if (ddLibraryAsString == "sylvan") { + return storm::dd::DdType::Sylvan; + } else { + return storm::dd::DdType::CUDD; + } + } + + 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(); + } + + bool MarkovChainSettings::isCudaSet() const { + return this->getOption(cudaOptionName).getHasOptionBeenSet(); + } + + MarkovChainSettings::Engine MarkovChainSettings::getEngine() const { + return engine; + } + + void MarkovChainSettings::setEngine(Engine newEngine) { + this->engine = newEngine; + } + + bool MarkovChainSettings::isPrismCompatibilityEnabled() const { + return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); + } + + storm::solver::MinMaxTechnique MarkovChainSettings::getMinMaxEquationSolvingTechnique() const { + std::string minMaxEquationSolvingTechnique = this->getOption(minMaxEquationSolvingTechniqueOptionName).getArgumentByName("name").getValueAsString(); + if (minMaxEquationSolvingTechnique == "valueIteration") { + return storm::solver::MinMaxTechnique::ValueIteration; + } else if (minMaxEquationSolvingTechnique == "policyIteration") { + return storm::solver::MinMaxTechnique::PolicyIteration; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); + } + + bool MarkovChainSettings::isMinMaxEquationSolvingTechniqueSet() const { + return this->getOption(minMaxEquationSolvingTechniqueOptionName).getHasOptionBeenSet(); + } + + void MarkovChainSettings::finalize() { + // Finalize engine. + std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString(); + if (engineStr == "sparse") { + engine = MarkovChainSettings::Engine::Sparse; + } else if (engineStr == "hybrid") { + engine = MarkovChainSettings::Engine::Hybrid; + } else if (engineStr == "dd") { + engine = MarkovChainSettings::Engine::Dd; + } else if (engineStr == "abs") { + engine = MarkovChainSettings::Engine::AbstractionRefinement; + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'."); + } + } + + 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; + } + + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/MarkovChainSettings.h b/src/settings/modules/MarkovChainSettings.h new file mode 100644 index 000000000..193b47c44 --- /dev/null +++ b/src/settings/modules/MarkovChainSettings.h @@ -0,0 +1,332 @@ +#ifndef STORM_SETTINGS_MODULES_MARKOVCHAINSETTINGS_H_ +#define STORM_SETTINGS_MODULES_MARKOVCHAINSETTINGS_H_ + +#include "storm-config.h" +#include "src/settings/modules/ModuleSettings.h" + +#include "src/builder/ExplorationOrder.h" + +namespace storm { + namespace solver { + enum class EquationSolverType; + enum class LpSolverType; + enum class MinMaxTechnique; + enum class SmtSolverType; + } + + namespace dd { + enum class DdType; + } + + namespace settings { + namespace modules { + + /*! + * This class represents the markov chain settings. + */ + class MarkovChainSettings : public ModuleSettings { + public: + // An enumeration of all engines. + enum class Engine { + Sparse, Hybrid, Dd, AbstractionRefinement + }; + + /*! + * Creates a new set of markov chain settings. + */ + 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. + * + * @return True if the counterexample option was set. + */ + bool isCounterexampleSet() const; + + /*! + * Retrieves the name of the file to which the counterexample is to be written if the counterexample + * option was set. + * + * @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. + * + * @return True if the dont-fix-deadlocks option was set. + */ + bool isDontFixDeadlocksSet() const; + + /*! + * Overrides the option to not fix deadlocks by setting it to the specified value. As soon as the + * returned memento goes out of scope, the original value is restored. + * + * @param stateToSet The value that is to be set for the fix-deadlocks option. + * @return The memento that will eventually restore the original value. + */ + std::unique_ptr 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. + * + * @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 the selected SMT solver. + * + * @return The selected SMT solver. + */ + storm::solver::SmtSolverType getSmtSolver() const; + + /*! + * Retrieves the selected library for DD-related operations. + * + * @return The selected library. + */ + 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. + * + * @return True iff statistics are to be shown for counterexample generation. + */ + bool isShowStatisticsSet() const; + + /*! + * Retrieves whether the option to use CUDA is set. + * + * @return True iff the option was set. + */ + bool isCudaSet() const; + + /*! + * Retrieves the selected engine. + * + * @return The selected engine. + */ + Engine getEngine() const; + + /*! + * Sets the engine for further usage. + */ + 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. + * + * @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; + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + private: + 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; + static const std::string dontFixDeadlockOptionShortName; + 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; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_MARKOVCHAINSETTINGS_H_ */ diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp index abc1860ee..251e7f1aa 100644 --- a/src/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/settings/modules/NativeEquationSolverSettings.cpp @@ -1,7 +1,7 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/Option.h" #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" @@ -81,11 +81,11 @@ namespace storm { // This list does not include the precision, because this option is shared with other modules. bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Native || !optionSet, "Native is not selected as the preferred equation solver, so setting options for native might have no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Native || !optionSet, "Native is not selected as the preferred equation solver, so setting options for native might have no effect."); return true; } } // namespace modules } // namespace settings -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 13bec6708..dea71fe58 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -1,6 +1,6 @@ #include "MinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" @@ -12,7 +12,7 @@ namespace storm { AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech) : precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackScheduler(trackScheduler) { if(prefTech == MinMaxTechniqueSelection::FROMSETTINGS) { - useValueIteration = (storm::settings::getModule().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); + useValueIteration = (storm::settings::getModule().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); } else { useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration); } diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index 4e34826a1..0140fec1d 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -9,7 +9,7 @@ #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" @@ -27,7 +27,7 @@ namespace storm { NativeMinMaxLinearEquationSolver(A, storm::settings::getModule().getPrecision(), storm::settings::getModule().getMaximalIterationCount(), MinMaxTechniqueSelection::ValueIteration, storm::settings::getModule().getConvergenceCriterion() == storm::settings::modules::TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative) { // Get the settings object to customize solving. - this->enableCuda = storm::settings::getModule().isCudaSet(); + this->enableCuda = storm::settings::getModule().isCudaSet(); #ifdef STORM_HAVE_CUDA STORM_LOG_INFO_COND(this->enableCuda, "Option CUDA was not set, but the topological value iteration solver will use it anyways."); #endif diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 048622c26..fb6a6c759 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -13,7 +13,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/logic/FormulaInformation.h" #include "src/logic/FragmentSpecification.h" @@ -210,7 +210,7 @@ namespace storm { std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; - if (storm::settings::getModule().isShowStatisticsSet()) { + if (storm::settings::getModule().isShowStatisticsSet()) { std::chrono::milliseconds initialPartitionTimeInMilliseconds = std::chrono::duration_cast(initialPartitionTime); std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast(refinementTime); std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast(extractionTime); diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 4137bec09..229f205f5 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/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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/solver.cpp b/src/utility/solver.cpp index 5709e1f58..77f644949 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -19,7 +19,7 @@ #include "src/solver/Z3SmtSolver.h" #include "src/solver/MathsatSmtSolver.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/exceptions/InvalidSettingsException.h" @@ -46,7 +46,7 @@ namespace storm { template std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); switch (equationSolver) { case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); case storm::solver::EquationSolverType::Native: return std::unique_ptr>(new storm::solver::NativeLinearEquationSolver(matrix)); @@ -93,7 +93,7 @@ namespace storm { template MinMaxLinearEquationSolverFactory& MinMaxLinearEquationSolverFactory::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) { - this->solverType = storm::settings::getModule().getEquationSolver(); + this->solverType = storm::settings::getModule().getEquationSolver(); } else { this->solverType = storm::solver::convert(solverTypeSel); } @@ -140,7 +140,7 @@ namespace storm { std::unique_ptr LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { - t = storm::settings::getModule().getLpSolver(); + t = storm::settings::getModule().getLpSolver(); } else { t = convert(solvT); } @@ -168,7 +168,7 @@ namespace storm { } std::unique_ptr SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { - storm::solver::SmtSolverType smtSolverType = storm::settings::getModule().getSmtSolver(); + storm::solver::SmtSolverType smtSolverType = storm::settings::getModule().getSmtSolver(); switch (smtSolverType) { case storm::solver::SmtSolverType::Z3: return std::unique_ptr(new storm::solver::Z3SmtSolver(manager)); case storm::solver::SmtSolverType::Mathsat: return std::unique_ptr(new storm::solver::MathsatSmtSolver(manager)); @@ -201,4 +201,4 @@ namespace storm { template class GameSolverFactory; } } -} \ No newline at end of file +} diff --git a/src/utility/storm.h b/src/utility/storm.h index 64f43fe0f..59f640bdf 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -20,6 +20,7 @@ #include "src/settings/SettingsManager.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/ParametricSettings.h" @@ -95,10 +96,10 @@ 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::GeneralSettings::Engine::Sparse) { + if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) { typename storm::builder::ExplicitPrismModelBuilder>::Options options; options = typename storm::builder::ExplicitPrismModelBuilder>::Options(formulas); options.addConstantDefinitionsFromString(program, constants); @@ -111,7 +112,7 @@ namespace storm { storm::builder::ExplicitPrismModelBuilder builder(program, options); result.model = builder.translate(); translatedProgram = builder.getTranslatedProgram(); - } else if (storm::settings::getModule().getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || storm::settings::getModule().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { + } else if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, constants); @@ -222,7 +223,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>(); @@ -232,7 +233,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 { @@ -249,23 +250,23 @@ namespace storm { template std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { - switch(storm::settings::getModule().getEngine()) { - case storm::settings::modules::GeneralSettings::Engine::Sparse: { + switch(storm::settings::getModule().getEngine()) { + case storm::settings::modules::MarkovChainSettings::Engine::Sparse: { std::shared_ptr> sparseModel = model->template as>(); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant); } - case storm::settings::modules::GeneralSettings::Engine::Hybrid: { + case storm::settings::modules::MarkovChainSettings::Engine::Hybrid: { std::shared_ptr> ddModel = model->template as>(); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model"); return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant); } - case storm::settings::modules::GeneralSettings::Engine::Dd: { + case storm::settings::modules::MarkovChainSettings::Engine::Dd: { std::shared_ptr> ddModel = model->template as>(); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model"); return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant); } - case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: { + case storm::settings::modules::MarkovChainSettings::Engine::AbstractionRefinement: { STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built."); } } @@ -292,7 +293,7 @@ namespace storm { } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr> mdp = model->template as>(); #ifdef STORM_HAVE_CUDA - if (storm::settings::getModule().isCudaSet()) { + if (storm::settings::getModule().isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); result = modelchecker.check(task); } else { diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index 102b7fb2a..9f1f66cf2 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/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -250,4 +250,4 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(37ul, mdp->getNumberOfStates()); EXPECT_EQ(59ul, mdp->getNumberOfTransitions()); EXPECT_EQ(59ul, mdp->getNumberOfChoices()); -} \ No newline at end of file +} diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index c2151c74c..634c106ee 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/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -97,4 +97,4 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) { model = storm::builder::ExplicitPrismModelBuilder(program).translate(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 73c16edb1..7a28ad892 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -13,13 +13,14 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -102,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -171,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -205,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 a128b4802..51a3a7bc9 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -16,13 +16,14 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 +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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 +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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 +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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 +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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 +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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 +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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); @@ -541,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); @@ -625,4 +626,4 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); -} \ No newline at end of file +} diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 6c94f0007..afa0e7e25 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -14,10 +14,11 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -93,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -155,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -182,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 d4b0fb9a5..3bfa011cb 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -16,12 +16,13 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -118,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); @@ -215,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -294,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); @@ -373,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -409,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); @@ -445,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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().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 +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::mutableGeneralSettings().overridePrismCompatibilityMode(true); + std::unique_ptr enablePrismCompatibility = storm::settings::mutableMarkovChainSettings().overridePrismCompatibilityMode(true); // Parse the model description. storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); @@ -628,4 +629,4 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) { // FIXME: because of divergence, these results are not correct. // EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMin(), storm::settings::getModule().getPrecision()); // EXPECT_NEAR(0.9100373532, quantitativeCheckResult7.getMax(), storm::settings::getModule().getPrecision()); -} \ No newline at end of file +} diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp index 50b545d25..3f40c1edb 100644 --- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp @@ -11,7 +11,7 @@ #include "src/parser/DeterministicSparseTransitionParser.h" #include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/settings/SettingMemento.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" @@ -193,7 +193,7 @@ TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) { TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr fixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"); @@ -217,7 +217,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr dontFixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException); } diff --git a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp index 4246c5b3d..e6cb09e54 100644 --- a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include @@ -187,7 +187,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) { TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr fixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(false); // Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works. typename storm::parser::MarkovAutomatonSparseTransitionParser<>::Result result = storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"); @@ -206,7 +206,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr dontFixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"), storm::exceptions::WrongFormatException); } diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp index c5c0807bc..f177eaf40 100644 --- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -13,7 +13,7 @@ #include "src/settings/SettingMemento.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" @@ -212,7 +212,7 @@ TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) { TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { // Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. - std::unique_ptr fixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr fixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra")); @@ -253,7 +253,7 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. - std::unique_ptr dontFixDeadlocks = storm::settings::mutableGeneralSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr dontFixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException); }