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

Removed many superfluous includes, added some source files -- towards faster compilation 

Former-commit-id: a575a97d40
main
sjunges 11 years ago
parent
a129983ae9
commit
3c2040f4b7
119 changed files with 1077 additions and 729 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/adapters/AddExpressionAdapter.cpp
  2. 158
      src/builder/DdPrismModelBuilder.cpp
  3. 171
      src/builder/DdPrismModelBuilder.h
  4. 4
      src/builder/ExplicitPrismModelBuilder.cpp
  5. 4
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  6. 2
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  7. 8
      src/logic/ComparisonType.cpp
  8. 2
      src/logic/ComparisonType.h
  9. 1
      src/logic/Formula.h
  10. 2
      src/logic/ReachabilityRewardFormula.h
  11. 2
      src/modelchecker/AbstractModelChecker.cpp
  12. 3
      src/modelchecker/AbstractModelChecker.h
  13. 6
      src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
  14. 4
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  15. 3
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  16. 4
      src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
  17. 4
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  18. 3
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  19. 3
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  20. 4
      src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
  21. 3
      src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
  22. 6
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  23. 17
      src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
  24. 2
      src/modelchecker/results/HybridQuantitativeCheckResult.cpp
  25. 1
      src/modelchecker/results/SymbolicQualitativeCheckResult.cpp
  26. 2
      src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
  27. 1
      src/models/sparse/Ctmc.cpp
  28. 5
      src/models/symbolic/Ctmc.cpp
  29. 4
      src/models/symbolic/DeterministicModel.cpp
  30. 5
      src/models/symbolic/Dtmc.cpp
  31. 6
      src/models/symbolic/Mdp.cpp
  32. 8
      src/models/symbolic/Model.cpp
  33. 17
      src/models/symbolic/Model.h
  34. 5
      src/models/symbolic/NondeterministicModel.cpp
  35. 5
      src/models/symbolic/StochasticTwoPlayerGame.cpp
  36. 1
      src/parser/DeterministicSparseTransitionParser.cpp
  37. 2
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  38. 1
      src/parser/NondeterministicSparseTransitionParser.cpp
  39. 123
      src/settings/Argument.h
  40. 1
      src/settings/ArgumentBase.cpp
  41. 1
      src/settings/ArgumentBase.h
  42. 4
      src/settings/ArgumentValidators.h
  43. 127
      src/settings/Option.cpp
  44. 123
      src/settings/Option.h
  45. 2
      src/settings/OptionBuilder.h
  46. 3
      src/settings/SettingMemento.h
  47. 16
      src/settings/SettingsManager.cpp
  48. 42
      src/settings/SettingsManager.h
  49. 6
      src/settings/modules/BisimulationSettings.cpp
  50. 5
      src/settings/modules/CounterexampleGeneratorSettings.cpp
  51. 5
      src/settings/modules/CuddSettings.cpp
  52. 4
      src/settings/modules/DebugSettings.cpp
  53. 6
      src/settings/modules/GeneralSettings.cpp
  54. 5
      src/settings/modules/GlpkSettings.cpp
  55. 6
      src/settings/modules/GmmxxEquationSolverSettings.cpp
  56. 5
      src/settings/modules/GurobiSettings.cpp
  57. 2
      src/settings/modules/ModuleSettings.cpp
  58. 3
      src/settings/modules/ModuleSettings.h
  59. 6
      src/settings/modules/NativeEquationSolverSettings.cpp
  60. 6
      src/settings/modules/ParametricSettings.cpp
  61. 6
      src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp
  62. 6
      src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp
  63. 3
      src/solver/GlpkLpSolver.cpp
  64. 1
      src/solver/GmmxxLinearEquationSolver.cpp
  65. 3
      src/solver/GmmxxMinMaxLinearEquationSolver.cpp
  66. 4
      src/solver/GurobiLpSolver.cpp
  67. 5
      src/solver/MinMaxLinearEquationSolver.h
  68. 2
      src/solver/NativeLinearEquationSolver.cpp
  69. 4
      src/solver/NativeMinMaxLinearEquationSolver.cpp
  70. 3
      src/solver/SymbolicGameSolver.cpp
  71. 6
      src/solver/SymbolicLinearEquationSolver.cpp
  72. 11
      src/solver/SymbolicLinearEquationSolver.h
  73. 9
      src/solver/TopologicalMinMaxLinearEquationSolver.cpp
  74. 5
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  75. 6
      src/storage/SparseMatrix.cpp
  76. 4
      src/storage/dd/CuddAdd.cpp
  77. 8
      src/storage/dd/CuddAdd.h
  78. 4
      src/storage/dd/CuddBdd.cpp
  79. 18
      src/storage/dd/CuddBdd.h
  80. 5
      src/storage/dd/CuddDdManager.cpp
  81. 1
      src/storage/dd/CuddDdManager.h
  82. 2
      src/storage/dd/CuddDdMetaVariable.h
  83. 4
      src/storage/dd/CuddOdd.cpp
  84. 1
      src/storage/prism/Program.cpp
  85. 98
      src/utility/cli.cpp
  86. 101
      src/utility/cli.h
  87. 79
      src/utility/constants.cpp
  88. 83
      src/utility/constants.h
  89. 4
      src/utility/initialize.cpp
  90. 3
      src/utility/solver.cpp
  91. 4
      test/functional/builder/DdPrismModelBuilderTest.cpp
  92. 2
      test/functional/builder/ExplicitPrismModelBuilderTest.cpp
  93. 2
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  94. 2
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  95. 2
      test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  96. 2
      test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  97. 4
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  98. 3
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  99. 2
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  100. 1
      test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp

