sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

renamed MarkovChainSettings 

Former-commit-id: 39024731f8
main
dehnert 9 years ago
parent
5616004e6e
commit
2a7dc0fad0
31 changed files with 130 additions and 130 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/builder/DdJaniModelBuilder.cpp
  2. 4
      src/builder/DdPrismModelBuilder.cpp
  3. 4
      src/builder/ExplicitModelBuilder.cpp
  4. 4
      src/cli/cli.cpp
  5. 24
      src/cli/entrypoints.h
  6. 4
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  7. 4
      src/modelchecker/exploration/SparseExplorationModelChecker.cpp
  8. 4
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  9. 4
      src/parser/DeterministicSparseTransitionParser.cpp
  10. 6
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  11. 4
      src/parser/NondeterministicSparseTransitionParser.cpp
  12. 8
      src/settings/SettingsManager.cpp
  13. 4
      src/settings/SettingsManager.h
  14. 80
      src/settings/modules/CoreSettings.cpp
  15. 10
      src/settings/modules/CoreSettings.h
  16. 4
      src/settings/modules/EigenEquationSolverSettings.cpp
  17. 4
      src/settings/modules/ExplorationSettings.cpp
  18. 4
      src/settings/modules/GlpkSettings.cpp
  19. 4
      src/settings/modules/GmmxxEquationSolverSettings.cpp
  20. 4
      src/settings/modules/GurobiSettings.cpp
  21. 4
      src/settings/modules/NativeEquationSolverSettings.cpp
  22. 8
      src/solver/LinearEquationSolver.cpp
  23. 4
      src/solver/MinMaxLinearEquationSolver.cpp
  24. 4
      src/solver/TopologicalMinMaxLinearEquationSolver.cpp
  25. 4
      src/storage/bisimulation/BisimulationDecomposition.cpp
  26. 4
      src/storm-dyftee.cpp
  27. 8
      src/utility/solver.cpp
  28. 20
      src/utility/storm.h
  29. 6
      test/functional/parser/DeterministicSparseTransitionParserTest.cpp
  30. 6
      test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
  31. 6
      test/functional/parser/NondeterministicSparseTransitionParserTest.cpp

4
src/builder/DdJaniModelBuilder.cpp
View File

@ -21,7 +21,7 @@
#include "src/models/symbolic/StandardRewardModel.h" #include "src/models/symbolic/StandardRewardModel.h"
#include "src/settings/SettingsManager.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/macros.h"
#include "src/utility/jani.h" #include "src/utility/jani.h"
@ -1677,7 +1677,7 @@ namespace storm {
if (!deadlockStates.isZero()) { if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now. // 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_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>(); storm::dd::Add<Type, ValueType> deadlockStatesAdd = deadlockStates.template toAdd<ValueType>();

4
src/builder/DdPrismModelBuilder.cpp
View File

@ -24,7 +24,7 @@
#include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/storage/dd/cudd/CuddAddIterator.h"
#include "src/storage/dd/Bdd.h" #include "src/storage/dd/Bdd.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
namespace storm { namespace storm {
namespace builder { namespace builder {
@ -1335,7 +1335,7 @@ namespace storm {
// If there are deadlocks, either fix them or raise an error. // If there are deadlocks, either fix them or raise an error.
if (!deadlockStates.isZero()) { if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now. // 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_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>(); storm::dd::Add<Type, ValueType> deadlockStatesAdd = deadlockStates.template toAdd<ValueType>();

4
src/builder/ExplicitModelBuilder.cpp
View File

@ -9,7 +9,7 @@
#include "src/storage/expressions/ExpressionManager.h" #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/settings/modules/IOSettings.h"
#include "src/generator/PrismNextStateGenerator.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 there is no behavior, we might have to introduce a self-loop.
if (behavior.empty()) { 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 the behavior was actually expanded and yet there are no transitions, then we have a deadlock state.
if (behavior.wasExpanded()) { if (behavior.wasExpanded()) {
this->stateStorage.deadlockStateIndices.push_back(currentIndex); this->stateStorage.deadlockStateIndices.push_back(currentIndex);

4
src/cli/cli.cpp
View File

@ -5,7 +5,7 @@
#include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/DebugSettings.h"
#include "src/settings/modules/IOSettings.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/exceptions/OptionParserException.h"
#include "src/utility/storm-version.h" #include "src/utility/storm-version.h"
@ -236,7 +236,7 @@ namespace storm {
buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true); buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true);
} }
} else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) { } 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 // If the model is given in an explicit format, we parse the properties without allowing expressions
// in formulas. // in formulas.

24
src/cli/entrypoints.h
View File

@ -189,7 +189,7 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>(); std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
// Finally, treat the formulas. // 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); generateCounterexamples<ValueType>(program, sparseModel, formulas);
} else { } else {
verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant); verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant);
@ -198,26 +198,26 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { 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) { if (ddlib == storm::dd::DdType::CUDD) {
verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant); verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant);
} else { } else {
verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant); 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); verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
} else { } 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) { 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 { } 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 { } 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); buildAndCheckSymbolicModelWithSparseEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
} }
@ -226,13 +226,13 @@ namespace storm {
template<> template<>
void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { 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); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(program, formulas, onlyInitialStatesRelevant);
} }
template<> template<>
void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { 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); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(program, formulas, onlyInitialStatesRelevant);
} }

