diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 2fe35e2c6..9397ed925 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -21,7 +21,7 @@ #include "src/models/symbolic/StandardRewardModel.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/utility/macros.h" #include "src/utility/jani.h" @@ -1677,7 +1677,7 @@ namespace storm { if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. - if (!storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet()) { + if (!storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) { STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); storm::dd::Add<Type, ValueType> deadlockStatesAdd = deadlockStates.template toAdd<ValueType>(); diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 1f38fa4a8..2af7fed58 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -24,7 +24,7 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/storage/dd/Bdd.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" namespace storm { namespace builder { @@ -1335,7 +1335,7 @@ namespace storm { // If there are deadlocks, either fix them or raise an error. if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. - if (!storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet()) { + if (!storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) { STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); storm::dd::Add<Type, ValueType> deadlockStatesAdd = deadlockStates.template toAdd<ValueType>(); diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index f5cb33aca..f008321ee 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -9,7 +9,7 @@ #include "src/storage/expressions/ExpressionManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/IOSettings.h" #include "src/generator/PrismNextStateGenerator.h" @@ -209,7 +209,7 @@ namespace storm { // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { - if (!storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { + if (!storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { // If the behavior was actually expanded and yet there are no transitions, then we have a deadlock state. if (behavior.wasExpanded()) { this->stateStorage.deadlockStateIndices.push_back(currentIndex); diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 4207ca722..c9e88410d 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -5,7 +5,7 @@ #include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/IOSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/exceptions/OptionParserException.h" #include "src/utility/storm-version.h" @@ -236,7 +236,7 @@ namespace storm { buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true); } } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) { - STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input."); + STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input."); // If the model is given in an explicit format, we parse the properties without allowing expressions // in formulas. diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 84b7fb753..c2990b072 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -189,7 +189,7 @@ namespace storm { std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>(); // Finally, treat the formulas. - if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isCounterexampleSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCounterexampleSet()) { generateCounterexamples<ValueType>(program, sparseModel, formulas); } else { verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant); @@ -198,26 +198,26 @@ namespace storm { template<typename ValueType> void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { - if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::AbstractionRefinement) { - auto ddlib = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getDdLibraryType(); + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { + auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType(); if (ddlib == storm::dd::DdType::CUDD) { verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant); } else { verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant); } - } else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Exploration) { + } else if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Exploration) { verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant); } else { - auto engine = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine(); - if (engine == storm::settings::modules::MarkovChainSettings::Engine::Dd || engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { - auto ddlib = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getDdLibraryType(); + auto engine = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine(); + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType(); if (ddlib == storm::dd::DdType::CUDD) { - buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant); + buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant); } else { - buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan>(engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant); + buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant); } } else { - STORM_LOG_THROW(engine == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine."); + STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine."); buildAndCheckSymbolicModelWithSparseEngine<ValueType>(program, formulas, onlyInitialStatesRelevant); } @@ -226,13 +226,13 @@ namespace storm { template<> void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { - STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); + STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(program, formulas, onlyInitialStatesRelevant); } template<> void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { - STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); + STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(program, formulas, onlyInitialStatesRelevant); } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index ee0613fca..3caed5f22 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.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<storm::settings::modules::MarkovChainSettings>().isShowStatisticsSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { std::cout << std::endl; std::cout << "Time breakdown:" << std::endl; std::cout << " * time for setup: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalSetupTime).count() << "ms" << std::endl; diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp index dba541891..b98a3ca7c 100644 --- a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -19,7 +19,7 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/ExplorationSettings.h" #include "src/utility/macros.h" @@ -113,7 +113,7 @@ namespace storm { } // Show statistics if required. - if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isShowStatisticsSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { stats.printToStream(std::cout, explorationInformation); } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 9d774a6ec..e6f0bbb2d 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/EliminationSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/SettingsManager.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" @@ -292,7 +292,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<storm::settings::modules::MarkovChainSettings>().isShowStatisticsSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { std::chrono::high_resolution_clock::duration sccDecompositionTime = sccDecompositionEnd - sccDecompositionStart; std::chrono::milliseconds sccDecompositionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(sccDecompositionTime); std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index db63f509f..298396e7b 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.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<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet(); bool hadDeadlocks = false; bool rowHadDiagonalEntry = false; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 43f8aed64..ed3046a11 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" #include "src/parser/MappedFile.h" @@ -18,7 +18,7 @@ namespace storm { typename MarkovAutomatonSparseTransitionParser<ValueType>::FirstPassResult MarkovAutomatonSparseTransitionParser<ValueType>::firstPass(char const* buf) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; - bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet(); // Skip the format hint if it is there. buf = trimWhitespaces(buf); @@ -171,7 +171,7 @@ namespace storm { typename MarkovAutomatonSparseTransitionParser<ValueType>::Result MarkovAutomatonSparseTransitionParser<ValueType>::secondPass(char const* buf, FirstPassResult const& firstPassResult) { Result result(firstPassResult); - bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::CoreSettings>().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 2186b4929..ff22c77ee 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.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<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet(); + bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::CoreSettings>().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 434327b16..c88f7017f 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -14,7 +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/CoreSettings.h" #include "src/settings/modules/IOSettings.h" #include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/CounterexampleGeneratorSettings.h" @@ -489,8 +489,8 @@ namespace storm { return SettingsManager::manager(); } - storm::settings::modules::MarkovChainSettings& mutableMarkovChainSettings() { - return dynamic_cast<storm::settings::modules::MarkovChainSettings&>(mutableManager().getModule(storm::settings::modules::MarkovChainSettings::moduleName)); + storm::settings::modules::CoreSettings& mutableCoreSettings() { + return dynamic_cast<storm::settings::modules::CoreSettings&>(mutableManager().getModule(storm::settings::modules::CoreSettings::moduleName)); } storm::settings::modules::IOSettings& mutableIOSettings() { @@ -503,7 +503,7 @@ namespace storm { // Register all known settings modules. storm::settings::addModule<storm::settings::modules::GeneralSettings>(); storm::settings::addModule<storm::settings::modules::IOSettings>(); - storm::settings::addModule<storm::settings::modules::MarkovChainSettings>(); + storm::settings::addModule<storm::settings::modules::CoreSettings>(); storm::settings::addModule<storm::settings::modules::DebugSettings>(); storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(); storm::settings::addModule<storm::settings::modules::CuddSettings>(); diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 0efdcd2fd..11c9d78d6 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -12,7 +12,7 @@ namespace storm { namespace settings { namespace modules { - class MarkovChainSettings; + class CoreSettings; class IOSettings; class ModuleSettings; } @@ -271,7 +271,7 @@ namespace storm { * * @return An object that allows accessing and modifying the markov chain settings. */ - storm::settings::modules::MarkovChainSettings& mutableMarkovChainSettings(); + storm::settings::modules::CoreSettings& mutableCoreSettings(); /*! * Retrieves the IO settings in a mutable form. This is only meant to be used for debug purposes or very diff --git a/src/settings/modules/MarkovChainSettings.cpp b/src/settings/modules/CoreSettings.cpp similarity index 75% rename from src/settings/modules/MarkovChainSettings.cpp rename to src/settings/modules/CoreSettings.cpp index 2db5dbca7..dc6babef8 100644 --- a/src/settings/modules/MarkovChainSettings.cpp +++ b/src/settings/modules/CoreSettings.cpp @@ -1,4 +1,4 @@ -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/SettingsManager.h" #include "src/settings/SettingMemento.h" @@ -16,23 +16,23 @@ namespace storm { namespace settings { namespace modules { - const std::string MarkovChainSettings::moduleName = "markovchain"; - 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::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::minMaxEquationSolvingTechniqueOptionName = "minMaxEquationSolvingTechnique"; + const std::string CoreSettings::moduleName = "core"; + const std::string CoreSettings::counterexampleOptionName = "counterexample"; + const std::string CoreSettings::counterexampleOptionShortName = "cex"; + const std::string CoreSettings::dontFixDeadlockOptionName = "nofixdl"; + const std::string CoreSettings::dontFixDeadlockOptionShortName = "ndl"; + const std::string CoreSettings::eqSolverOptionName = "eqsolver"; + const std::string CoreSettings::lpSolverOptionName = "lpsolver"; + const std::string CoreSettings::smtSolverOptionName = "smtsolver"; + const std::string CoreSettings::statisticsOptionName = "statistics"; + const std::string CoreSettings::statisticsOptionShortName = "stats"; + const std::string CoreSettings::engineOptionName = "engine"; + const std::string CoreSettings::engineOptionShortName = "e"; + const std::string CoreSettings::ddLibraryOptionName = "ddlib"; + const std::string CoreSettings::cudaOptionName = "cuda"; + const std::string CoreSettings::minMaxEquationSolvingTechniqueOptionName = "minMaxEquationSolvingTechnique"; - MarkovChainSettings::MarkovChainSettings() : ModuleSettings(moduleName) { + CoreSettings::CoreSettings() : ModuleSettings(moduleName) { 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, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build()); @@ -63,23 +63,23 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique. Available are: valueIteration and policyIteration.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(minMaxSolvingTechniques)).setDefaultValueString("valueIteration").build()).build()); } - bool MarkovChainSettings::isCounterexampleSet() const { + bool CoreSettings::isCounterexampleSet() const { return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); } - std::string MarkovChainSettings::getCounterexampleFilename() const { + std::string CoreSettings::getCounterexampleFilename() const { return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString(); } - bool MarkovChainSettings::isDontFixDeadlocksSet() const { + bool CoreSettings::isDontFixDeadlocksSet() const { return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); } - std::unique_ptr<storm::settings::SettingMemento> MarkovChainSettings::overrideDontFixDeadlocksSet(bool stateToSet) { + std::unique_ptr<storm::settings::SettingMemento> CoreSettings::overrideDontFixDeadlocksSet(bool stateToSet) { return this->overrideOption(dontFixDeadlockOptionName, stateToSet); } - storm::solver::EquationSolverType MarkovChainSettings::getEquationSolver() const { + storm::solver::EquationSolverType CoreSettings::getEquationSolver() const { std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); if (equationSolverName == "gmm++") { return storm::solver::EquationSolverType::Gmmxx; @@ -93,11 +93,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); } - bool MarkovChainSettings::isEquationSolverSet() const { + bool CoreSettings::isEquationSolverSet() const { return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); } - storm::solver::LpSolverType MarkovChainSettings::getLpSolver() const { + storm::solver::LpSolverType CoreSettings::getLpSolver() const { std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); if (lpSolverName == "gurobi") { return storm::solver::LpSolverType::Gurobi; @@ -107,7 +107,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); } - storm::solver::SmtSolverType MarkovChainSettings::getSmtSolver() const { + storm::solver::SmtSolverType CoreSettings::getSmtSolver() const { std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString(); if (smtSolverName == "z3") { return storm::solver::SmtSolverType::Z3; @@ -117,7 +117,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'."); } - storm::dd::DdType MarkovChainSettings::getDdLibraryType() const { + storm::dd::DdType CoreSettings::getDdLibraryType() const { std::string ddLibraryAsString = this->getOption(ddLibraryOptionName).getArgumentByName("name").getValueAsString(); if (ddLibraryAsString == "sylvan") { return storm::dd::DdType::Sylvan; @@ -126,23 +126,23 @@ namespace storm { } } - bool MarkovChainSettings::isShowStatisticsSet() const { + bool CoreSettings::isShowStatisticsSet() const { return this->getOption(statisticsOptionName).getHasOptionBeenSet(); } - bool MarkovChainSettings::isCudaSet() const { + bool CoreSettings::isCudaSet() const { return this->getOption(cudaOptionName).getHasOptionBeenSet(); } - MarkovChainSettings::Engine MarkovChainSettings::getEngine() const { + CoreSettings::Engine CoreSettings::getEngine() const { return engine; } - void MarkovChainSettings::setEngine(Engine newEngine) { + void CoreSettings::setEngine(Engine newEngine) { this->engine = newEngine; } - storm::solver::MinMaxTechnique MarkovChainSettings::getMinMaxEquationSolvingTechnique() const { + storm::solver::MinMaxTechnique CoreSettings::getMinMaxEquationSolvingTechnique() const { std::string minMaxEquationSolvingTechnique = this->getOption(minMaxEquationSolvingTechniqueOptionName).getArgumentByName("name").getValueAsString(); if (minMaxEquationSolvingTechnique == "valueIteration") { return storm::solver::MinMaxTechnique::ValueIteration; @@ -152,29 +152,29 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); } - bool MarkovChainSettings::isMinMaxEquationSolvingTechniqueSet() const { + bool CoreSettings::isMinMaxEquationSolvingTechniqueSet() const { return this->getOption(minMaxEquationSolvingTechniqueOptionName).getHasOptionBeenSet(); } - void MarkovChainSettings::finalize() { + void CoreSettings::finalize() { // Finalize engine. std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString(); if (engineStr == "sparse") { - engine = MarkovChainSettings::Engine::Sparse; + engine = CoreSettings::Engine::Sparse; } else if (engineStr == "hybrid") { - engine = MarkovChainSettings::Engine::Hybrid; + engine = CoreSettings::Engine::Hybrid; } else if (engineStr == "dd") { - engine = MarkovChainSettings::Engine::Dd; + engine = CoreSettings::Engine::Dd; } else if (engineStr == "expl") { - engine = MarkovChainSettings::Engine::Exploration; + engine = CoreSettings::Engine::Exploration; } else if (engineStr == "abs") { - engine = MarkovChainSettings::Engine::AbstractionRefinement; + engine = CoreSettings::Engine::AbstractionRefinement; } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'."); } } - bool MarkovChainSettings::check() const { + bool CoreSettings::check() const { return true; } diff --git a/src/settings/modules/MarkovChainSettings.h b/src/settings/modules/CoreSettings.h similarity index 95% rename from src/settings/modules/MarkovChainSettings.h rename to src/settings/modules/CoreSettings.h index 5f8fe2153..204081dd2 100644 --- a/src/settings/modules/MarkovChainSettings.h +++ b/src/settings/modules/CoreSettings.h @@ -1,5 +1,5 @@ -#ifndef STORM_SETTINGS_MODULES_MARKOVCHAINSETTINGS_H_ -#define STORM_SETTINGS_MODULES_MARKOVCHAINSETTINGS_H_ +#ifndef STORM_SETTINGS_MODULES_CoreSettings_H_ +#define STORM_SETTINGS_MODULES_CoreSettings_H_ #include "storm-config.h" #include "src/settings/modules/ModuleSettings.h" @@ -24,7 +24,7 @@ namespace storm { /*! * This class represents the markov chain settings. */ - class MarkovChainSettings : public ModuleSettings { + class CoreSettings : public ModuleSettings { public: // An enumeration of all engines. enum class Engine { @@ -34,7 +34,7 @@ namespace storm { /*! * Creates a new set of markov chain settings. */ - MarkovChainSettings(); + CoreSettings(); /*! * Retrieves whether the counterexample option was set. @@ -173,4 +173,4 @@ namespace storm { } // namespace settings } // namespace storm -#endif /* STORM_SETTINGS_MODULES_MARKOVCHAINSETTINGS_H_ */ +#endif /* STORM_SETTINGS_MODULES_CoreSettings_H_ */ diff --git a/src/settings/modules/EigenEquationSolverSettings.cpp b/src/settings/modules/EigenEquationSolverSettings.cpp index f61b0414c..f66d48c9a 100644 --- a/src/settings/modules/EigenEquationSolverSettings.cpp +++ b/src/settings/modules/EigenEquationSolverSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/solver/SolverSelectionOptions.h" namespace storm { @@ -98,7 +98,7 @@ namespace storm { // This list does not include the precision, because this option is shared with other modules. bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isMaximalIterationCountSet(); - STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "eigen is not selected as the preferred equation solver, so setting options for eigen might have no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "eigen is not selected as the preferred equation solver, so setting options for eigen might have no effect."); return true; } diff --git a/src/settings/modules/ExplorationSettings.cpp b/src/settings/modules/ExplorationSettings.cpp index c7fb3140c..18db2d43a 100644 --- a/src/settings/modules/ExplorationSettings.cpp +++ b/src/settings/modules/ExplorationSettings.cpp @@ -1,5 +1,5 @@ #include "src/settings/modules/ExplorationSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/Option.h" #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" @@ -88,7 +88,7 @@ namespace storm { this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet(); - STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect."); + STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect."); return true; } } // namespace modules diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp index 188c196eb..562022e08 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.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<storm::settings::modules::MarkovChainSettings>().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<storm::settings::modules::CoreSettings>().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; diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp index cc81fb6f5..938aa3b79 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/solver/SolverSelectionOptions.h" namespace storm { @@ -109,7 +109,7 @@ 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<storm::settings::modules::MarkovChainSettings>().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<storm::settings::modules::CoreSettings>().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; } diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp index 412578fe0..b9ea6402d 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.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<storm::settings::modules::MarkovChainSettings>().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<storm::settings::modules::CoreSettings>().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; diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp index 251e7f1aa..9f1915cbc 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/Option.h" #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" @@ -81,7 +81,7 @@ 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<storm::settings::modules::MarkovChainSettings>().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<storm::settings::modules::CoreSettings>().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; } diff --git a/src/solver/LinearEquationSolver.cpp b/src/solver/LinearEquationSolver.cpp index 801855765..e6a780350 100644 --- a/src/solver/LinearEquationSolver.cpp +++ b/src/solver/LinearEquationSolver.cpp @@ -8,7 +8,7 @@ #include "src/solver/EliminationLinearEquationSolver.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" namespace storm { namespace solver { @@ -31,7 +31,7 @@ namespace storm { template<typename ValueType> template<typename MatrixType> std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::selectSolver(MatrixType&& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver(); switch (equationSolver) { case storm::solver::EquationSolverType::Gmmxx: return std::make_unique<storm::solver::GmmxxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix)); case storm::solver::EquationSolverType::Native: return std::make_unique<storm::solver::NativeLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix)); @@ -51,7 +51,7 @@ namespace storm { template<typename MatrixType> std::unique_ptr<storm::solver::LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::selectSolver(MatrixType&& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver(); switch (equationSolver) { case storm::solver::EquationSolverType::Elimination: return std::make_unique<storm::solver::EliminationLinearEquationSolver<storm::RationalNumber>>(matrix); default: return std::make_unique<storm::solver::EigenLinearEquationSolver<storm::RationalNumber>>(matrix); @@ -68,7 +68,7 @@ namespace storm { template<typename MatrixType> std::unique_ptr<storm::solver::LinearEquationSolver<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::selectSolver(MatrixType&& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver(); switch (equationSolver) { case storm::solver::EquationSolverType::Elimination: return std::make_unique<storm::solver::EliminationLinearEquationSolver<storm::RationalFunction>>(matrix); default: return std::make_unique<storm::solver::EigenLinearEquationSolver<storm::RationalFunction>>(matrix); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index dea71fe58..0390b7453 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" @@ -12,7 +12,7 @@ namespace storm { AbstractMinMaxLinearEquationSolver<ValueType>::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<storm::settings::modules::MarkovChainSettings>().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); + useValueIteration = (storm::settings::getModule<storm::settings::modules::CoreSettings>().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); } else { useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration); } diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index 2f6e51de1..16cd70627 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -9,7 +9,7 @@ #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" @@ -27,7 +27,7 @@ namespace storm { NativeMinMaxLinearEquationSolver<ValueType>(A, storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision(), storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getMaximalIterationCount(), MinMaxTechniqueSelection::ValueIteration, storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getConvergenceCriterion() == storm::settings::modules::TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative) { // Get the settings object to customize solving. - this->enableCuda = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isCudaSet(); + this->enableCuda = storm::settings::getModule<storm::settings::modules::CoreSettings>().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 751708e24..30fc5a2c9 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.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<storm::settings::modules::MarkovChainSettings>().isShowStatisticsSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) { std::chrono::milliseconds initialPartitionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(initialPartitionTime); std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime); std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime); diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 4dd7bdbe3..6b6f74d46 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -9,7 +9,7 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/DFTSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/DebugSettings.h" //#include "src/settings/modules/CounterexampleGeneratorSettings.h" //#include "src/settings/modules/CuddSettings.h" @@ -53,7 +53,7 @@ void initializeSettings() { // Register all known settings modules. storm::settings::addModule<storm::settings::modules::GeneralSettings>(); storm::settings::addModule<storm::settings::modules::DFTSettings>(); - storm::settings::addModule<storm::settings::modules::MarkovChainSettings>(); + storm::settings::addModule<storm::settings::modules::CoreSettings>(); storm::settings::addModule<storm::settings::modules::DebugSettings>(); //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(); //storm::settings::addModule<storm::settings::modules::CuddSettings>(); diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index cafe63565..d0d3beab9 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -21,7 +21,7 @@ #include "src/solver/Z3SmtSolver.h" #include "src/solver/MathsatSmtSolver.h" #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/exceptions/InvalidSettingsException.h" @@ -56,7 +56,7 @@ namespace storm { template<typename ValueType> MinMaxLinearEquationSolverFactory<ValueType>& MinMaxLinearEquationSolverFactory<ValueType>::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) { - this->solverType = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver(); + this->solverType = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver(); } else { this->solverType = storm::solver::convert(solverTypeSel); } @@ -103,7 +103,7 @@ namespace storm { std::unique_ptr<storm::solver::LpSolver> 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<storm::settings::modules::MarkovChainSettings>().getLpSolver(); + t = storm::settings::getModule<storm::settings::modules::CoreSettings>().getLpSolver(); } else { t = convert(solvT); } @@ -131,7 +131,7 @@ namespace storm { } std::unique_ptr<storm::solver::SmtSolver> SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { - storm::solver::SmtSolverType smtSolverType = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getSmtSolver(); + storm::solver::SmtSolverType smtSolverType = storm::settings::getModule<storm::settings::modules::CoreSettings>().getSmtSolver(); switch (smtSolverType) { case storm::solver::SmtSolverType::Z3: return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Z3SmtSolver(manager)); case storm::solver::SmtSolverType::Mathsat: return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::MathsatSmtSolver(manager)); diff --git a/src/utility/storm.h b/src/utility/storm.h index a623e04b6..aee9bca9e 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -17,12 +17,12 @@ // Headers that provide auxiliary functionality. #include "src/settings/SettingsManager.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/IOSettings.h" #include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/ParametricSettings.h" #include "src/settings/modules/EliminationSettings.h" -#include "src/settings/modules/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" // Formula headers. #include "src/logic/Formulas.h" @@ -239,18 +239,18 @@ namespace storm { template<typename ValueType, storm::dd::DdType DdType> std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) { - switch(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine()) { - case storm::settings::modules::MarkovChainSettings::Engine::Sparse: { + switch(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine()) { + case storm::settings::modules::CoreSettings::Engine::Sparse: { std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>(); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant); } - case storm::settings::modules::MarkovChainSettings::Engine::Hybrid: { + case storm::settings::modules::CoreSettings::Engine::Hybrid: { std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>(); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model"); return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant); } - case storm::settings::modules::MarkovChainSettings::Engine::Dd: { + case storm::settings::modules::CoreSettings::Engine::Dd: { std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>(); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model"); return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant); @@ -267,7 +267,7 @@ namespace storm { storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>(); - if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) { storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); @@ -285,7 +285,7 @@ namespace storm { } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>(); #ifdef STORM_HAVE_CUDA - if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isCudaSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp); result = modelchecker.check(task); } else { @@ -324,7 +324,7 @@ namespace storm { if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalNumber>>(); - if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) { storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); @@ -370,7 +370,7 @@ namespace storm { if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(); - if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) { + if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule<storm::settings::modules::EliminationSettings>().isUseDedicatedModelCheckerSet()) { storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp index 25306def2..b2fb76bf2 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/settings/SettingMemento.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" @@ -191,7 +191,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<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"); @@ -215,7 +215,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<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableCoreSettings().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 e6cb09e54..2e312510b 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include <vector> @@ -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<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableCoreSettings().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<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableCoreSettings().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 ab53fa4b6..21975c20d 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/MarkovChainSettings.h" +#include "src/settings/modules/CoreSettings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" @@ -210,7 +210,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<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(false); + std::unique_ptr<storm::settings::SettingMemento> fixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(false); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra")); @@ -251,7 +251,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<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableMarkovChainSettings().overrideDontFixDeadlocksSet(true); + std::unique_ptr<storm::settings::SettingMemento> dontFixDeadlocks = storm::settings::mutableCoreSettings().overrideDontFixDeadlocksSet(true); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException); }