4
src/adapters/AddExpressionAdapter.cpp
View File

@ -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 {

158
src/builder/DdPrismModelBuilder.cpp
View File

@ -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 <storm::dd::DdType Type>
class DdPrismModelBuilder<Type>::GenerationInformation {
public:
GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() {
// Initializes variables and identity DDs.
createMetaVariablesAndIdentities();
rowExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToRowMetaVariableMap));
columnExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToColumnMetaVariableMap));
}
// The program that is currently translated.
storm::prism::Program const& program;
// The manager used to build the decision diagrams.
std::shared_ptr<storm::dd::DdManager<Type>> manager;
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
// The meta variables used to encode the nondeterminism.
std::vector<storm::expressions::Variable> nondeterminismMetaVariables;
// The meta variables used to encode the synchronization.
std::vector<storm::expressions::Variable> 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<storm::expressions::Variable> allNondeterminismVariables;
// DDs representing the identity for each variable.
std::map<storm::expressions::Variable, storm::dd::Add<Type>> variableToIdentityMap;
// DDs representing the identity for each module.
std::map<std::string, storm::dd::Add<Type>> moduleToIdentityMap;
// DDs representing the valid ranges of the variables of each module.
std::map<std::string, storm::dd::Add<Type>> moduleToRangeMap;
private:
/*!
* Creates the required meta variables and variable/module identities.
*/
void createMetaVariablesAndIdentities() {
// Add synchronization variables.
for (auto const& actionIndex : program.getActionIndices()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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<Type> moduleIdentity = manager->getAddOne();
storm::dd::Add<Type> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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 <storm::dd::DdType Type>
DdPrismModelBuilder<Type>::Options::Options() : buildRewards(false), rewardModelName(), constantDefinitions() {
// Intentionally left empty.

171
src/builder/DdPrismModelBuilder.h
View File

@ -4,13 +4,30 @@
#include <map>
#include <boost/optional.hpp>
#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<storm::dd::DdType T> class Bdd;
}
namespace models {
namespace symbolic {
template<storm::dd::DdType T> class Model;
}
}
namespace builder {
template <storm::dd::DdType Type>
@ -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<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() {
// Initializes variables and identity DDs.
createMetaVariablesAndIdentities();
rowExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToRowMetaVariableMap));
columnExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToColumnMetaVariableMap));
}
// The program that is currently translated.
storm::prism::Program const& program;
// The manager used to build the decision diagrams.
std::shared_ptr<storm::dd::DdManager<Type>> manager;
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
// The meta variables used to encode the nondeterminism.
std::vector<storm::expressions::Variable> nondeterminismMetaVariables;
// The meta variables used to encode the synchronization.
std::vector<storm::expressions::Variable> 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<storm::expressions::Variable> allNondeterminismVariables;
// DDs representing the identity for each variable.
std::map<storm::expressions::Variable, storm::dd::Add<Type>> variableToIdentityMap;
// DDs representing the identity for each module.
std::map<std::string, storm::dd::Add<Type>> moduleToIdentityMap;
// DDs representing the valid ranges of the variables of each module.
std::map<std::string, storm::dd::Add<Type>> moduleToRangeMap;
private:
/*!
* Creates the required meta variables and variable/module identities.
*/
void createMetaVariablesAndIdentities() {
// Add synchronization variables.
for (auto const& actionIndex : program.getActionIndices()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Variable> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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<Type> moduleIdentity = manager->getAddOne();
storm::dd::Add<Type> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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<storm::expressions::Variable, storm::expressions::Variable> 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<Type> 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<Type> encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value);

4
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -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"

4
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -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 {

2
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -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"

8
src/logic/ComparisonType.cpp
View File

@ -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;
}

2
src/logic/ComparisonType.h
View File

@ -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);
}