4
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -12,7 +12,7 @@
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/solver/GmmxxMinMaxLinearEquationSolver.h" #include "src/solver/GmmxxMinMaxLinearEquationSolver.h"
#include "src/settings/SettingsManager.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/counterexamples.h"
#include "src/utility/prism.h" #include "src/utility/prism.h"
@ -1729,7 +1729,7 @@ namespace storm {
// Compute and emit the time measurements if the corresponding flag was set. // Compute and emit the time measurements if the corresponding flag was set.
totalTime = std::chrono::high_resolution_clock::now() - totalClock; 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 << std::endl;
std::cout << "Time breakdown:" << 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; std::cout << " * time for setup: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalSetupTime).count() << "ms" << std::endl;

4
src/modelchecker/exploration/SparseExplorationModelChecker.cpp
View File

@ -19,7 +19,7 @@
#include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/StandardRewardModel.h"
#include "src/settings/SettingsManager.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/settings/modules/ExplorationSettings.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
@ -113,7 +113,7 @@ namespace storm {
} }
// Show statistics if required. // 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); stats.printToStream(std::cout, explorationInformation);
} }

4
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -7,7 +7,7 @@
#include "src/adapters/CarlAdapter.h" #include "src/adapters/CarlAdapter.h"
#include "src/settings/modules/EliminationSettings.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/settings/SettingsManager.h"
#include "src/storage/StronglyConnectedComponentDecomposition.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 modelCheckingEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point totalTimeEnd = 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::high_resolution_clock::duration sccDecompositionTime = sccDecompositionEnd - sccDecompositionStart;
std::chrono::milliseconds sccDecompositionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(sccDecompositionTime); std::chrono::milliseconds sccDecompositionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(sccDecompositionTime);
std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart;

