diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index 284ff0b6b..dce1baf5a 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -2,8 +2,12 @@ #include "src/utility/macros.h" #include "src/exceptions/ExpressionEvaluationException.h" +#include "src/exceptions/InvalidArgumentException.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace adapters { diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index eae18d06e..48ffa7344 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -12,10 +12,168 @@ #include "src/utility/prism.h" #include "src/utility/math.h" +#include "src/storage/prism/Program.h" + +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + +#include "src/settings/modules/GeneralSettings.h" namespace storm { namespace builder { + template + class DdPrismModelBuilder::GenerationInformation { + public: + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() { + // Initializes variables and identity DDs. + createMetaVariablesAndIdentities(); + + rowExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToRowMetaVariableMap)); + columnExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToColumnMetaVariableMap)); + } + + // The program that is currently translated. + storm::prism::Program const& program; + + // The manager used to build the decision diagrams. + std::shared_ptr> manager; + + // The meta variables for the row encoding. + std::set rowMetaVariables; + std::map variableToRowMetaVariableMap; + std::shared_ptr> rowExpressionAdapter; + + // The meta variables for the column encoding. + std::set columnMetaVariables; + std::map variableToColumnMetaVariableMap; + std::shared_ptr> columnExpressionAdapter; + + // All pairs of row/column meta variables. + std::vector> rowColumnMetaVariablePairs; + + // The meta variables used to encode the nondeterminism. + std::vector nondeterminismMetaVariables; + + // The meta variables used to encode the synchronization. + std::vector synchronizationMetaVariables; + + // A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization + // variables). This is handy to abstract from this variable set. + std::set allNondeterminismVariables; + + // DDs representing the identity for each variable. + std::map> variableToIdentityMap; + + // DDs representing the identity for each module. + std::map> moduleToIdentityMap; + + // DDs representing the valid ranges of the variables of each module. + std::map> moduleToRangeMap; + + private: + /*! + * Creates the required meta variables and variable/module identities. + */ + void createMetaVariablesAndIdentities() { + // Add synchronization variables. + for (auto const& actionIndex : program.getActionIndices()) { + std::pair variablePair = manager->addMetaVariable(program.getActionName(actionIndex)); + synchronizationMetaVariables.push_back(variablePair.first); + allNondeterminismVariables.insert(variablePair.first); + } + + // Add nondeterminism variables (number of modules + number of commands). + uint_fast64_t numberOfNondeterminismVariables = program.getModules().size(); + for (auto const& module : program.getModules()) { + numberOfNondeterminismVariables += module.getNumberOfCommands(); + } + for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { + std::pair variablePair = manager->addMetaVariable("nondet" + std::to_string(i)); + nondeterminismMetaVariables.push_back(variablePair.first); + allNondeterminismVariables.insert(variablePair.first); + } + + // Create meta variables for global program variables. + for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) { + int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); + int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); + std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd(); + variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); + rowColumnMetaVariablePairs.push_back(variablePair); + } + for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { + std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + + rowColumnMetaVariablePairs.push_back(variablePair); + } + + // Create meta variables for each of the modules' variables. + for (storm::prism::Module const& module : program.getModules()) { + storm::dd::Add moduleIdentity = manager->getAddOne(); + storm::dd::Add moduleRange = manager->getAddOne(); + + for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { + int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); + int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); + std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); + STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).toAdd(); + variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); + moduleIdentity *= variableIdentity; + moduleRange *= manager->getRange(variablePair.first).toAdd(); + + rowColumnMetaVariablePairs.push_back(variablePair); + } + for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { + std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); + STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).toAdd(); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + moduleIdentity *= variableIdentity; + moduleRange *= manager->getRange(variablePair.first).toAdd(); + + rowColumnMetaVariablePairs.push_back(variablePair); + } + moduleToIdentityMap[module.getName()] = moduleIdentity; + moduleToRangeMap[module.getName()] = moduleRange; + } + } + }; + + + template DdPrismModelBuilder::Options::Options() : buildRewards(false), rewardModelName(), constantDefinitions() { // Intentionally left empty. diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 4f6d8f580..c65265530 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -4,13 +4,30 @@ #include #include -#include "src/models/symbolic/Model.h" #include "src/logic/Formulas.h" -#include "src/storage/prism/Program.h" #include "src/adapters/AddExpressionAdapter.h" #include "src/utility/macros.h" namespace storm { + namespace prism { + class Program; + class Module; + class RewardModel; + class Update; + class Command; + } + + namespace dd { + template class Bdd; + } + + namespace models { + namespace symbolic { + template class Model; + } + } + + namespace builder { template @@ -129,155 +146,7 @@ namespace storm { /*! * Structure to store all information required to generate the model from the program. */ - class GenerationInformation { - public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() { - // Initializes variables and identity DDs. - createMetaVariablesAndIdentities(); - - rowExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToRowMetaVariableMap)); - columnExpressionAdapter = std::shared_ptr>(new storm::adapters::AddExpressionAdapter(manager, variableToColumnMetaVariableMap)); - } - - // The program that is currently translated. - storm::prism::Program const& program; - - // The manager used to build the decision diagrams. - std::shared_ptr> manager; - - // The meta variables for the row encoding. - std::set rowMetaVariables; - std::map variableToRowMetaVariableMap; - std::shared_ptr> rowExpressionAdapter; - - // The meta variables for the column encoding. - std::set columnMetaVariables; - std::map variableToColumnMetaVariableMap; - std::shared_ptr> columnExpressionAdapter; - - // All pairs of row/column meta variables. - std::vector> rowColumnMetaVariablePairs; - - // The meta variables used to encode the nondeterminism. - std::vector nondeterminismMetaVariables; - - // The meta variables used to encode the synchronization. - std::vector synchronizationMetaVariables; - - // A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization - // variables). This is handy to abstract from this variable set. - std::set allNondeterminismVariables; - - // DDs representing the identity for each variable. - std::map> variableToIdentityMap; - - // DDs representing the identity for each module. - std::map> moduleToIdentityMap; - - // DDs representing the valid ranges of the variables of each module. - std::map> moduleToRangeMap; - - private: - /*! - * Creates the required meta variables and variable/module identities. - */ - void createMetaVariablesAndIdentities() { - // Add synchronization variables. - for (auto const& actionIndex : program.getActionIndices()) { - std::pair variablePair = manager->addMetaVariable(program.getActionName(actionIndex)); - synchronizationMetaVariables.push_back(variablePair.first); - allNondeterminismVariables.insert(variablePair.first); - } - - // Add nondeterminism variables (number of modules + number of commands). - uint_fast64_t numberOfNondeterminismVariables = program.getModules().size(); - for (auto const& module : program.getModules()) { - numberOfNondeterminismVariables += module.getNumberOfCommands(); - } - for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { - std::pair variablePair = manager->addMetaVariable("nondet" + std::to_string(i)); - nondeterminismMetaVariables.push_back(variablePair.first); - allNondeterminismVariables.insert(variablePair.first); - } - - // Create meta variables for global program variables. - for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) { - int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); - std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd(); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); - rowColumnMetaVariablePairs.push_back(variablePair); - } - for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { - std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); - - rowColumnMetaVariablePairs.push_back(variablePair); - } - - // Create meta variables for each of the modules' variables. - for (storm::prism::Module const& module : program.getModules()) { - storm::dd::Add moduleIdentity = manager->getAddOne(); - storm::dd::Add moduleRange = manager->getAddOne(); - - for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { - int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); - int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); - std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); - STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).toAdd(); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); - moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first).toAdd(); - - rowColumnMetaVariablePairs.push_back(variablePair); - } - for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { - std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - - storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).toAdd(); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); - moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first).toAdd(); - - rowColumnMetaVariablePairs.push_back(variablePair); - } - moduleToIdentityMap[module.getName()] = moduleIdentity; - moduleToRangeMap[module.getName()] = moduleRange; - } - } - }; - + class GenerationInformation; private: static storm::dd::Add encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value); diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 8b3dbffa0..ab034238c 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -6,6 +6,10 @@ #include "src/models/sparse/Ctmc.h" #include "src/models/sparse/Mdp.h" + + +#include "src/settings/modules/GeneralSettings.h" + #include "src/utility/prism.h" #include "src/utility/macros.h" #include "src/exceptions/WrongFormatException.h" diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index f7891ef5e..1339d646a 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -18,6 +18,10 @@ #include "src/utility/counterexamples.h" #include "src/utility/solver.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/CounterexampleGeneratorSettings.h" + namespace storm { namespace counterexamples { diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index a096810ed..658b5a114 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -11,6 +11,8 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/solver/GmmxxMinMaxLinearEquationSolver.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/utility/counterexamples.h" #include "src/utility/prism.h" diff --git a/src/logic/ComparisonType.cpp b/src/logic/ComparisonType.cpp index 1eacaf1c2..bea35d8bb 100644 --- a/src/logic/ComparisonType.cpp +++ b/src/logic/ComparisonType.cpp @@ -4,10 +4,10 @@ namespace storm { namespace logic { std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType) { switch (comparisonType) { - case Less: out << "<"; break; - case LessEqual: out << "<="; break; - case Greater: out << ">"; break; - case GreaterEqual: out << ">="; break; + case ComparisonType::Less: out << "<"; break; + case ComparisonType::LessEqual: out << "<="; break; + case ComparisonType::Greater: out << ">"; break; + case ComparisonType::GreaterEqual: out << ">="; break; } return out; } diff --git a/src/logic/ComparisonType.h b/src/logic/ComparisonType.h index c339ea7fd..61dbe53bb 100644 --- a/src/logic/ComparisonType.h +++ b/src/logic/ComparisonType.h @@ -5,7 +5,7 @@ namespace storm { namespace logic { - enum ComparisonType { Less, LessEqual, Greater, GreaterEqual }; + enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual }; std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 42aafcada..746ab71a7 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -5,7 +5,6 @@ #include #include -#include "src/modelchecker/results/CheckResult.h" namespace storm { namespace logic { diff --git a/src/logic/ReachabilityRewardFormula.h b/src/logic/ReachabilityRewardFormula.h index 357d2f680..064b9acb2 100644 --- a/src/logic/ReachabilityRewardFormula.h +++ b/src/logic/ReachabilityRewardFormula.h @@ -4,7 +4,7 @@ #include #include "src/logic/RewardPathFormula.h" -#include "src/logic/StateFormula.h" + namespace storm { namespace logic { diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 2b6d2ef3a..e6611979d 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -6,6 +6,8 @@ #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidOperationException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InternalTypeErrorException.h" namespace storm { namespace modelchecker { diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 92434d18d..42b84fef7 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -5,8 +5,11 @@ #include "src/logic/Formulas.h" + namespace storm { namespace modelchecker { + class CheckResult; + class AbstractModelChecker { public: virtual ~AbstractModelChecker() { diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 498a2fc02..d97466ecd 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -3,10 +3,14 @@ #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "src/storage/dd/CuddOdd.h" +#include "src/storage/dd/CuddDdManager.h" #include "src/utility/macros.h" #include "src/utility/graph.h" + +#include "src/settings/modules/GeneralSettings.h" + #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" @@ -15,6 +19,8 @@ #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" + + namespace storm { namespace modelchecker { template diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 9b6818884..d1eaea8e7 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -8,6 +8,10 @@ #include "src/utility/solver.h" #include "src/utility/numerical.h" + +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/SettingsManager.h" + #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index e3149901f..64c6810f4 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -10,6 +10,9 @@ #include "src/utility/vector.h" #include "src/utility/graph.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 3b61ded53..7268d9bfa 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -2,10 +2,14 @@ #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/storage/dd/CuddOdd.h" +#include "src/storage/dd/CuddDdManager.h" #include "src/utility/macros.h" #include "src/utility/graph.h" + +#include "src/settings/modules/GeneralSettings.h" + #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index f54bed203..3f83672b2 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/prctl/HybridMdpPrctlModelChecker.h" #include "src/storage/dd/CuddOdd.h" +#include "src/storage/dd/CuddDdManager.h" #include "src/utility/macros.h" #include "src/utility/graph.h" @@ -9,6 +10,9 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" + +#include "src/settings/modules/GeneralSettings.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index d49075faa..08dcf98dc 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -12,6 +12,9 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/settings/modules/GeneralSettings.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index adf65d728..c6ffb103d 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -13,6 +13,9 @@ #include "src/solver/LpSolver.h" + +#include "src/settings/modules/GeneralSettings.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/storage/expressions/Expressions.h" diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 022eca0af..30720b091 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "src/storage/dd/CuddOdd.h" +#include "src/storage/dd/CuddDdManager.h" #include "src/utility/macros.h" #include "src/utility/graph.h" @@ -9,6 +10,9 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" + +#include "src/settings/modules/GeneralSettings.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 1ddd761d6..e594c2f70 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -1,5 +1,8 @@ #include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddDdManager.h" + #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 0ae832563..19de40fa2 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -5,6 +5,10 @@ #include "src/adapters/CarlAdapter.h" +#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/SettingsManager.h" + #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -17,6 +21,8 @@ #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/IllegalArgumentException.h" + namespace storm { namespace modelchecker { diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index f54984ac3..16339f38b 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -7,6 +7,7 @@ #include "src/exceptions/InvalidOperationException.h" #include "src/adapters/CarlAdapter.h" + namespace storm { namespace modelchecker { template @@ -114,28 +115,28 @@ namespace storm { vector_type const& valuesAsVector = boost::get(values); storm::storage::BitVector result(valuesAsVector.size()); switch (comparisonType) { - case logic::Less: + case logic::ComparisonType::Less: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { if (valuesAsVector[index] < bound) { result.set(index); } } break; - case logic::LessEqual: + case logic::ComparisonType::LessEqual: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { if (valuesAsVector[index] <= bound) { result.set(index); } } break; - case logic::Greater: + case logic::ComparisonType::Greater: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { if (valuesAsVector[index] > bound) { result.set(index); } } break; - case logic::GreaterEqual: + case logic::ComparisonType::GreaterEqual: for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) { if (valuesAsVector[index] >= bound) { result.set(index); @@ -148,22 +149,22 @@ namespace storm { map_type const& valuesAsMap = boost::get(values); std::map result; switch (comparisonType) { - case logic::Less: + case logic::ComparisonType::Less: for (auto const& element : valuesAsMap) { result[element.first] = element.second < bound; } break; - case logic::LessEqual: + case logic::ComparisonType::LessEqual: for (auto const& element : valuesAsMap) { result[element.first] = element.second <= bound; } break; - case logic::Greater: + case logic::ComparisonType::Greater: for (auto const& element : valuesAsMap) { result[element.first] = element.second > bound; } break; - case logic::GreaterEqual: + case logic::ComparisonType::GreaterEqual: for (auto const& element : valuesAsMap) { result[element.first] = element.second >= bound; } diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index abf56e163..6cf6bd8e2 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -4,6 +4,8 @@ #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidOperationException.h" +#include "src/utility/macros.h" +#include "src/utility/constants.h" namespace storm { namespace modelchecker { diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index f2cdf8553..0dbf1c5fc 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/storage/dd/CuddDd.h" +#include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" namespace storm { diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index c9630a4c3..f05cd4f62 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -4,6 +4,8 @@ #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/exceptions/InvalidOperationException.h" +#include "src/utility/macros.h" +#include "src/utility/constants.h" namespace storm { namespace modelchecker { diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 5217396ce..051cf0373 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -1,6 +1,7 @@ #include "src/models/sparse/Ctmc.h" #include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" namespace storm { namespace models { diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp index 01f4cb4d7..f4917d7c8 100644 --- a/src/models/symbolic/Ctmc.cpp +++ b/src/models/symbolic/Ctmc.cpp @@ -1,5 +1,10 @@ #include "src/models/symbolic/Ctmc.h" + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp index 57cf7af60..8fb222c3c 100644 --- a/src/models/symbolic/DeterministicModel.cpp +++ b/src/models/symbolic/DeterministicModel.cpp @@ -1,5 +1,9 @@ #include "src/models/symbolic/DeterministicModel.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp index c11b94850..b7012e71b 100644 --- a/src/models/symbolic/Dtmc.cpp +++ b/src/models/symbolic/Dtmc.cpp @@ -1,5 +1,10 @@ #include "src/models/symbolic/Dtmc.h" + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp index 6084e2965..677ffa5ec 100644 --- a/src/models/symbolic/Mdp.cpp +++ b/src/models/symbolic/Mdp.cpp @@ -1,5 +1,11 @@ #include "src/models/symbolic/Mdp.h" + + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 8b72f3687..c974739e9 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -1,5 +1,13 @@ #include "src/models/symbolic/Model.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include "src/adapters/AddExpressionAdapter.h" + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 23d2030f3..62d8dc24c 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -7,13 +7,24 @@ #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Variable.h" -#include "src/adapters/AddExpressionAdapter.h" -#include "src/storage/dd/CuddDd.h" -#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/DdType.h" #include "src/models/ModelBase.h" #include "src/utility/OsDetection.h" namespace storm { + namespace dd { + + template class Dd; + template class Add; + template class Bdd; + template class DdManager; + + } + + namespace adapters { + template class AddExpressionAdapter; + } + namespace models { namespace symbolic { diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index 64b4cf6bc..2d97c767e 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -1,5 +1,10 @@ #include "src/models/symbolic/NondeterministicModel.h" + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp index 0424f100c..99141e611 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp @@ -1,5 +1,10 @@ #include "src/models/symbolic/StochasticTwoPlayerGame.h" + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + namespace storm { namespace models { namespace symbolic { diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 1f248430a..e7aa4f348 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -20,6 +20,7 @@ #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index a943cfaae..97faa4152 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -1,10 +1,12 @@ #include "MarkovAutomatonSparseTransitionParser.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" #include "src/parser/MappedFile.h" #include "src/utility/cstring.h" +#include "src/utility/macros.h" namespace storm { diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index c31552561..af8754e89 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -11,6 +11,7 @@ #include "src/parser/MappedFile.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/WrongFormatException.h" diff --git a/src/settings/Argument.h b/src/settings/Argument.h index 7aad2c048..e50b25dfc 100644 --- a/src/settings/Argument.h +++ b/src/settings/Argument.h @@ -12,13 +12,10 @@ #include #include "src/settings/ArgumentBase.h" + #include "src/settings/ArgumentType.h" -#include "src/settings/ArgumentTypeInferationHelper.h" -#include "src/utility/macros.h" #include "src/exceptions/ArgumentUnificationException.h" -#include "src/exceptions/IllegalArgumentException.h" -#include "src/exceptions/IllegalArgumentValueException.h" -#include "src/exceptions/IllegalFunctionCallException.h" + namespace storm { namespace settings { @@ -28,11 +25,11 @@ namespace storm { * is necessary so that it becomes easy to store a vector of arguments later despite variing template types, by * keeping a vector of pointers to the base class. */ - template - class Argument : public ArgumentBase { + template + class Argument : public ArgumentBase { public: // Introduce shortcuts for validation functions. - typedef std::function userValidationFunction_t; + typedef std::function userValidationFunction_t; /*! * Creates a new argument with the given parameters. @@ -43,9 +40,7 @@ namespace storm { * to this argument. * @param isOptional A flag indicating whether the argument is optional. */ - Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) { - // Intentionally left empty. - } + Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions); /*! * Creates a new argument with the given parameters. @@ -56,35 +51,15 @@ namespace storm { * to this argument. * @param isOptional A flag indicating whether the argument is optional. */ - Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(), hasDefaultValue(true) { - this->setDefaultValue(defaultValue); - } + Argument(std::string const& name, std::string const& description, std::vector const& validationFunctions, bool isOptional, T defaultValue); - virtual bool getIsOptional() const override { - return this->isOptional; - } + virtual bool getIsOptional() const override; + + bool setFromStringValue(std::string const& fromStringValue) override; - bool setFromStringValue(std::string const& fromStringValue) override { - bool conversionOk = false; - T newValue = ArgumentBase::convertFromString(fromStringValue, conversionOk); - if (!conversionOk) { - return false; - } - return this->setFromTypeValue(newValue); - } - - bool setFromTypeValue(T const& newValue, bool hasBeenSet = true) { - if (!this->validate(newValue)) { - return false; - } - this->argumentValue = newValue; - this->hasBeenSet = hasBeenSet; - return true; - } - - virtual ArgumentType getType() const override { - return this->argumentType; - } + bool setFromTypeValue(T const& newValue, bool hasBeenSet = true); + + virtual ArgumentType getType() const override; /*! * Checks whether the given argument is compatible with the current one. If not, an exception is thrown. @@ -92,88 +67,36 @@ namespace storm { * @param other The other argument with which to check compatibility. * @return True iff the given argument is compatible with the current one. */ - template - bool isCompatibleWith(Argument const& other) const { + template + bool isCompatibleWith(Argument const& other) const { STORM_LOG_THROW(this->getType() == other.getType(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because they have different types."); STORM_LOG_THROW(this->getIsOptional() == other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments '" << this->getName() << "' and '" << other.getName() << "', because one of them is optional and the other one is not."); STORM_LOG_THROW(this->getHasDefaultValue() == other.getHasDefaultValue(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them has a default value and the other one does not."); return true; - } + } /*! * Retrieves the value of the argument if any has been set. Otherwise, an exception is thrown. * * @return The value of the argument. */ - T const& getArgumentValue() const { - STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument '" << this->getName() << "', because it was neither set nor specifies a default value."); - if (this->getHasBeenSet()) { - return this->argumentValue; - } else { - return this->defaultValue; - } - } - - virtual bool getHasDefaultValue() const override { - return this->hasDefaultValue; - } - - void setFromDefaultValue() override { - STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none."); - bool result = this->setFromTypeValue(this->defaultValue, false); - STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected."); - } - - virtual std::string getValueAsString() const override { - switch (this->argumentType) { - case ArgumentType::String: - return inferToString(ArgumentType::String, this->getArgumentValue()); - case ArgumentType::Boolean: { - bool iValue = inferToBoolean(ArgumentType::Boolean, this->getArgumentValue()); - if (iValue) { - return "true"; - } else { - return "false"; - } - } - default: return ArgumentBase::convertToString(this->argumentValue); - } - } - - virtual int_fast64_t getValueAsInteger() const override { - switch (this->argumentType) { - case ArgumentType::Integer: - return inferToInteger(ArgumentType::Integer, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break; - } - } + T const& getArgumentValue() const; + + virtual bool getHasDefaultValue() const override; + void setFromDefaultValue() override; - virtual uint_fast64_t getValueAsUnsignedInteger() const override { - switch (this->argumentType) { - case ArgumentType::UnsignedInteger: - return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break; - } - } + virtual std::string getValueAsString() const override; + + virtual int_fast64_t getValueAsInteger() const override; + virtual uint_fast64_t getValueAsUnsignedInteger() const override; - virtual double getValueAsDouble() const override { - switch (this->argumentType) { - case ArgumentType::Double: - return inferToDouble(ArgumentType::Double, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break; - } - } + virtual double getValueAsDouble() const override; - virtual bool getValueAsBoolean() const override { - switch (this->argumentType) { - case ArgumentType::Boolean: - return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break; - } - } + + virtual bool getValueAsBoolean() const override; private: // The value of the argument (in case it has been set). @@ -199,11 +122,7 @@ namespace storm { * * @param newDefault The new default value of the argument. */ - void setDefaultValue(T const& newDefault) { - STORM_LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions."); - this->defaultValue = newDefault; - this->hasDefaultValue = true; - } + void setDefaultValue(T const& newDefault); /*! * Applies all validation functions to the given value and therefore checks the validity of a value for this @@ -212,13 +131,7 @@ namespace storm { * @param value The value that is to be validated. * @return True iff the value passed all validation functions successfully. */ - bool validate(T const& value) const { - bool result = true; - for (auto const& lambda : validationFunctions) { - result = result && lambda(value); - } - return result; - } + bool validate(T const& value) const; }; } diff --git a/src/settings/ArgumentBase.cpp b/src/settings/ArgumentBase.cpp index 5ccfdbe2f..f307e1f93 100644 --- a/src/settings/ArgumentBase.cpp +++ b/src/settings/ArgumentBase.cpp @@ -1,5 +1,6 @@ #include "src/settings/ArgumentBase.h" +#include #include namespace storm { diff --git a/src/settings/ArgumentBase.h b/src/settings/ArgumentBase.h index 3531ccd20..836dd9674 100644 --- a/src/settings/ArgumentBase.h +++ b/src/settings/ArgumentBase.h @@ -3,7 +3,6 @@ #include #include -#include #include "src/settings/ArgumentType.h" diff --git a/src/settings/ArgumentBuilder.h b/src/settings/ArgumentBuilder.h index 18f03334d..7c3b7e8f0 100644 --- a/src/settings/ArgumentBuilder.h +++ b/src/settings/ArgumentBuilder.h @@ -26,7 +26,7 @@ namespace storm { /*! * This class serves as an API for creating arguments. */ - class ArgumentBuilder { + class ArgumentBuilder { public: /*! * Creates a string argument with the given parameters. @@ -35,10 +35,10 @@ namespace storm { * @param description The description of the argument. * @return The builder of the argument. */ - static ArgumentBuilder createStringArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::String, name, description); - return ab; - } + static ArgumentBuilder createStringArgument(std::string const& name, std::string const& description) { + ArgumentBuilder ab(ArgumentType::String, name, description); + return ab; + } /*! * Creates an integer argument with the given parameters. @@ -47,10 +47,10 @@ namespace storm { * @param description The description of the argument. * @return The builder of the argument. */ - static ArgumentBuilder createIntegerArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::Integer, name, description); - return ab; - } + static ArgumentBuilder createIntegerArgument(std::string const& name, std::string const& description) { + ArgumentBuilder ab(ArgumentType::Integer, name, description); + return ab; + } /*! * Creates an unsigned integer argument with the given parameters. @@ -59,10 +59,10 @@ namespace storm { * @param description The description of the argument. * @return The builder of the argument. */ - static ArgumentBuilder createUnsignedIntegerArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::UnsignedInteger, name, description); - return ab; - } + static ArgumentBuilder createUnsignedIntegerArgument(std::string const& name, std::string const& description) { + ArgumentBuilder ab(ArgumentType::UnsignedInteger, name, description); + return ab; + } /*! * Creates a double argument with the given parameters. @@ -71,10 +71,10 @@ namespace storm { * @param description The description of the argument. * @return The builder of the argument. */ - static ArgumentBuilder createDoubleArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::Double, name, description); - return ab; - } + static ArgumentBuilder createDoubleArgument(std::string const& name, std::string const& description) { + ArgumentBuilder ab(ArgumentType::Double, name, description); + return ab; + } /*! * Creates a boolean argument with the given parameters. @@ -83,10 +83,10 @@ namespace storm { * @param description The description of the argument. * @return The builder of the argument. */ - static ArgumentBuilder createBooleanArgument(std::string const& name, std::string const& description) { - ArgumentBuilder ab(ArgumentType::Boolean, name, description); - return ab; - } + static ArgumentBuilder createBooleanArgument(std::string const& name, std::string const& description) { + ArgumentBuilder ab(ArgumentType::Boolean, name, description); + return ab; + } /*! * Sets whether the argument is to be optional. @@ -94,11 +94,11 @@ namespace storm { * @param isOptional A flag that indicates whether the argument is to be optional. * @return A reference to the argument builder. */ - ArgumentBuilder& setIsOptional(bool isOptional) { - this->isOptional = isOptional; + ArgumentBuilder& setIsOptional(bool isOptional) { + this->isOptional = isOptional; STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to make argument '" << this->name << "' optional without default value."); - return *this; - } + return *this; + } #define PPCAT_NX(A, B) A ## B #define PPCAT(A, B) PPCAT_NX(A, B) @@ -109,12 +109,12 @@ return *this; \ } // Add the methods to add validation functions. - MACROaddValidationFunction(String, std::string) - MACROaddValidationFunction(Integer, int_fast64_t) - MACROaddValidationFunction(UnsignedInteger, uint_fast64_t) - MACROaddValidationFunction(Double, double) - MACROaddValidationFunction(Boolean, bool) - + MACROaddValidationFunction(String, std::string) + MACROaddValidationFunction(Integer, int_fast64_t) + MACROaddValidationFunction(UnsignedInteger, uint_fast64_t) + MACROaddValidationFunction(Double, double) + MACROaddValidationFunction(Boolean, bool) + #define MACROsetDefaultValue(funcName, funcType) ArgumentBuilder& PPCAT(setDefaultValue, funcName) (funcType const& defaultValue) { \ STORM_LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type."); \ @@ -124,11 +124,11 @@ return *this; \ } // Add the methods to set a default value. - MACROsetDefaultValue(String, std::string) - MACROsetDefaultValue(Integer, int_fast64_t) - MACROsetDefaultValue(UnsignedInteger, uint_fast64_t) - MACROsetDefaultValue(Double, double) - MACROsetDefaultValue(Boolean, bool) + MACROsetDefaultValue(String, std::string) + MACROsetDefaultValue(Integer, int_fast64_t) + MACROsetDefaultValue(UnsignedInteger, uint_fast64_t) + MACROsetDefaultValue(Double, double) + MACROsetDefaultValue(Boolean, bool) /*! * Builds an argument based on the information that was added to the builder object. @@ -137,45 +137,45 @@ return *this; \ */ std::shared_ptr build() { STORM_LOG_THROW(!this->hasBeenBuilt, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild argument with builder that was already used to build an argument."); - this->hasBeenBuilt = true; - switch (this->type) { - case ArgumentType::String: { - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_String, this->isOptional, this->defaultValue_String)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_String)); - } - break; + this->hasBeenBuilt = true; + switch (this->type) { + case ArgumentType::String: { + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_String, this->isOptional, this->defaultValue_String)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_String)); + } + break; + } + case ArgumentType::Integer: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Integer)); + } + break; + case ArgumentType::UnsignedInteger: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_UnsignedInteger)); } - case ArgumentType::Integer: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Integer)); - } - break; - case ArgumentType::UnsignedInteger: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_UnsignedInteger)); - } - break; - case ArgumentType::Double: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Double, this->isOptional, this->defaultValue_Double)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Double)); - } - break; - case ArgumentType::Boolean: - if (this->hasDefaultValue) { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean)); - } else { - return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Boolean)); - } - break; - } + break; + case ArgumentType::Double: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Double, this->isOptional, this->defaultValue_Double)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Double)); + } + break; + case ArgumentType::Boolean: + if (this->hasDefaultValue) { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean)); + } else { + return std::shared_ptr(new Argument(this->name, this->description, this->userValidationFunctions_Boolean)); + } + break; + } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException, "Argument has illegal type."); } @@ -187,43 +187,43 @@ return *this; \ * @param name The name of the argument. * @param description The description of the argument. */ - ArgumentBuilder(ArgumentType type, std::string const& name, std::string const& description) : hasBeenBuilt(false), type(type), name(name), description(description), isOptional(false), hasDefaultValue(false), defaultValue_String(), defaultValue_Integer(), defaultValue_UnsignedInteger(), defaultValue_Double(), defaultValue_Boolean(), userValidationFunctions_String(), userValidationFunctions_Integer(), userValidationFunctions_UnsignedInteger(), userValidationFunctions_Double(), userValidationFunctions_Boolean() { - // Intentionally left empty. - } + ArgumentBuilder(ArgumentType type, std::string const& name, std::string const& description) : hasBeenBuilt(false), type(type), name(name), description(description), isOptional(false), hasDefaultValue(false), defaultValue_String(), defaultValue_Integer(), defaultValue_UnsignedInteger(), defaultValue_Double(), defaultValue_Boolean(), userValidationFunctions_String(), userValidationFunctions_Integer(), userValidationFunctions_UnsignedInteger(), userValidationFunctions_Double(), userValidationFunctions_Boolean() { + // Intentionally left empty. + } // A flag that stores whether an argument has been built using this builder. - bool hasBeenBuilt; + bool hasBeenBuilt; // The type of the argument. - ArgumentType type; + ArgumentType type; // The name of te argument. - std::string name; + std::string name; // The description of the argument. - std::string description; + std::string description; // A flag indicating whether the argument is optional. - bool isOptional; + bool isOptional; // A flag that stores whether the argument has a default value. - bool hasDefaultValue; + bool hasDefaultValue; // The default value of the argument separated by its type. - std::string defaultValue_String; - int_fast64_t defaultValue_Integer; - uint_fast64_t defaultValue_UnsignedInteger; - double defaultValue_Double; - bool defaultValue_Boolean; + std::string defaultValue_String; + int_fast64_t defaultValue_Integer; + uint_fast64_t defaultValue_UnsignedInteger; + double defaultValue_Double; + bool defaultValue_Boolean; // The validation functions separated by their type. - std::vector::userValidationFunction_t> userValidationFunctions_String; - std::vector::userValidationFunction_t> userValidationFunctions_Integer; - std::vector::userValidationFunction_t> userValidationFunctions_UnsignedInteger; - std::vector::userValidationFunction_t> userValidationFunctions_Double; - std::vector::userValidationFunction_t> userValidationFunctions_Boolean; - }; - } + std::vector::userValidationFunction_t> userValidationFunctions_String; + std::vector::userValidationFunction_t> userValidationFunctions_Integer; + std::vector::userValidationFunction_t> userValidationFunctions_UnsignedInteger; + std::vector::userValidationFunction_t> userValidationFunctions_Double; + std::vector::userValidationFunction_t> userValidationFunctions_Boolean; + }; + } } #endif // STORM_SETTINGS_ARGUMENTBUILDER_H_ \ No newline at end of file diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h index d5ac0dac2..235ddd765 100644 --- a/src/settings/ArgumentValidators.h +++ b/src/settings/ArgumentValidators.h @@ -14,6 +14,10 @@ #include "src/settings/Argument.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/IllegalArgumentValueException.h" +#include "src/exceptions/IllegalFunctionCallException.h" + namespace storm { namespace settings { diff --git a/src/settings/Option.cpp b/src/settings/Option.cpp index 02a3ca1c9..b5cba7759 100644 --- a/src/settings/Option.cpp +++ b/src/settings/Option.cpp @@ -1,26 +1,153 @@ #include "src/settings/Option.h" #include +#include +#include "ArgumentBase.h" +#include "Argument.h" + +#include "src/utility/macros.h" +#include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/OptionUnificationException.h" + namespace storm { namespace settings { - uint_fast64_t Option::getPrintLength() const { - uint_fast64_t length = 2; - if (!this->getRequiresModulePrefix()) { - length += 2; + + Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments) : Option(moduleName, longOptionName, "", false, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) { + // Intentionally left empty. + } + + Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments) : Option(moduleName, longOptionName, shortOptionName, true, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) { + // Intentionally left empty. + } + + + bool Option::isCompatibleWith(Option const& other) { + STORM_LOG_THROW(this->getArgumentCount() == other.getArgumentCount(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their argument count differs."); + + for(size_t i = 0; i != this->arguments.size(); i++) { + ArgumentBase const& firstArgument = this->getArgument(i); + ArgumentBase const& secondArgument = other.getArgument(i); + + STORM_LOG_THROW(firstArgument.getType() == secondArgument.getType(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their arguments are incompatible."); + + switch (firstArgument.getType()) { + case ArgumentType::String: + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); + break; + case ArgumentType::Integer: + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); + break; + case ArgumentType::UnsignedInteger: + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); + break; + case ArgumentType::Double: + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); + break; + case ArgumentType::Boolean: + static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); + break; + } + } + return true; + } + + + uint_fast64_t Option::getArgumentCount() const { + return this->arguments.size(); + } + + + ArgumentBase const& Option::getArgument(uint_fast64_t argumentIndex) const { + STORM_LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds."); + return *this->arguments.at(argumentIndex); + } + + ArgumentBase& Option::getArgument(uint_fast64_t argumentIndex) { + STORM_LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds."); + return *this->arguments.at(argumentIndex); + } + + + ArgumentBase const& Option::getArgumentByName(std::string const& argumentName) const { + auto argumentIterator = this->argumentNameMap.find(argumentName); + STORM_LOG_THROW(argumentIterator != this->argumentNameMap.end(), storm::exceptions::IllegalArgumentException, "Unable to retrieve argument with unknown name '" << argumentName << "'."); + return *argumentIterator->second; + } + + std::string const& Option::getLongName() const { + return this->longName; + } + + + bool Option::getHasShortName() const { + return this->hasShortName; + } + + + std::string const& Option::getShortName() const { + return this->shortName; + } + + std::string const& Option::getDescription() const { + return this->description; + } + + std::string const& Option::getModuleName() const { + return this->moduleName; + } + + bool Option::getIsRequired() const { + return this->isRequired; + } + + + bool Option::getRequiresModulePrefix() const { + return this->requireModulePrefix; + } + + bool Option::getHasOptionBeenSet() const { + return this->hasBeenSet; + } + + Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(optionArguments), argumentNameMap() { + // First, do some sanity checks. + STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name."); + STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name."); + + bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != longName.end(); + STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal long name '" << longName << "'."); + + bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != shortName.end(); + STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal short name '" << shortName << "'."); + + // Then index all arguments. + for (auto const& argument : arguments) { + argumentNameMap.emplace(argument->getName(), argument); + } + } + + void Option::setHasOptionBeenSet(bool newValue) { + this->hasBeenSet = newValue; } - length += this->getModuleName().length() + 1; - length += this->getLongName().length(); - if (this->getHasShortName()) { - length += 4; + + uint_fast64_t Option::getPrintLength() const { + uint_fast64_t length = 2; if (!this->getRequiresModulePrefix()) { length += 2; } length += this->getModuleName().length() + 1; - length += this->getShortName().length(); + length += this->getLongName().length(); + if (this->getHasShortName()) { + length += 4; + if (!this->getRequiresModulePrefix()) { + length += 2; + } + length += this->getModuleName().length() + 1; + length += this->getShortName().length(); + } + return length; } - return length; - } std::vector> const& Option::getArguments() const { return this->arguments; diff --git a/src/settings/Option.h b/src/settings/Option.h index 84fe10bca..bcd0f2f3d 100644 --- a/src/settings/Option.h +++ b/src/settings/Option.h @@ -4,19 +4,13 @@ #include #include #include -#include #include #include -#include -#include -#include "ArgumentType.h" +#include + #include "ArgumentBase.h" -#include "Argument.h" -#include "src/utility/macros.h" -#include "src/exceptions/IllegalArgumentException.h" -#include "src/exceptions/OptionUnificationException.h" namespace storm { namespace settings { @@ -26,14 +20,15 @@ namespace storm { namespace modules { class ModuleSettings; } + class ArgumentBase; /*! * This class represents one command-line option. */ - class Option { + class Option { public: // Declare settings manager and module settings classes as friends. - friend class SettingsManager; + friend class SettingsManager; friend class modules::ModuleSettings; /*! @@ -47,9 +42,7 @@ namespace storm { * module name. * @param optionArguments The arguments of the option. */ - Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()) : Option(moduleName, longOptionName, "", false, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) { - // Intentionally left empty. - } + Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()); /*! * Creates an option with the given parameters. @@ -63,9 +56,7 @@ namespace storm { * module name. * @param optionArguments The arguments of the option. */ - Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()) : Option(moduleName, longOptionName, shortOptionName, true, optionDescription, isOptionRequired, requireModulePrefix, optionArguments) { - // Intentionally left empty. - } + Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()); /*! * Checks whether the given option is compatible with the current one. If not, an exception is thrown. @@ -73,44 +64,14 @@ namespace storm { * @param other The other option with which to check compatibility. * @return True iff the given argument is compatible with the current one. */ - bool isCompatibleWith(Option const& other) { - STORM_LOG_THROW(this->getArgumentCount() == other.getArgumentCount(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their argument count differs."); - - for(size_t i = 0; i != this->arguments.size(); i++) { - ArgumentBase const& firstArgument = this->getArgument(i); - ArgumentBase const& secondArgument = other.getArgument(i); - - STORM_LOG_THROW(firstArgument.getType() == secondArgument.getType(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their arguments are incompatible."); - - switch (firstArgument.getType()) { - case ArgumentType::String: - static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); - break; - case ArgumentType::Integer: - static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); - break; - case ArgumentType::UnsignedInteger: - static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); - break; - case ArgumentType::Double: - static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); - break; - case ArgumentType::Boolean: - static_cast const&>(firstArgument).isCompatibleWith(static_cast const&>(secondArgument)); - break; - } - } - return true; - } + bool isCompatibleWith(Option const& other); /*! * Retrieves the argument count this option expects. * * @return The argument count of this option. */ - uint_fast64_t getArgumentCount() const { - return this->arguments.size(); - } + uint_fast64_t getArgumentCount() const; /*! * Retrieves the i-th argument of this option. @@ -118,10 +79,7 @@ namespace storm { * @param argumentIndex The index of the argument to retrieve. * @return The i-th argument of this option. */ - ArgumentBase const& getArgument(uint_fast64_t argumentIndex) const { - STORM_LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds."); - return *this->arguments.at(argumentIndex); - } + ArgumentBase const& getArgument(uint_fast64_t argumentIndex) const; /*! * Retrieves the i-th argument of this option. @@ -129,10 +87,7 @@ namespace storm { * @param argumentIndex The index of the argument to retrieve. * @return The i-th argument of this option. */ - ArgumentBase& getArgument(uint_fast64_t argumentIndex) { - STORM_LOG_THROW(argumentIndex < this->getArgumentCount(), storm::exceptions::IllegalArgumentException, "Index of argument is out of bounds."); - return *this->arguments.at(argumentIndex); - } + ArgumentBase& getArgument(uint_fast64_t argumentIndex); /*! * Returns a reference to the argument with the specified long name. @@ -140,83 +95,63 @@ namespace storm { * @param argumentName The name of the argument to retrieve. * @return The argument with the given name. */ - ArgumentBase const& getArgumentByName(std::string const& argumentName) const { - auto argumentIterator = this->argumentNameMap.find(argumentName); - STORM_LOG_THROW(argumentIterator != this->argumentNameMap.end(), storm::exceptions::IllegalArgumentException, "Unable to retrieve argument with unknown name '" << argumentName << "'."); - return *argumentIterator->second; - } + ArgumentBase const& getArgumentByName(std::string const& argumentName) const; /*! * Retrieves the long name of this option. * * @return The long name of this option. */ - std::string const& getLongName() const { - return this->longName; - } + std::string const& getLongName() const; /*! * Retrieves whether this option has a short name. * * @return True iff the option has a short name. */ - bool getHasShortName() const { - return this->hasShortName; - } + bool getHasShortName() const; /*! * Retrieves the short name of this option. * * @return The short name of this option. */ - std::string const& getShortName() const { - return this->shortName; - } + std::string const& getShortName() const; /*! * Retrieves the description of the option. * * @return The description of the option. */ - std::string const& getDescription() const { - return this->description; - } + std::string const& getDescription() const; /*! * Retrieves the name of the module to which this option belongs. * * @return The name of the module to which this option belongs. */ - std::string const& getModuleName() const { - return this->moduleName; - } + std::string const& getModuleName() const; /*! * Retrieves whether the option is required. * * @return True iff the option is required. */ - bool getIsRequired() const { - return this->isRequired; - } + bool getIsRequired() const; /*! * Retrieves whether the option requires the module name as a prefix. * * @return True iff the option requires the module name as a prefix. */ - bool getRequiresModulePrefix() const { - return this->requireModulePrefix; - } + bool getRequiresModulePrefix() const; /*! * Retrieves whether the option has been set. * * @return True iff the option has been set. */ - bool getHasOptionBeenSet() const { - return this->hasBeenSet; - } + bool getHasOptionBeenSet() const; /*! * Retrieves the arguments of the option. @@ -234,36 +169,36 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, Option const& option); - private: + private: // The long name of the option. - std::string longName; + std::string longName; // A flag that indicates whether the option has a short name. bool hasShortName; // The short name of the option if any is set and an empty string otherwise. - std::string shortName; + std::string shortName; // The description of the option. - std::string description; + std::string description; // The name of the module to which this option belongs. - std::string moduleName; + std::string moduleName; // A flag that indicates whether this option is required to appear. - bool isRequired; + bool isRequired; // A flag that indicates whether this option is required to be prefixed with the module name. bool requireModulePrefix; // A flag that indicates whether this option has been set. - bool hasBeenSet; + bool hasBeenSet; // The arguments of this option (possibly empty). - std::vector> arguments; + std::vector> arguments; // A mapping from argument names of this option to the actual arguments. - std::unordered_map> argumentNameMap; + std::unordered_map> argumentNameMap; /*! * Creates an option with the given parameters. @@ -278,32 +213,14 @@ namespace storm { * module name. * @param optionArguments The arguments of the option. */ - Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(optionArguments), argumentNameMap() { - - // First, do some sanity checks. - STORM_LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name."); - STORM_LOG_THROW(!moduleName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty module name."); - - bool longNameContainsNonAlpha = std::find_if(longName.begin(), longName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != longName.end(); - STORM_LOG_THROW(!longNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal long name '" << longName << "'."); - - bool shortNameContainsNonAlpha = std::find_if(shortName.begin(), shortName.end(), [](char c) { return !(std::isalpha(c) || std::isdigit(c)); }) != shortName.end(); - STORM_LOG_THROW(!shortNameContainsNonAlpha, storm::exceptions::IllegalArgumentException, "Unable to construct option with illegal short name '" << shortName << "'."); - - // Then index all arguments. - for (auto const& argument : arguments) { - argumentNameMap.emplace(argument->getName(), argument); - } - } + Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector> const& optionArguments = std::vector>()); /*! * Sets the flag that marks the option as being (un)set. * * @param newValue The new status of the flag. */ - void setHasOptionBeenSet(bool newValue = true) { - this->hasBeenSet = newValue; - } + void setHasOptionBeenSet(bool newValue = true); }; } } diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h index abcd35862..622a7cb1c 100644 --- a/src/settings/OptionBuilder.h +++ b/src/settings/OptionBuilder.h @@ -21,7 +21,7 @@ namespace storm { namespace settings { /*! - * This class provides the interface to create an option. + * This class provides the interface to create an option... */ class OptionBuilder { public: diff --git a/src/settings/SettingMemento.h b/src/settings/SettingMemento.h index 551142fd2..bfbbcf9c3 100644 --- a/src/settings/SettingMemento.h +++ b/src/settings/SettingMemento.h @@ -1,7 +1,8 @@ #ifndef STORM_SETTINGS_SETTINGMEMENTO_H_ #define STORM_SETTINGS_SETTINGMEMENTO_H_ -#include "src/settings/SettingsManager.h" +#include + namespace storm { namespace settings { diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 857badfe6..96466d3c9 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include #include #include @@ -12,6 +13,21 @@ #include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/OptionParserException.h" #include "src/utility/storm-version.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/DebugSettings.h" +#include "src/settings/modules/CounterexampleGeneratorSettings.h" +#include "src/settings/modules/CuddSettings.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" +#include "src/settings/modules/BisimulationSettings.h" +#include "src/settings/modules/GlpkSettings.h" +#include "src/settings/modules/GurobiSettings.h" +#include "src/settings/modules/ParametricSettings.h" +#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" +#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" +#include "src/utility/macros.h" +#include "src/settings/Option.h" + namespace storm { namespace settings { diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 1a97bb07a..f4fad9919 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -2,9 +2,6 @@ #define STORM_SETTINGS_SETTINGSMANAGER_H_ #include -#include -#include -#include #include #include #include @@ -12,31 +9,24 @@ #include #include -#include "src/settings/Option.h" -#include "src/settings/OptionBuilder.h" -#include "src/settings/ArgumentBase.h" -#include "src/settings/Argument.h" -#include "src/settings/ArgumentBuilder.h" -#include "src/settings/ArgumentType.h" -#include "src/settings/modules/ModuleSettings.h" -#include "src/settings/modules/GeneralSettings.h" -#include "src/settings/modules/DebugSettings.h" -#include "src/settings/modules/CounterexampleGeneratorSettings.h" -#include "src/settings/modules/CuddSettings.h" -#include "src/settings/modules/GmmxxEquationSolverSettings.h" -#include "src/settings/modules/NativeEquationSolverSettings.h" -#include "src/settings/modules/BisimulationSettings.h" -#include "src/settings/modules/GlpkSettings.h" -#include "src/settings/modules/GurobiSettings.h" -#include "src/settings/modules/ParametricSettings.h" -#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" -#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" - -#include "src/utility/macros.h" -#include "src/exceptions/OptionParserException.h" - namespace storm { namespace settings { + namespace modules { + class GeneralSettings; + class DebugSettings; + class CounterexampleGeneratorSettings; + class CuddSettings; + class GmmxxEquationSolverSettings; + class NativeEquationSolverSettings; + class BisimulationSettings; + class GlpkSettings; + class GurobiSettings; + class TopologicalValueIterationEquationSolverSettings; + class ParametricSettings; + class SparseDtmcEliminationModelCheckerSettings; + class ModuleSettings; + } + class Option; /*! * Provides the central API for the registration of command line options and parsing the options from the diff --git a/src/settings/modules/BisimulationSettings.cpp b/src/settings/modules/BisimulationSettings.cpp index 291b9c9b5..db3bdce9e 100644 --- a/src/settings/modules/BisimulationSettings.cpp +++ b/src/settings/modules/BisimulationSettings.cpp @@ -1,5 +1,9 @@ #include "src/settings/modules/BisimulationSettings.h" - +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" namespace storm { diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp index 6191b1643..e4f8d2a32 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp @@ -2,6 +2,11 @@ #include "src/settings/SettingsManager.h" #include "src/exceptions/InvalidSettingsException.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" +#include "src/settings/modules/GeneralSettings.h" namespace storm { namespace settings { diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp index c494b5ca6..02f0db53f 100644 --- a/src/settings/modules/CuddSettings.cpp +++ b/src/settings/modules/CuddSettings.cpp @@ -2,6 +2,11 @@ #include "src/settings/SettingsManager.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + namespace storm { namespace settings { namespace modules { diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp index e0236d2ea..cf2867181 100644 --- a/src/settings/modules/DebugSettings.cpp +++ b/src/settings/modules/DebugSettings.cpp @@ -1,6 +1,10 @@ #include "src/settings/modules/DebugSettings.h" #include "src/settings/SettingsManager.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/Argument.h" +#include "src/settings/ArgumentBuilder.h" namespace storm { namespace settings { @@ -11,7 +15,7 @@ namespace storm { const std::string DebugSettings::traceOptionName = "trace"; const std::string DebugSettings::logfileOptionName = "logfile"; const std::string DebugSettings::logfileOptionShortName = "l"; - + DebugSettings::DebugSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build()); diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 807823f67..7a9ae2971 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -2,6 +2,12 @@ #include "src/settings/SettingsManager.h" #include "src/settings/SettingMemento.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + + #include "src/exceptions/InvalidSettingsException.h" namespace storm { diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp index 030a69006..7474feb00 100644 --- a/src/settings/modules/GlpkSettings.cpp +++ b/src/settings/modules/GlpkSettings.cpp @@ -1,6 +1,11 @@ #include "src/settings/modules/GlpkSettings.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" namespace storm { namespace settings { diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp index 359836968..dbaf8832a 100644 --- a/src/settings/modules/GmmxxEquationSolverSettings.cpp +++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp @@ -1,6 +1,12 @@ #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" namespace storm { namespace settings { diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp index 86751cc1d..b669a45d3 100644 --- a/src/settings/modules/GurobiSettings.cpp +++ b/src/settings/modules/GurobiSettings.cpp @@ -1,6 +1,11 @@ #include "src/settings/modules/GurobiSettings.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" namespace storm { namespace settings { diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp index f29e15109..befea1589 100644 --- a/src/settings/modules/ModuleSettings.cpp +++ b/src/settings/modules/ModuleSettings.cpp @@ -1,7 +1,9 @@ #include "src/settings/modules/ModuleSettings.h" #include "src/settings/SettingMemento.h" +#include "src/settings/Option.h" #include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/IllegalFunctionCallException.h" namespace storm { namespace settings { diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h index 383174647..89776ce46 100644 --- a/src/settings/modules/ModuleSettings.h +++ b/src/settings/modules/ModuleSettings.h @@ -3,14 +3,15 @@ #include #include +#include -#include "src/settings/Option.h" namespace storm { namespace settings { // Forward-declare some classes. class SettingsManager; class SettingMemento; + class Option; namespace modules { diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp index 482713ed8..5584308c5 100644 --- a/src/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/settings/modules/NativeEquationSolverSettings.cpp @@ -1,6 +1,12 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + namespace storm { namespace settings { diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp index 89a62a008..a1388f308 100644 --- a/src/settings/modules/ParametricSettings.cpp +++ b/src/settings/modules/ParametricSettings.cpp @@ -1,6 +1,10 @@ #include "src/settings/modules/ParametricSettings.h" -#include "src/settings/SettingsManager.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + namespace storm { namespace settings { diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp index ce4221c7d..6a2528a5b 100644 --- a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp +++ b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp @@ -1,6 +1,10 @@ #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" -#include "src/settings/SettingsManager.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + namespace storm { namespace settings { diff --git a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp index a277ac07a..1be47979a 100644 --- a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp +++ b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp @@ -1,6 +1,12 @@ #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" namespace storm { namespace settings { diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index fd36a0bff..f2082e32a 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -13,7 +13,10 @@ #include "src/exceptions/InvalidAccessException.h" #include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/settings/modules/DebugSettings.h" +#include "src/settings/modules/GlpkSettings.h" namespace storm { namespace solver { GlpkLpSolver::GlpkLpSolver(std::string const& name, ModelSense const& modelSense) : LpSolver(modelSense), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() { diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index 835d2194e..123e0c440 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -8,6 +8,7 @@ #include "src/utility/vector.h" #include "src/utility/constants.h" #include "src/exceptions/InvalidStateException.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" #include "gmm/gmm_iter_solvers.h" diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index 58ae540a5..a92130b7e 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -7,6 +7,9 @@ #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/utility/vector.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" + namespace storm { namespace solver { diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp index b6c0202f7..bb1a070fb 100644 --- a/src/solver/GurobiLpSolver.cpp +++ b/src/solver/GurobiLpSolver.cpp @@ -6,12 +6,16 @@ #include "src/storage/expressions/LinearCoefficientVisitor.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/DebugSettings.h" +#include "src/settings/modules/GurobiSettings.h" + #include "src/utility/macros.h" #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/ExpressionManager.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidAccessException.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace solver { diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 8b69058cf..2c31f67cb 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -3,9 +3,12 @@ #include -#include "src/storage/SparseMatrix.h" namespace storm { + namespace storage { + template class SparseMatrix; + } + namespace solver { /*! diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index ea8d4bf4d..312eaecf5 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -3,6 +3,8 @@ #include #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + #include "src/utility/vector.h" #include "src/exceptions/InvalidStateException.h" diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index f701ee79c..22eb207ad 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -2,7 +2,11 @@ #include + + #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/utility/vector.h" #include "src/solver/NativeLinearEquationSolver.h" diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index 8ad635be5..8faab2914 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -3,6 +3,9 @@ #include "src/storage/dd/CuddBdd.h" #include "src/storage/dd/CuddAdd.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + namespace storm { namespace solver { diff --git a/src/solver/SymbolicLinearEquationSolver.cpp b/src/solver/SymbolicLinearEquationSolver.cpp index 5ec30cbb1..d53489392 100644 --- a/src/solver/SymbolicLinearEquationSolver.cpp +++ b/src/solver/SymbolicLinearEquationSolver.cpp @@ -3,6 +3,12 @@ #include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/Add.h" + + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + namespace storm { namespace solver { diff --git a/src/solver/SymbolicLinearEquationSolver.h b/src/solver/SymbolicLinearEquationSolver.h index 7defb0b79..007f28df6 100644 --- a/src/solver/SymbolicLinearEquationSolver.h +++ b/src/solver/SymbolicLinearEquationSolver.h @@ -7,11 +7,16 @@ #include #include "src/storage/expressions/Variable.h" -#include "src/storage/dd/Bdd.h" -#include "src/storage/dd/Add.h" -#include "src/storage/dd/Odd.h" +#include "src/storage/dd/DdType.h" + namespace storm { + namespace dd { + template class Add; + template class Bdd; + + } + namespace solver { /*! * An interface that represents an abstract symbolic linear equation solver. In addition to solving a system of diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index fc2725a3b..d3d122e12 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -1,14 +1,19 @@ #include "src/solver/TopologicalMinMaxLinearEquationSolver.h" #include - -#include "src/settings/SettingsManager.h" #include "src/utility/vector.h" #include "src/utility/graph.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/exceptions/IllegalArgumentException.h" #include "src/exceptions/InvalidStateException.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" +#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" + + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 395202ed1..6006934d0 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -14,6 +14,11 @@ #include "src/utility/constants.h" #include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/InvalidOptionException.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + namespace storm { namespace storage { diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index ac8a38144..53277ec2d 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -10,8 +10,14 @@ #include "src/storage/SparseMatrix.h" #include "src/adapters/CarlAdapter.h" +#include "src/storage/BitVector.h" +#include "src/utility/constants.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/NotImplementedException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/OutOfRangeException.h" + #include "src/utility/macros.h" #include "log4cplus/logger.h" diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index dbee2e94a..633128dd0 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -9,6 +9,10 @@ #include "src/utility/vector.h" #include "src/utility/macros.h" + +#include "src/storage/SparseMatrix.h" + + #include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotImplementedException.h" diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index 03c8b3a2c..76b949d6b 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -2,11 +2,11 @@ #define STORM_STORAGE_DD_CUDDADD_H_ #include +#include #include "src/storage/dd/Add.h" #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdForwardIterator.h" -#include "src/storage/SparseMatrix.h" #include "src/storage/expressions/Variable.h" #include "src/utility/OsDetection.h" @@ -14,6 +14,12 @@ #include "cuddObj.hh" namespace storm { + namespace storage { + template class SparseMatrix; + class BitVector; + template class MatrixEntry; + } + namespace dd { // Forward-declare some classes. template class DdManager; diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp index 30ed8a191..3c2ff4ad3 100644 --- a/src/storage/dd/CuddBdd.cpp +++ b/src/storage/dd/CuddBdd.cpp @@ -7,6 +7,10 @@ #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/storage/BitVector.h" + +#include "src/logic/ComparisonType.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h index ad2d9aa6a..3ce4f9d89 100644 --- a/src/storage/dd/CuddBdd.h +++ b/src/storage/dd/CuddBdd.h @@ -1,22 +1,34 @@ #ifndef STORM_STORAGE_DD_CUDDBDD_H_ #define STORM_STORAGE_DD_CUDDBDD_H_ -#include "src/logic/ComparisonType.h" #include "src/storage/dd/Bdd.h" #include "src/storage/dd/CuddDd.h" -#include "src/storage/dd/CuddAdd.h" -#include "src/storage/expressions/Variable.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" namespace storm { + namespace logic { + enum class ComparisonType; + } + + namespace expressions { + class Variable; + } + + namespace storage { + class BitVector; + } + + + namespace dd { // Forward-declare some classes. template class DdManager; template class Odd; template class Add; + template class DdForwardIterator; template<> class Bdd : public Dd { diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index d84f3e602..b5f31e442 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -4,9 +4,14 @@ #include "src/storage/dd/CuddDdManager.h" #include "src/utility/macros.h" +#include "src/storage/expressions/Variable.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/CuddSettings.h" #include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/dd/CuddAdd.h" +#include "CuddBdd.h" + namespace storm { namespace dd { diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index 5bf1c3080..ec6a3b57d 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -6,7 +6,6 @@ #include "src/storage/dd/DdManager.h" #include "src/storage/dd/CuddDdMetaVariable.h" -#include "src/storage/expressions/Variable.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. diff --git a/src/storage/dd/CuddDdMetaVariable.h b/src/storage/dd/CuddDdMetaVariable.h index fea461229..54673c83d 100644 --- a/src/storage/dd/CuddDdMetaVariable.h +++ b/src/storage/dd/CuddDdMetaVariable.h @@ -8,7 +8,6 @@ #include "utility/OsDetection.h" #include "src/storage/dd/CuddBdd.h" -#include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/DdMetaVariable.h" #include "src/storage/dd/CuddDdForwardIterator.h" @@ -18,6 +17,7 @@ namespace storm { // Forward-declare some classes. template class DdManager; template class Odd; + template class Add; template<> class DdMetaVariable { diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index 29301957e..d851ffaa0 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -1,6 +1,10 @@ #include "src/storage/dd/CuddOdd.h" #include +#include + +#include "src/exceptions/InvalidArgumentException.h" +#include "src/utility/macros.h" #include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddDdMetaVariable.h" diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 9d6f10c8f..d58d1a940 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -4,6 +4,7 @@ #include "src/storage/expressions/ExpressionManager.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index 40e8c4693..efa026c7e 100644 --- a/src/utility/cli.cpp +++ b/src/utility/cli.cpp @@ -1,5 +1,9 @@ #include "cli.h" + +#include "src/settings/modules/DebugSettings.h" +#include "src/exceptions/OptionParserException.h" + // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB # include "tbb/tbb_stddef.h" @@ -196,6 +200,100 @@ namespace storm { } return true; } + + void processOptions() { + if (storm::settings::debugSettings().isLogfileSet()) { + initializeFileLogging(); + } + + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); + + // If we have to build the model from a symbolic representation, we need to parse the representation first. + boost::optional program; + if (settings.isSymbolicSet()) { + std::string const& programFile = settings.getSymbolicModelFilename(); + program = storm::parser::PrismParser::parse(programFile).simplify(); + + program->checkValidity(); + std::cout << program.get() << std::endl; + } + + // Then proceed to parsing the property (if given), since the model we are building may depend on the property. + std::vector>> formulas; + if (settings.isPropertySet()) { + boost::optional> formula; + if (program) { + storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); + formula = formulaParser.parseFromString(settings.getProperty()); + } else { + storm::parser::FormulaParser formulaParser; + formula = formulaParser.parseFromString(settings.getProperty()); + } + formulas.push_back(formula); + } + else if (settings.isPropertyFileSet()) { + std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl; + + std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in); + + std::vector properties; + + if (inputFileStream.good()) { + try { + while (inputFileStream.good()) { + std::string prop; + std::getline(inputFileStream, prop); + if (!prop.empty()) { + properties.push_back(prop); + } + } + } + catch (std::exception& e) { + inputFileStream.close(); + throw e; + } + inputFileStream.close(); + } else { + STORM_LOG_ERROR("Unable to read property file."); + } + + for (std::string prop : properties) { + boost::optional> formula; + try { + if (program) { + storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); + formula = formulaParser.parseFromString(prop); + } else { + storm::parser::FormulaParser formulaParser; + formula = formulaParser.parseFromString(prop); + } + formulas.push_back(formula); + } + catch (storm::exceptions::WrongFormatException &e) { + STORM_LOG_WARN("Unable to parse line as formula: " << prop); + } + } + std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl; + } + + for (boost::optional> formula : formulas) { + if (settings.isSymbolicSet()) { +#ifdef STORM_HAVE_CARL + if (settings.isParametricSet()) { + buildAndCheckSymbolicModel(program.get(), formula); + } else { +#endif + buildAndCheckSymbolicModel(program.get(), formula); +#ifdef STORM_HAVE_CARL + } +#endif + } else if (settings.isExplicitSet()) { + buildAndCheckExplicitModel(formula); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); + } + } + } } } diff --git a/src/utility/cli.h b/src/utility/cli.h index 63de731b3..917ff57d5 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -19,6 +19,10 @@ #include "src/utility/OsDetection.h" #include "src/settings/SettingsManager.h" + +#include "src/settings/modules/BisimulationSettings.h" +#include "src/settings/modules/ParametricSettings.h" + // Headers related to parsing. #include "src/parser/AutoParser.h" #include "src/parser/PrismParser.h" @@ -32,6 +36,9 @@ #include "src/models/sparse/Model.h" #include "src/models/symbolic/Model.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + // Headers of builders. #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/builder/DdPrismModelBuilder.h" @@ -387,99 +394,7 @@ namespace storm { } } - inline void processOptions() { - if (storm::settings::debugSettings().isLogfileSet()) { - initializeFileLogging(); - } - - storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - - // If we have to build the model from a symbolic representation, we need to parse the representation first. - boost::optional program; - if (settings.isSymbolicSet()) { - std::string const& programFile = settings.getSymbolicModelFilename(); - program = storm::parser::PrismParser::parse(programFile).simplify(); - - program->checkValidity(); - std::cout << program.get() << std::endl; - } - - // Then proceed to parsing the property (if given), since the model we are building may depend on the property. - std::vector>> formulas; - if (settings.isPropertySet()) { - boost::optional> formula; - if (program) { - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - formula = formulaParser.parseFromString(settings.getProperty()); - } else { - storm::parser::FormulaParser formulaParser; - formula = formulaParser.parseFromString(settings.getProperty()); - } - formulas.push_back(formula); - } - else if (settings.isPropertyFileSet()) { - std::cout << "Reading properties from " << settings.getPropertiesFilename() << std::endl; - - std::ifstream inputFileStream(settings.getPropertiesFilename(), std::ios::in); - - std::vector properties; - - if (inputFileStream.good()) { - try { - while (inputFileStream.good()) { - std::string prop; - std::getline(inputFileStream, prop); - if (!prop.empty()) { - properties.push_back(prop); - } - } - } - catch (std::exception& e) { - inputFileStream.close(); - throw e; - } - inputFileStream.close(); - } else { - STORM_LOG_ERROR("Unable to read property file."); - } - - for (std::string prop : properties) { - boost::optional> formula; - try { - if (program) { - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - formula = formulaParser.parseFromString(prop); - } else { - storm::parser::FormulaParser formulaParser; - formula = formulaParser.parseFromString(prop); - } - formulas.push_back(formula); - } - catch (storm::exceptions::WrongFormatException &e) { - STORM_LOG_WARN("Unable to parse line as formula: " << prop); - } - } - std::cout << "Parsed " << formulas.size() << " properties from file " << settings.getPropertiesFilename() << std::endl; - } - - for (boost::optional> formula : formulas) { - if (settings.isSymbolicSet()) { -#ifdef STORM_HAVE_CARL - if (settings.isParametricSet()) { - buildAndCheckSymbolicModel(program.get(), formula); - } else { -#endif - buildAndCheckSymbolicModel(program.get(), formula); -#ifdef STORM_HAVE_CARL - } -#endif - } else if (settings.isExplicitSet()) { - buildAndCheckExplicitModel(formula); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); - } - } - } + void processOptions(); } } } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 4604b3cb2..8b518413c 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -2,6 +2,8 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/sparse/StateType.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" namespace storm { namespace utility { @@ -55,6 +57,83 @@ namespace storm { return value; } + // For floats we specialize this class and consider the comparison modulo some predefined precision. + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + ConstantsComparator(float precision); + + bool isOne(float const& value) const; + + bool isZero(float const& value) const; + + bool isEqual(float const& value1, float const& value2) const; + + bool isConstant(float const& value) const; + + private: + // The precision used for comparisons. + float precision; + }; + + // For doubles we specialize this class and consider the comparison modulo some predefined precision. + template<> + class ConstantsComparator { + public: + ConstantsComparator(); + + ConstantsComparator(double precision); + + bool isOne(double const& value) const; + + bool isZero(double const& value) const; + + bool isInfinity(double const& value) const; + + bool isEqual(double const& value1, double const& value2) const; + + bool isConstant(double const& value) const; + + private: + // The precision used for comparisons. + double precision; + }; + +#ifdef STORM_HAVE_CARL + template<> + RationalFunction& simplify(RationalFunction& value); + + template<> + RationalFunction&& simplify(RationalFunction&& value); + + template<> + class ConstantsComparator { + public: + bool isOne(storm::RationalFunction const& value) const; + + bool isZero(storm::RationalFunction const& value) const; + + bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; + + bool isConstant(storm::RationalFunction const& value) const; + }; + + template<> + class ConstantsComparator { + public: + bool isOne(storm::Polynomial const& value) const; + + bool isZero(storm::Polynomial const& value) const; + + bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; + + bool isConstant(storm::Polynomial const& value) const; + }; +#endif + + template bool ConstantsComparator::isOne(ValueType const& value) const { return value == one(); diff --git a/src/utility/constants.h b/src/utility/constants.h index e8573130c..82994f16f 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -12,7 +12,6 @@ #include #include -#include "src/settings/SettingsManager.h" #include "src/adapters/CarlAdapter.h" namespace storm { @@ -32,19 +31,11 @@ namespace storm { template ValueType infinity(); - -#ifdef STORM_HAVE_CARL - template<> - storm::RationalFunction infinity(); -#endif + template ValueType pow(ValueType const& value, uint_fast64_t exponent); - -#ifdef STORM_HAVE_CARL - template<> - RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); -#endif + template ValueType simplify(ValueType value); @@ -58,83 +49,13 @@ namespace storm { bool isZero(ValueType const& value) const; bool isEqual(ValueType const& value1, ValueType const& value2) const; - }; - - // For floats we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - ConstantsComparator(float precision); - - bool isOne(float const& value) const; - bool isZero(float const& value) const; + bool isConstant(ValueType const& value) const; - bool isEqual(float const& value1, float const& value2) const; - - bool isConstant(float const& value) const; - - private: - // The precision used for comparisons. - float precision; + bool isInfinity(ValueType const& value) const; }; - // For doubles we specialize this class and consider the comparison modulo some predefined precision. - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - ConstantsComparator(double precision); - - bool isOne(double const& value) const; - - bool isZero(double const& value) const; - - bool isInfinity(double const& value) const; - - bool isEqual(double const& value1, double const& value2) const; - - bool isConstant(double const& value) const; - - private: - // The precision used for comparisons. - double precision; - }; - -#ifdef STORM_HAVE_CARL - template<> - RationalFunction& simplify(RationalFunction& value); - - template<> - RationalFunction&& simplify(RationalFunction&& value); - - template<> - class ConstantsComparator { - public: - bool isOne(storm::RationalFunction const& value) const; - - bool isZero(storm::RationalFunction const& value) const; - - bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; - - bool isConstant(storm::RationalFunction const& value) const; - }; - - template<> - class ConstantsComparator { - public: - bool isOne(storm::Polynomial const& value) const; - - bool isZero(storm::Polynomial const& value) const; - - bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; - - bool isConstant(storm::Polynomial const& value) const; - }; -#endif + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); diff --git a/src/utility/initialize.cpp b/src/utility/initialize.cpp index b0998972b..a20619720 100644 --- a/src/utility/initialize.cpp +++ b/src/utility/initialize.cpp @@ -1,5 +1,9 @@ #include "initialize.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/DebugSettings.h" + + log4cplus::Logger logger; log4cplus::Logger printer; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 1cc0ea445..14cd65396 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -14,6 +14,9 @@ #include "src/solver/GurobiLpSolver.h" #include "src/solver/GlpkLpSolver.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + namespace storm { namespace utility { namespace solver { diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index c93ac830a..096d83fbf 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -1,9 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/settings/SettingMemento.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" #include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index 8b8fde965..8c0a6e81e 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -4,6 +4,8 @@ #include "src/parser/PrismParser.h" #include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/settings/modules/GeneralSettings.h" + TEST(ExplicitPrismModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 80300f1f4..76f178e8f 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -11,6 +11,8 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 9bbedfa7b..01f97ba61 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -6,6 +6,8 @@ #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index a720507a4..f5580a179 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -14,6 +14,8 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index e2dfdcfd4..4919a2e69 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -11,6 +11,8 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 571492a5b..935cf9fb3 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -12,6 +12,10 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/GmmxxEquationSolverSettings.h" + TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 41eade466..69dcda869 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -6,6 +6,9 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/GmmxxEquationSolverSettings.h" #include "src/parser/AutoParser.h" TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 688acda91..a7ee670b6 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -12,6 +12,8 @@ #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + TEST(SparseCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 169289035..8cade7ab9 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -14,6 +14,7 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 26869f425..ad5aa1a1a 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -11,6 +11,9 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index a74d9059d..ba6e37abd 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -12,6 +12,8 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 59b2ad23f..87a4f0e21 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -6,6 +6,8 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" + +#include "src/settings/modules/GeneralSettings.h" #include "src/parser/AutoParser.h" TEST(SparseMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 55bb8443f..e14a146d6 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -5,6 +5,8 @@ #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" + +#include "src/settings/modules/GeneralSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 916633101..3ecea41a7 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -11,6 +11,8 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 4920fe746..a71930f44 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -7,6 +7,9 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" + +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp index a92987875..3a07f46f7 100644 --- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp @@ -10,6 +10,8 @@ #include "src/parser/DeterministicSparseTransitionParser.h" #include "src/storage/SparseMatrix.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/settings/SettingMemento.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" diff --git a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp index b8bb2e3cd..83b2f2ae5 100644 --- a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -8,6 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp index 3f9017d1f..07fef8955 100644 --- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -11,6 +11,9 @@ #include "src/parser/NondeterministicSparseTransitionParser.h" #include "src/storage/SparseMatrix.h" #include "src/settings/SettingMemento.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index e41606d7f..d2ea6db1c 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -2,8 +2,13 @@ #include "storm-config.h" #include "src/storage/dd/CuddDdManager.h" - +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" #include "src/utility/solver.h" +#include "src/settings/SettingsManager.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(FullySymbolicGameSolverTest, Solve) { // Create some variables. diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp index 3c0112cf7..c19c605a0 100644 --- a/test/functional/solver/GlpkLpSolverTest.cpp +++ b/test/functional/solver/GlpkLpSolverTest.cpp @@ -8,6 +8,8 @@ #include "src/exceptions/InvalidAccessException.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + #include "src/storage/expressions/Expressions.h" TEST(GlpkLpSolver, LPOptimizeMax) { diff --git a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp index f4db7c409..5d6ccde26 100644 --- a/test/functional/solver/GmmxxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxLinearEquationSolverTest.cpp @@ -4,6 +4,8 @@ #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" + TEST(GmmxxLinearEquationSolver, SolveWithStandardOptions) { ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); storm::storage::SparseMatrixBuilder builder; diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index bd402d915..5b4174e51 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -3,6 +3,8 @@ #include "src/solver/GmmxxMinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/storage/SparseMatrix.h" TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index 7e1547333..b8fd4f256 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -6,6 +6,7 @@ #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidAccessException.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expressions.h" diff --git a/test/functional/solver/NativeLinearEquationSolverTest.cpp b/test/functional/solver/NativeLinearEquationSolverTest.cpp index 3d30d6b4f..844b0c5c9 100644 --- a/test/functional/solver/NativeLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeLinearEquationSolverTest.cpp @@ -4,6 +4,8 @@ #include "src/solver/NativeLinearEquationSolver.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(NativeLinearEquationSolver, SolveWithStandardOptions) { ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); storm::storage::SparseMatrixBuilder builder; diff --git a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp index 10c630395..bb7c281c9 100644 --- a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -4,6 +4,9 @@ #include "src/solver/NativeMinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" +#include "src/storage/SparseMatrix.h" + TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) { storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index ea15855fa..4acf5b489 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -5,6 +5,9 @@ #include "src/storage/dd/CuddAdd.h" #include "src/storage/dd/CuddOdd.h" #include "src/storage/dd/DdMetaVariable.h" +#include "src/settings/SettingsManager.h" + +#include "src/storage/SparseMatrix.h" TEST(CuddDdManager, Constants) { std::shared_ptr> manager(new storm::dd::DdManager()); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index c1deafcd3..2d4d7615d 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -10,6 +10,9 @@ #include "src/builder/DdPrismModelBuilder.h" #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/utility/graph.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddDdManager.h" TEST(GraphTest, SymbolicProb01) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");