1
src/logic/Formula.h
View File

@ -5,7 +5,6 @@
#include <vector>
#include <iostream>
#include "src/modelchecker/results/CheckResult.h"
namespace storm {
namespace logic {

2
src/logic/ReachabilityRewardFormula.h
View File

@ -4,7 +4,7 @@
#include <memory>
#include "src/logic/RewardPathFormula.h"
#include "src/logic/StateFormula.h"
namespace storm {
namespace logic {

2
src/modelchecker/AbstractModelChecker.cpp
View File

@ -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 {

3
src/modelchecker/AbstractModelChecker.h
View File

@ -5,8 +5,11 @@
#include "src/logic/Formulas.h"
namespace storm {
namespace modelchecker {
class CheckResult;
class AbstractModelChecker {
public:
virtual ~AbstractModelChecker() {

6
src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
View File

@ -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<storm::dd::DdType DdType, class ValueType>

4
src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -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"

3
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
View File

@ -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"

4
src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
View File

@ -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"

4
src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
View File

@ -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"

3
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -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"

3
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -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"

4
src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
View File

@ -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"

3
src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
View File

@ -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"

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

@ -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 {

17
src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
View File

@ -7,6 +7,7 @@
#include "src/exceptions/InvalidOperationException.h"
#include "src/adapters/CarlAdapter.h"
namespace storm {
namespace modelchecker {
template<typename ValueType>
@ -114,28 +115,28 @@ namespace storm {
vector_type const& valuesAsVector = boost::get<vector_type>(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<map_type>(values);
std::map<storm::storage::sparse::state_type, bool> 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;
}

2
src/modelchecker/results/HybridQuantitativeCheckResult.cpp
View File

@ -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 {

1
src/modelchecker/results/SymbolicQualitativeCheckResult.cpp
View File

@ -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 {

2
src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
View File

@ -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 {

1
src/models/sparse/Ctmc.cpp
View File

@ -1,6 +1,7 @@
#include "src/models/sparse/Ctmc.h"
#include "src/adapters/CarlAdapter.h"
#include "src/utility/macros.h"
namespace storm {
namespace models {

5
src/models/symbolic/Ctmc.cpp
View File

@ -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 {

4
src/models/symbolic/DeterministicModel.cpp
View File

@ -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 {

5
src/models/symbolic/Dtmc.cpp
View File

@ -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 {

6
src/models/symbolic/Mdp.cpp
View File

@ -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 {

8
src/models/symbolic/Model.cpp
View File

@ -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 {

17
src/models/symbolic/Model.h
View File

@ -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<storm::dd::DdType Type> class Dd;
template<storm::dd::DdType Type> class Add;
template<storm::dd::DdType Type> class Bdd;
template<storm::dd::DdType Type> class DdManager;
}
namespace adapters {
template<storm::dd::DdType Type> class AddExpressionAdapter;
}
namespace models {
namespace symbolic {

5
src/models/symbolic/NondeterministicModel.cpp
View File

@ -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 {

5
src/models/symbolic/StochasticTwoPlayerGame.cpp
View File

@ -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 {

1
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -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"

2
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -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 {

1
src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -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"

123
src/settings/Argument.h
View File

@ -12,13 +12,10 @@
#include <memory>
#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 {
@ -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<userValidationFunction_t> const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) {
// Intentionally left empty.
}
Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> 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<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
this->setDefaultValue(defaultValue);
}
Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> 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 conversionOk = false;
T newValue = ArgumentBase::convertFromString<T>(fromStringValue, conversionOk);
if (!conversionOk) {
return false;
}
return this->setFromTypeValue(newValue);
}
bool setFromStringValue(std::string const& fromStringValue) override;
bool setFromTypeValue(T const& newValue, bool hasBeenSet = true) {
if (!this->validate(newValue)) {
return false;
}
this->argumentValue = newValue;
this->hasBeenSet = hasBeenSet;
return true;
}
bool setFromTypeValue(T const& newValue, bool hasBeenSet = true);
virtual ArgumentType getType() const override {
return this->argumentType;
}
virtual ArgumentType getType() const override;
/*!
* Checks whether the given argument is compatible with the current one. If not, an exception is thrown.
@ -105,75 +80,23 @@ namespace storm {
*
* @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;
}
}
T const& getArgumentValue() const;
virtual bool getHasDefaultValue() const override {
return this->hasDefaultValue;
}
virtual bool getHasDefaultValue() const override;
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.");
}
void setFromDefaultValue() override;
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 std::string getValueAsString() const override;
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;
}
}
virtual int_fast64_t getValueAsInteger() const override;
virtual uint_fast64_t getValueAsUnsignedInteger() const 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 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;
};
}

1
src/settings/ArgumentBase.cpp
View File

@ -1,5 +1,6 @@
#include "src/settings/ArgumentBase.h"
#include <boost/algorithm/string.hpp>
#include <iomanip>
namespace storm {

1
src/settings/ArgumentBase.h
View File

@ -3,7 +3,6 @@
#include <iostream>
#include <string>
#include <boost/algorithm/string.hpp>
#include "src/settings/ArgumentType.h"

4
src/settings/ArgumentValidators.h
View File

@ -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 {

127
src/settings/Option.cpp
View File

@ -1,9 +1,136 @@
#include "src/settings/Option.h"
#include <iomanip>
#include <string>
#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 {
Option::Option(std::string const& moduleName, std::string const& longOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> 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<std::shared_ptr<ArgumentBase>> 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<storm::settings::Argument<std::string> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<std::string> const&>(secondArgument));
break;
case ArgumentType::Integer:
static_cast<storm::settings::Argument<int_fast64_t> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<int_fast64_t> const&>(secondArgument));
break;
case ArgumentType::UnsignedInteger:
static_cast<storm::settings::Argument<uint_fast64_t> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<uint_fast64_t> const&>(secondArgument));
break;
case ArgumentType::Double:
static_cast<storm::settings::Argument<double> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<double> const&>(secondArgument));
break;
case ArgumentType::Boolean:
static_cast<storm::settings::Argument<bool> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<bool> 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<std::shared_ptr<ArgumentBase>> 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;
}
uint_fast64_t Option::getPrintLength() const {
uint_fast64_t length = 2;
if (!this->getRequiresModulePrefix()) {

123
src/settings/Option.h
View File

@ -4,19 +4,13 @@
#include <iostream>
#include <string>
#include <cstdint>
#include <cctype>
#include <vector>
#include <memory>
#include <algorithm>
#include <unordered_set>
#include "ArgumentType.h"
#include <unordered_map>
#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,6 +20,7 @@ namespace storm {
namespace modules {
class ModuleSettings;
}
class ArgumentBase;
/*!
* This class represents one command-line option.
@ -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<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : 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<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
/*!
* 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<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : 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<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
/*!
* 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<storm::settings::Argument<std::string> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<std::string> const&>(secondArgument));
break;
case ArgumentType::Integer:
static_cast<storm::settings::Argument<int_fast64_t> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<int_fast64_t> const&>(secondArgument));
break;
case ArgumentType::UnsignedInteger:
static_cast<storm::settings::Argument<uint_fast64_t> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<uint_fast64_t> const&>(secondArgument));
break;
case ArgumentType::Double:
static_cast<storm::settings::Argument<double> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<double> const&>(secondArgument));
break;
case ArgumentType::Boolean:
static_cast<storm::settings::Argument<bool> const&>(firstArgument).isCompatibleWith(static_cast<storm::settings::Argument<bool> 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.
@ -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<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : 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<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>());
/*!
* 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);
};
}
}

2
src/settings/OptionBuilder.h
View File

@ -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:

3
src/settings/SettingMemento.h
View File

@ -1,7 +1,8 @@
#ifndef STORM_SETTINGS_SETTINGMEMENTO_H_
#define STORM_SETTINGS_SETTINGMEMENTO_H_
#include "src/settings/SettingsManager.h"
#include <string>
namespace storm {
namespace settings {

16
src/settings/SettingsManager.cpp
View File

@ -4,6 +4,7 @@
#include <cctype>
#include <mutex>
#include <iomanip>
#include <fstream>
#include <regex>
#include <set>
#include <boost/algorithm/string.hpp>
@ -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 {

42
src/settings/SettingsManager.h
View File

@ -2,9 +2,6 @@
#define STORM_SETTINGS_SETTINGSMANAGER_H_
#include <iostream>
#include <sstream>
#include <list>
#include <set>
#include <utility>
#include <functional>
#include <unordered_map>
@ -12,31 +9,24 @@
#include <vector>
#include <memory>
#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

6
src/settings/modules/BisimulationSettings.cpp
View File

@ -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 {

5
src/settings/modules/CounterexampleGeneratorSettings.cpp
View File

@ -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 {

5
src/settings/modules/CuddSettings.cpp
View File

@ -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 {

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

@ -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 {

6
src/settings/modules/GeneralSettings.cpp
View File

@ -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 {

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

@ -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 {

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

@ -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 {

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

@ -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 {

2
src/settings/modules/ModuleSettings.cpp
View File

@ -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 {

3
src/settings/modules/ModuleSettings.h
View File

@ -3,14 +3,15 @@
#include <string>
#include <unordered_map>
#include <vector>
#include "src/settings/Option.h"
namespace storm {
namespace settings {
// Forward-declare some classes.
class SettingsManager;
class SettingMemento;
class Option;
namespace modules {

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

@ -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 {

6
src/settings/modules/ParametricSettings.cpp
View File

@ -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 {

6
src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp
View File

@ -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 {

6
src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp
View File

@ -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 {

3
src/solver/GlpkLpSolver.cpp
View File

@ -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() {

1
src/solver/GmmxxLinearEquationSolver.cpp
View File

@ -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"

3
src/solver/GmmxxMinMaxLinearEquationSolver.cpp
View File

@ -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 {

4
src/solver/GurobiLpSolver.cpp
View File

@ -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 {

5
src/solver/MinMaxLinearEquationSolver.h
View File

@ -3,9 +3,12 @@
#include <vector>
#include "src/storage/SparseMatrix.h"
namespace storm {
namespace storage {
template<typename T> class SparseMatrix;
}
namespace solver {
/*!

2
src/solver/NativeLinearEquationSolver.cpp
View File

@ -3,6 +3,8 @@
#include <utility>
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/utility/vector.h"
#include "src/exceptions/InvalidStateException.h"

4
src/solver/NativeMinMaxLinearEquationSolver.cpp
View File

@ -2,7 +2,11 @@
#include <utility>
#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"

3
src/solver/SymbolicGameSolver.cpp
View File

@ -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 {

6
src/solver/SymbolicLinearEquationSolver.cpp
View File

@ -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 {

11
src/solver/SymbolicLinearEquationSolver.h
View File

@ -7,11 +7,16 @@
#include <boost/variant.hpp>
#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<storm::dd::DdType T> class Add;
template<storm::dd::DdType T> class Bdd;
}
namespace solver {
/*!
* An interface that represents an abstract symbolic linear equation solver. In addition to solving a system of

9
src/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -1,14 +1,19 @@
#include "src/solver/TopologicalMinMaxLinearEquationSolver.h"
#include <utility>
#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;

5
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -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 {

6
src/storage/SparseMatrix.cpp
View File

@ -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"

4
src/storage/dd/CuddAdd.cpp
View File

@ -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"

8
src/storage/dd/CuddAdd.h
View File

@ -2,11 +2,11 @@
#define STORM_STORAGE_DD_CUDDADD_H_
#include <boost/optional.hpp>
#include <map>
#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<typename T> class SparseMatrix;
class BitVector;
template<typename E, typename V> class MatrixEntry;
}
namespace dd {
// Forward-declare some classes.
template<DdType Type> class DdManager;

4
src/storage/dd/CuddBdd.cpp
View File

@ -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"

18
src/storage/dd/CuddBdd.h
View File

@ -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<DdType Type> class DdManager;
template<DdType Type> class Odd;
template<DdType Type> class Add;
template<DdType Type> class DdForwardIterator;
template<>
class Bdd<DdType::CUDD> : public Dd<DdType::CUDD> {

5
src/storage/dd/CuddDdManager.cpp
View File

@ -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 {

1
src/storage/dd/CuddDdManager.h
View File

@ -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.

2
src/storage/dd/CuddDdMetaVariable.h
View File

@ -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<DdType Type> class DdManager;
template<DdType Type> class Odd;
template<DdType Type> class Add;
template<>
class DdMetaVariable<DdType::CUDD> {

4
src/storage/dd/CuddOdd.cpp
View File

@ -1,6 +1,10 @@
#include "src/storage/dd/CuddOdd.h"
#include <algorithm>
#include <boost/functional/hash.hpp>
#include "src/exceptions/InvalidArgumentException.h"
#include "src/utility/macros.h"
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddDdMetaVariable.h"

1
src/storage/prism/Program.cpp
View File

@ -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"

98
src/utility/cli.cpp
View File

@ -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"
@ -197,6 +201,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<storm::prism::Program> 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<boost::optional<std::shared_ptr<storm::logic::Formula>>> formulas;
if (settings.isPropertySet()) {
boost::optional<std::shared_ptr<storm::logic::Formula>> 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<std::string> 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<std::shared_ptr<storm::logic::Formula>> 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<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
if (settings.isSymbolicSet()) {
#ifdef STORM_HAVE_CARL
if (settings.isParametricSet()) {
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
} else {
#endif
buildAndCheckSymbolicModel<double>(program.get(), formula);
#ifdef STORM_HAVE_CARL
}
#endif
} else if (settings.isExplicitSet()) {
buildAndCheckExplicitModel<double>(formula);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
}
}
}
}

101
src/utility/cli.h
View File

@ -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<storm::prism::Program> 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<boost::optional<std::shared_ptr<storm::logic::Formula>>> formulas;
if (settings.isPropertySet()) {
boost::optional<std::shared_ptr<storm::logic::Formula>> 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<std::string> 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<std::shared_ptr<storm::logic::Formula>> 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<std::shared_ptr<storm::logic::Formula>> formula : formulas) {
if (settings.isSymbolicSet()) {
#ifdef STORM_HAVE_CARL
if (settings.isParametricSet()) {
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
} else {
#endif
buildAndCheckSymbolicModel<double>(program.get(), formula);
#ifdef STORM_HAVE_CARL
}
#endif
} else if (settings.isExplicitSet()) {
buildAndCheckExplicitModel<double>(formula);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
}
void processOptions();
}
}
}

79
src/utility/constants.cpp
View File

@ -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<float> {
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<double> {
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<storm::RationalFunction> {
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<storm::Polynomial> {
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<typename ValueType>
bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const {
return value == one<ValueType>();

83
src/utility/constants.h
View File

@ -12,7 +12,6 @@
#include <limits>
#include <cstdint>
#include "src/settings/SettingsManager.h"
#include "src/adapters/CarlAdapter.h"
namespace storm {
@ -33,18 +32,10 @@ namespace storm {
template<typename ValueType>
ValueType infinity();
#ifdef STORM_HAVE_CARL
template<>
storm::RationalFunction infinity();
#endif
template<typename ValueType>
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<typename ValueType>
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<float> {
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<double> {
public:
ConstantsComparator();
ConstantsComparator(double precision);
bool isOne(double const& value) const;
bool isZero(double const& value) const;
bool isConstant(ValueType 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<storm::RationalFunction> {
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;
bool isInfinity(ValueType const& value) const;
};
template<>
class ConstantsComparator<storm::Polynomial> {
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<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);

4
src/utility/initialize.cpp
View File

@ -1,5 +1,9 @@
#include "initialize.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/DebugSettings.h"
log4cplus::Logger logger;
log4cplus::Logger printer;

3
src/utility/solver.cpp
View File

@ -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 {

4
test/functional/builder/DdPrismModelBuilderTest.cpp
View File

@ -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"

2
test/functional/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -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");

2
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -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.

2
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

@ -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"

2
test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
View File

@ -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.

2
test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -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");

4
test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

@ -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");

3
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -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) {

2
test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
View File

@ -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<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);

1
test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
View File

@ -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.

Some files were not shown because too many files changed in this diff

Write Preview
Loading…
Cancel
Save