4
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -14,7 +14,7 @@
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "src/settings/SettingsManager.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/adapters/CarlAdapter.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
@ -88,7 +88,7 @@ namespace storm {
uint_fast64_t row, col, lastRow = 0; uint_fast64_t row, col, lastRow = 0;
double val; 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 hadDeadlocks = false;
bool rowHadDiagonalEntry = false; bool rowHadDiagonalEntry = false;

6
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -1,7 +1,7 @@
#include "MarkovAutomatonSparseTransitionParser.h" #include "MarkovAutomatonSparseTransitionParser.h"
#include "src/settings/SettingsManager.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/WrongFormatException.h"
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/parser/MappedFile.h" #include "src/parser/MappedFile.h"
@ -18,7 +18,7 @@ namespace storm {
typename MarkovAutomatonSparseTransitionParser<ValueType>::FirstPassResult MarkovAutomatonSparseTransitionParser<ValueType>::firstPass(char const* buf) { typename MarkovAutomatonSparseTransitionParser<ValueType>::FirstPassResult MarkovAutomatonSparseTransitionParser<ValueType>::firstPass(char const* buf) {
MarkovAutomatonSparseTransitionParser::FirstPassResult result; 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. // Skip the format hint if it is there.
buf = trimWhitespaces(buf); buf = trimWhitespaces(buf);
@ -171,7 +171,7 @@ namespace storm {
typename MarkovAutomatonSparseTransitionParser<ValueType>::Result MarkovAutomatonSparseTransitionParser<ValueType>::secondPass(char const* buf, FirstPassResult const& firstPassResult) { typename MarkovAutomatonSparseTransitionParser<ValueType>::Result MarkovAutomatonSparseTransitionParser<ValueType>::secondPass(char const* buf, FirstPassResult const& firstPassResult) {
Result result(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. // Skip the format hint if it is there.
buf = trimWhitespaces(buf); buf = trimWhitespaces(buf);

4
src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -4,7 +4,7 @@
#include "src/parser/MappedFile.h" #include "src/parser/MappedFile.h"
#include "src/settings/SettingsManager.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/FileIoException.h"
#include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/OutOfRangeException.h"
@ -96,7 +96,7 @@ namespace storm {
// Initialize variables for the parsing run. // Initialize variables for the parsing run.
uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0; uint_fast64_t source = 0, target = 0, lastSource = 0, choice = 0, lastChoice = 0, curRow = 0;
double val = 0.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; bool hadDeadlocks = false;
// The first state already starts a new row group of the matrix. // The first state already starts a new row group of the matrix.

8
src/settings/SettingsManager.cpp
View File

@ -14,7 +14,7 @@
#include "src/exceptions/OptionParserException.h" #include "src/exceptions/OptionParserException.h"
#include "src/utility/storm-version.h" #include "src/utility/storm-version.h"
#include "src/settings/modules/GeneralSettings.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/IOSettings.h"
#include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/DebugSettings.h"
#include "src/settings/modules/CounterexampleGeneratorSettings.h" #include "src/settings/modules/CounterexampleGeneratorSettings.h"
@ -489,8 +489,8 @@ namespace storm {
return SettingsManager::manager(); 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() { storm::settings::modules::IOSettings& mutableIOSettings() {
@ -503,7 +503,7 @@ namespace storm {
// Register all known settings modules. // Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>(); storm::settings::addModule<storm::settings::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::IOSettings>(); 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::DebugSettings>();
storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(); storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
storm::settings::addModule<storm::settings::modules::CuddSettings>(); storm::settings::addModule<storm::settings::modules::CuddSettings>();

4
src/settings/SettingsManager.h
View File

@ -12,7 +12,7 @@
namespace storm { namespace storm {
namespace settings { namespace settings {
namespace modules { namespace modules {
class MarkovChainSettings;
class CoreSettings;
class IOSettings; class IOSettings;
class ModuleSettings; class ModuleSettings;
} }
@ -271,7 +271,7 @@ namespace storm {
* *
* @return An object that allows accessing and modifying the markov chain settings. * @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 * Retrieves the IO settings in a mutable form. This is only meant to be used for debug purposes or very

80
src/settings/modules/MarkovChainSettings.cpp → src/settings/modules/CoreSettings.cpp
View File

@ -1,4 +1,4 @@
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h" #include "src/settings/SettingMemento.h"
@ -16,23 +16,23 @@ namespace storm {
namespace settings { namespace settings {
namespace modules { 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";
MarkovChainSettings::MarkovChainSettings() : ModuleSettings(moduleName) {
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";
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") 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()); .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()); 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()); .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(); return this->getOption(counterexampleOptionName).getHasOptionBeenSet();
} }
std::string MarkovChainSettings::getCounterexampleFilename() const {
std::string CoreSettings::getCounterexampleFilename() const {
return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString(); return this->getOption(counterexampleOptionName).getArgumentByName("filename").getValueAsString();
} }
bool MarkovChainSettings::isDontFixDeadlocksSet() const {
bool CoreSettings::isDontFixDeadlocksSet() const {
return this->getOption(dontFixDeadlockOptionName).getHasOptionBeenSet(); 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); 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(); std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString();
if (equationSolverName == "gmm++") { if (equationSolverName == "gmm++") {
return storm::solver::EquationSolverType::Gmmxx; return storm::solver::EquationSolverType::Gmmxx;
@ -93,11 +93,11 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'.");
} }
bool MarkovChainSettings::isEquationSolverSet() const {
bool CoreSettings::isEquationSolverSet() const {
return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); 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(); std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString();
if (lpSolverName == "gurobi") { if (lpSolverName == "gurobi") {
return storm::solver::LpSolverType::Gurobi; return storm::solver::LpSolverType::Gurobi;
@ -107,7 +107,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); 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(); std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString();
if (smtSolverName == "z3") { if (smtSolverName == "z3") {
return storm::solver::SmtSolverType::Z3; return storm::solver::SmtSolverType::Z3;
@ -117,7 +117,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'."); 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(); std::string ddLibraryAsString = this->getOption(ddLibraryOptionName).getArgumentByName("name").getValueAsString();
if (ddLibraryAsString == "sylvan") { if (ddLibraryAsString == "sylvan") {
return storm::dd::DdType::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(); return this->getOption(statisticsOptionName).getHasOptionBeenSet();
} }
bool MarkovChainSettings::isCudaSet() const {
bool CoreSettings::isCudaSet() const {
return this->getOption(cudaOptionName).getHasOptionBeenSet(); return this->getOption(cudaOptionName).getHasOptionBeenSet();
} }
MarkovChainSettings::Engine MarkovChainSettings::getEngine() const {
CoreSettings::Engine CoreSettings::getEngine() const {
return engine; return engine;
} }
void MarkovChainSettings::setEngine(Engine newEngine) {
void CoreSettings::setEngine(Engine newEngine) {
this->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(); std::string minMaxEquationSolvingTechnique = this->getOption(minMaxEquationSolvingTechniqueOptionName).getArgumentByName("name").getValueAsString();
if (minMaxEquationSolvingTechnique == "valueIteration") { if (minMaxEquationSolvingTechnique == "valueIteration") {
return storm::solver::MinMaxTechnique::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 << "'."); 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(); return this->getOption(minMaxEquationSolvingTechniqueOptionName).getHasOptionBeenSet();
} }
void MarkovChainSettings::finalize() {
void CoreSettings::finalize() {
// Finalize engine. // Finalize engine.
std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString(); std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString();
if (engineStr == "sparse") { if (engineStr == "sparse") {
engine = MarkovChainSettings::Engine::Sparse;
engine = CoreSettings::Engine::Sparse;
} else if (engineStr == "hybrid") { } else if (engineStr == "hybrid") {
engine = MarkovChainSettings::Engine::Hybrid;
engine = CoreSettings::Engine::Hybrid;
} else if (engineStr == "dd") { } else if (engineStr == "dd") {
engine = MarkovChainSettings::Engine::Dd;
engine = CoreSettings::Engine::Dd;
} else if (engineStr == "expl") { } else if (engineStr == "expl") {
engine = MarkovChainSettings::Engine::Exploration;
engine = CoreSettings::Engine::Exploration;
} else if (engineStr == "abs") { } else if (engineStr == "abs") {
engine = MarkovChainSettings::Engine::AbstractionRefinement;
engine = CoreSettings::Engine::AbstractionRefinement;
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'."); STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'.");
} }
} }
bool MarkovChainSettings::check() const {
bool CoreSettings::check() const {
return true; return true;
} }

10
src/settings/modules/MarkovChainSettings.h → src/settings/modules/CoreSettings.h
View File

@ -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 "storm-config.h"
#include "src/settings/modules/ModuleSettings.h" #include "src/settings/modules/ModuleSettings.h"
@ -24,7 +24,7 @@ namespace storm {
/*! /*!
* This class represents the markov chain settings. * This class represents the markov chain settings.
*/ */
class MarkovChainSettings : public ModuleSettings {
class CoreSettings : public ModuleSettings {
public: public:
// An enumeration of all engines. // An enumeration of all engines.
enum class Engine { enum class Engine {
@ -34,7 +34,7 @@ namespace storm {
/*! /*!
* Creates a new set of markov chain settings. * Creates a new set of markov chain settings.
*/ */
MarkovChainSettings();
CoreSettings();
/*! /*!
* Retrieves whether the counterexample option was set. * Retrieves whether the counterexample option was set.
@ -173,4 +173,4 @@ namespace storm {
} // namespace settings } // namespace settings
} // namespace storm } // namespace storm
#endif /* STORM_SETTINGS_MODULES_MARKOVCHAINSETTINGS_H_ */
#endif /* STORM_SETTINGS_MODULES_CoreSettings_H_ */

4
src/settings/modules/EigenEquationSolverSettings.cpp
View File

@ -6,7 +6,7 @@
#include "src/settings/Argument.h" #include "src/settings/Argument.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
#include "src/solver/SolverSelectionOptions.h" #include "src/solver/SolverSelectionOptions.h"
namespace storm { namespace storm {
@ -98,7 +98,7 @@ namespace storm {
// This list does not include the precision, because this option is shared with other modules. // This list does not include the precision, because this option is shared with other modules.
bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isMaximalIterationCountSet(); 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; return true;
} }

4
src/settings/modules/ExplorationSettings.cpp
View File

@ -1,5 +1,5 @@
#include "src/settings/modules/ExplorationSettings.h" #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/Option.h"
#include "src/settings/OptionBuilder.h" #include "src/settings/OptionBuilder.h"
#include "src/settings/ArgumentBuilder.h" #include "src/settings/ArgumentBuilder.h"
@ -88,7 +88,7 @@ namespace storm {
this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() || this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
this->getOption(nextStateHeuristicOptionName).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; return true;
} }
} // namespace modules } // namespace modules

4
src/settings/modules/GlpkSettings.cpp
View File

@ -5,7 +5,7 @@
#include "src/settings/Argument.h" #include "src/settings/Argument.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
#include "src/solver/SolverSelectionOptions.h" #include "src/solver/SolverSelectionOptions.h"
namespace storm { namespace storm {
@ -35,7 +35,7 @@ namespace storm {
bool GlpkSettings::check() const { bool GlpkSettings::check() const {
if (isOutputSet() || isIntegerToleranceSet()) { 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; return true;

4
src/settings/modules/GmmxxEquationSolverSettings.cpp
View File

@ -6,7 +6,7 @@
#include "src/settings/Argument.h" #include "src/settings/Argument.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
#include "src/solver/SolverSelectionOptions.h" #include "src/solver/SolverSelectionOptions.h"
namespace storm { namespace storm {
@ -109,7 +109,7 @@ namespace storm {
// This list does not include the precision, because this option is shared with other modules. // This list does not include the precision, because this option is shared with other modules.
bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isConvergenceCriterionSet(); 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; return true;
} }

4
src/settings/modules/GurobiSettings.cpp
View File

@ -5,7 +5,7 @@
#include "src/settings/ArgumentBuilder.h" #include "src/settings/ArgumentBuilder.h"
#include "src/settings/Argument.h" #include "src/settings/Argument.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
#include "src/solver/SolverSelectionOptions.h" #include "src/solver/SolverSelectionOptions.h"
namespace storm { namespace storm {
namespace settings { namespace settings {
@ -46,7 +46,7 @@ namespace storm {
bool GurobiSettings::check() const { bool GurobiSettings::check() const {
if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) { 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; return true;

4
src/settings/modules/NativeEquationSolverSettings.cpp
View File

@ -1,7 +1,7 @@
#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/SettingsManager.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/Option.h"
#include "src/settings/OptionBuilder.h" #include "src/settings/OptionBuilder.h"
#include "src/settings/ArgumentBuilder.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. // This list does not include the precision, because this option is shared with other modules.
bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isConvergenceCriterionSet(); 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; return true;
} }

8
src/solver/LinearEquationSolver.cpp
View File

@ -8,7 +8,7 @@
#include "src/solver/EliminationLinearEquationSolver.h" #include "src/solver/EliminationLinearEquationSolver.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
namespace storm { namespace storm {
namespace solver { namespace solver {
@ -31,7 +31,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename MatrixType> template<typename MatrixType>
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> GeneralLinearEquationSolverFactory<ValueType>::selectSolver(MatrixType&& matrix) const { 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) { switch (equationSolver) {
case storm::solver::EquationSolverType::Gmmxx: return std::make_unique<storm::solver::GmmxxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix)); 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)); 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> template<typename MatrixType>
std::unique_ptr<storm::solver::LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::selectSolver(MatrixType&& matrix) const { 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) { switch (equationSolver) {
case storm::solver::EquationSolverType::Elimination: return std::make_unique<storm::solver::EliminationLinearEquationSolver<storm::RationalNumber>>(matrix); 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); default: return std::make_unique<storm::solver::EigenLinearEquationSolver<storm::RationalNumber>>(matrix);
@ -68,7 +68,7 @@ namespace storm {
template<typename MatrixType> template<typename MatrixType>
std::unique_ptr<storm::solver::LinearEquationSolver<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::selectSolver(MatrixType&& matrix) const { 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) { switch (equationSolver) {
case storm::solver::EquationSolverType::Elimination: return std::make_unique<storm::solver::EliminationLinearEquationSolver<storm::RationalFunction>>(matrix); 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); default: return std::make_unique<storm::solver::EigenLinearEquationSolver<storm::RationalFunction>>(matrix);

4
src/solver/MinMaxLinearEquationSolver.cpp
View File

@ -1,6 +1,6 @@
#include "MinMaxLinearEquationSolver.h" #include "MinMaxLinearEquationSolver.h"
#include "src/settings/SettingsManager.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/macros.h"
#include "src/exceptions/NotImplementedException.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) { 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) { 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 { } else {
useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration); useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration);
} }

4
src/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -9,7 +9,7 @@
#include "src/settings/SettingsManager.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/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.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) 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. // 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 #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."); STORM_LOG_INFO_COND(this->enableCuda, "Option CUDA was not set, but the topological value iteration solver will use it anyways.");
#endif #endif

4
src/storage/bisimulation/BisimulationDecomposition.cpp
View File

@ -13,7 +13,7 @@
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "src/settings/SettingsManager.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/FormulaInformation.h"
#include "src/logic/FragmentSpecification.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; 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 initialPartitionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(initialPartitionTime);
std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime); std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime);
std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime); std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime);

4
src/storm-dyftee.cpp
View File

@ -9,7 +9,7 @@
#include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/DFTSettings.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/DebugSettings.h"
//#include "src/settings/modules/CounterexampleGeneratorSettings.h" //#include "src/settings/modules/CounterexampleGeneratorSettings.h"
//#include "src/settings/modules/CuddSettings.h" //#include "src/settings/modules/CuddSettings.h"
@ -53,7 +53,7 @@ void initializeSettings() {
// Register all known settings modules. // Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>(); storm::settings::addModule<storm::settings::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::DFTSettings>(); 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::DebugSettings>();
//storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(); //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
//storm::settings::addModule<storm::settings::modules::CuddSettings>(); //storm::settings::addModule<storm::settings::modules::CuddSettings>();

8
src/utility/solver.cpp
View File

@ -21,7 +21,7 @@
#include "src/solver/Z3SmtSolver.h" #include "src/solver/Z3SmtSolver.h"
#include "src/solver/MathsatSmtSolver.h" #include "src/solver/MathsatSmtSolver.h"
#include "src/settings/SettingsManager.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/settings/modules/NativeEquationSolverSettings.h"
#include "src/exceptions/InvalidSettingsException.h" #include "src/exceptions/InvalidSettingsException.h"
@ -56,7 +56,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
MinMaxLinearEquationSolverFactory<ValueType>& MinMaxLinearEquationSolverFactory<ValueType>::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { MinMaxLinearEquationSolverFactory<ValueType>& MinMaxLinearEquationSolverFactory<ValueType>::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) {
if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) { 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 { } else {
this->solverType = storm::solver::convert(solverTypeSel); 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 { std::unique_ptr<storm::solver::LpSolver> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const {
storm::solver::LpSolverType t; storm::solver::LpSolverType t;
if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { 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 { } else {
t = convert(solvT); t = convert(solvT);
} }
@ -131,7 +131,7 @@ namespace storm {
} }
std::unique_ptr<storm::solver::SmtSolver> SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { 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) { switch (smtSolverType) {
case storm::solver::SmtSolverType::Z3: return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::Z3SmtSolver(manager)); 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)); case storm::solver::SmtSolverType::Mathsat: return std::unique_ptr<storm::solver::SmtSolver>(new storm::solver::MathsatSmtSolver(manager));

20
src/utility/storm.h
View File

@ -17,12 +17,12 @@
// Headers that provide auxiliary functionality. // Headers that provide auxiliary functionality.
#include "src/settings/SettingsManager.h" #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/IOSettings.h"
#include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/BisimulationSettings.h"
#include "src/settings/modules/ParametricSettings.h" #include "src/settings/modules/ParametricSettings.h"
#include "src/settings/modules/EliminationSettings.h" #include "src/settings/modules/EliminationSettings.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
// Formula headers. // Formula headers.
#include "src/logic/Formulas.h" #include "src/logic/Formulas.h"
@ -239,18 +239,18 @@ namespace storm {
template<typename ValueType, storm::dd::DdType DdType> 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) { 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>>(); 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"); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model");
return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant); 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>>(); 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"); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model");
return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant); 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>>(); 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"); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant); return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant);
@ -267,7 +267,7 @@ namespace storm {
storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
if (model->getType() == storm::models::ModelType::Dtmc) { if (model->getType() == storm::models::ModelType::Dtmc) {
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>(); 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); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
if (modelchecker.canHandle(task)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);
@ -285,7 +285,7 @@ namespace storm {
} else if (model->getType() == storm::models::ModelType::Mdp) { } 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>>(); std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
#ifdef STORM_HAVE_CUDA #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); storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
result = modelchecker.check(task); result = modelchecker.check(task);
} else { } else {
@ -324,7 +324,7 @@ namespace storm {
if (model->getType() == storm::models::ModelType::Dtmc) { 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>>(); 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); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> modelchecker(*dtmc);
if (modelchecker.canHandle(task)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);
@ -370,7 +370,7 @@ namespace storm {
if (model->getType() == storm::models::ModelType::Dtmc) { 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>>(); 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); storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
if (modelchecker.canHandle(task)) { if (modelchecker.canHandle(task)) {
result = modelchecker.check(task); result = modelchecker.check(task);

6
test/functional/parser/DeterministicSparseTransitionParserTest.cpp
View File

@ -11,7 +11,7 @@
#include "src/parser/DeterministicSparseTransitionParser.h" #include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/storage/SparseMatrix.h" #include "src/storage/SparseMatrix.h"
#include "src/settings/SettingsManager.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/settings/SettingMemento.h"
#include "src/exceptions/FileIoException.h" #include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
@ -191,7 +191,7 @@ TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) {
TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. // 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. // 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"); 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) { TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. // 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); ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException);
} }

6
test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
View File

@ -8,7 +8,7 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/modules/CoreSettings.h"
#include <vector> #include <vector>
@ -187,7 +187,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) { TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. // 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. // 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"); 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) { TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. // 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); ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser<>::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"), storm::exceptions::WrongFormatException);
} }

6
test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
View File

@ -13,7 +13,7 @@
#include "src/settings/SettingMemento.h" #include "src/settings/SettingMemento.h"
#include "src/settings/SettingsManager.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/FileIoException.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
@ -210,7 +210,7 @@ TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) {
TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed. // 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. // 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")); 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) { TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. // 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); ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException);
} }

Write Preview
Loading…
Cancel
Save