From 5e428a795afe24baddacc346fde42ca764764b55 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 18 Aug 2015 13:31:13 +0200 Subject: [PATCH 1/9] And more includes on the right spot. Former-commit-id: 72bb348687d518fe5ef35633fbbacc16dba6bdea --- .../MILPMinimalLabelSetGenerator.h | 1 + .../prctl/HybridMdpPrctlModelChecker.cpp | 1 + .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 1 + src/utility/solver.cpp | 8 ++++-- src/utility/solver.h | 25 +++++++++++-------- .../GmmxxCtmcCslModelCheckerTest.cpp | 2 ++ .../GmmxxDtmcPrctlModelCheckerTest.cpp | 1 + .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 2 ++ .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 2 ++ .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 4 +-- .../GmmxxMdpPrctlModelCheckerTest.cpp | 2 ++ .../NativeCtmcCslModelCheckerTest.cpp | 2 ++ .../NativeDtmcPrctlModelCheckerTest.cpp | 2 ++ .../NativeHybridCtmcCslModelCheckerTest.cpp | 2 ++ .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 2 ++ .../NativeHybridMdpPrctlModelCheckerTest.cpp | 2 ++ .../NativeMdpPrctlModelCheckerTest.cpp | 2 ++ .../SymbolicDtmcPrctlModelCheckerTest.cpp | 2 ++ .../solver/FullySymbolicGameSolverTest.cpp | 1 + .../GmmxxDtmcPrctModelCheckerTest.cpp | 1 + .../GmmxxMdpPrctlModelCheckerTest.cpp | 1 + .../NativeDtmcPrctlModelCheckerTest.cpp | 2 ++ .../NativeMdpPrctlModelCheckerTest.cpp | 2 ++ 23 files changed, 56 insertions(+), 14 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 1339d646a..26c1113c8 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -17,6 +17,7 @@ #include "src/utility/graph.h" #include "src/utility/counterexamples.h" #include "src/utility/solver.h" +#include "src/solver/LpSolver.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 3f83672b2..bd3f493e9 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -10,6 +10,7 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/settings/modules/GeneralSettings.h" diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 30720b091..0e7e4a136 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -10,6 +10,7 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/solver/SymbolicLinearEquationSolver.h" #include "src/settings/modules/GeneralSettings.h" diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 14cd65396..b58e74cb5 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -1,9 +1,9 @@ #include "src/utility/solver.h" -#include "src/settings/SettingsManager.h" - #include "src/solver/SymbolicGameSolver.h" + +#include "src/solver/SymbolicLinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h" @@ -16,6 +16,10 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + +#include "src/exceptions/InvalidSettingsException.h" + namespace storm { namespace utility { diff --git a/src/utility/solver.h b/src/utility/solver.h index cd56695f0..661bd90ba 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -1,20 +1,25 @@ #ifndef STORM_UTILITY_SOLVER_H_ #define STORM_UTILITY_SOLVER_H_ -#include "src/solver/SymbolicGameSolver.h" - -#include "src/solver/SymbolicLinearEquationSolver.h" -#include "src/solver/LinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" -#include "src/solver/MinMaxLinearEquationSolver.h" -#include "src/solver/LpSolver.h" - #include "src/storage/dd/DdType.h" -#include "src/settings/modules/NativeEquationSolverSettings.h" - -#include "src/exceptions/InvalidSettingsException.h" namespace storm { + namespace solver { + template class SymbolicGameSolver; + template class SymbolicLinearEquationSolver; + template class LinearEquationSolver; + template class MinMaxLinearEquationSolver; + class LpSolver; + } + namespace dd { + template class Add; + template class Bdd; + } + namespace expressions { + class Variable; + } + namespace utility { namespace solver { template diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 76f178e8f..fea32ac90 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -12,6 +12,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 01f97ba61..0735dbcfd 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -8,6 +8,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index f5580a179..874a667af 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -17,6 +17,8 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 4919a2e69..e66a9bb6e 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -14,6 +14,8 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 935cf9fb3..d480c01af 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -10,10 +10,10 @@ #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" -#include "src/settings/SettingsManager.h" +#include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" - +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 69dcda869..ac5c62f15 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -9,6 +9,8 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/parser/AutoParser.h" TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index a7ee670b6..2e6684ae5 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -14,6 +14,8 @@ #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(SparseCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index ced23c35e..f9dc4ff7b 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -9,6 +9,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 8cade7ab9..aeb28084d 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -16,6 +16,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index ad5aa1a1a..eca106543 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -15,6 +15,8 @@ #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index ba6e37abd..e1913a1de 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -14,6 +14,8 @@ #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 87a4f0e21..d3bee454d 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -8,6 +8,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/parser/AutoParser.h" TEST(SparseMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 3ecea41a7..52638f8b7 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -11,6 +11,8 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index d2ea6db1c..ce9e21798 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -7,6 +7,7 @@ #include "src/utility/solver.h" #include "src/settings/SettingsManager.h" +#include "src/solver/SymbolicGameSolver.h" #include "src/settings/modules/NativeEquationSolverSettings.h" diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index ea480bd22..0ecce639f 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 1db6f796d..527dbed69 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/utility/solver.h" diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index bc0b5b563..cce9c8878 100644 --- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -2,6 +2,8 @@ #include "storm-config.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 788f1fee6..e327910d8 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -4,6 +4,8 @@ #include "src/settings/SettingsManager.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/utility/solver.h" #include "src/parser/AutoParser.h" From 9201c6420a8462fb3345353a82058ba776100abb Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 19 Aug 2015 10:17:11 +0200 Subject: [PATCH 2/9] Removes identity assignments Former-commit-id: bdf15fd4c1bf67bd256a346e3ef14bfba238b5b9 --- src/storage/prism/Assignment.cpp | 15 +++++++++++++++ src/storage/prism/Assignment.h | 7 +++++++ src/storage/prism/Command.cpp | 16 ++++++++++++++++ src/storage/prism/Command.h | 8 ++++++++ src/storage/prism/Program.cpp | 12 ++++++++++-- src/storage/prism/Update.cpp | 17 ++++++++++++++++- src/storage/prism/Update.h | 6 ++++++ 7 files changed, 78 insertions(+), 3 deletions(-) diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp index 3628c76ef..a6c8b4456 100644 --- a/src/storage/prism/Assignment.cpp +++ b/src/storage/prism/Assignment.cpp @@ -1,4 +1,5 @@ #include "Assignment.h" +#include namespace storm { namespace prism { @@ -22,6 +23,20 @@ namespace storm { return Assignment(this->getVariable(), this->getExpression().substitute(substitution).simplify(), this->getFilename(), this->getLineNumber()); } + bool Assignment::isIdentity() const { + if(this->expression.isVariable()) { + assert(this->expression.getVariables().size() == 1); + //if( variable == *(this->expression.getVariables().begin())) { + // std::cout << variable.getName() << " == " << (this->expression.getVariables().begin())->getName() << std::endl; + //} + //else { + // std::cout << "********" << variable.getName() << " != " << (this->expression.getVariables().begin())->getName() << std::endl; + //} + return variable == *(this->expression.getVariables().begin()); + } + return false; + } + std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { stream << "(" << assignment.getVariableName() << "' = " << assignment.getExpression() << ")"; return stream; diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h index cb6006ba7..1c45a2b78 100644 --- a/src/storage/prism/Assignment.h +++ b/src/storage/prism/Assignment.h @@ -60,6 +60,13 @@ namespace storm { */ Assignment substitute(std::map const& substitution) const; + /*! + * Checks whether the assignment is an identity (lhs equals rhs) + * + * @return true iff the assignment is of the form a' = a. + */ + bool isIdentity() const; + friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment); private: diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index e2b1d3698..5cad634e7 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -1,4 +1,5 @@ #include "Command.h" +#include namespace storm { namespace prism { @@ -31,6 +32,7 @@ namespace storm { } storm::prism::Update const& Command::getUpdate(uint_fast64_t index) const { + assert(index < getNumberOfUpdates()); return this->updates[index]; } @@ -71,6 +73,20 @@ namespace storm { return true; } + Command Command::removeIdentityAssignmentsFromUpdates() const { + std::vector newUpdates; + newUpdates.reserve(this->getNumberOfUpdates()); + for (auto const& update : this->getUpdates()) { + newUpdates.emplace_back(update.removeIdentityAssignments()); + } + return copyWithNewUpdates(std::move(newUpdates)); + + } + + Command Command::copyWithNewUpdates(std::vector && newUpdates) const { + return Command(this->globalIndex, this->markovian, this->getActionIndex(), this->getActionName(), guardExpression, newUpdates, this->getFilename(), this->getLineNumber()); + } + std::ostream& operator<<(std::ostream& stream, Command const& command) { if (command.isMarkovian()) { stream << "<" << command.getActionName() << "> "; diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h index dd8b2f9b6..658cce67d 100644 --- a/src/storage/prism/Command.h +++ b/src/storage/prism/Command.h @@ -128,6 +128,12 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, Command const& command); + /** + * Removes identity assignments from the updates + * @return The resulting command + */ + Command removeIdentityAssignmentsFromUpdates() const; + private: // The index of the action associated with this command. uint_fast64_t actionIndex; @@ -150,6 +156,8 @@ namespace storm { // A flag indicating whether the command is labeled. bool labeled; + + Command copyWithNewUpdates(std::vector&& newUpdates) const; }; } // namespace prism diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index d58d1a940..611943b16 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -781,6 +781,14 @@ namespace storm { std::vector newModules; std::vector newConstants = this->getConstants(); for (auto const& module : this->getModules()) { + // Remove identity assignments from the updates + std::vector newCommands; + for (auto const& command : module.getCommands()) { + newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates()); + } + + // Substitute Variables by Global constants if possible. + std::map booleanVars; std::map integerVars; for (auto const& variable : module.getBooleanVariables()) { @@ -790,7 +798,7 @@ namespace storm { integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression()); } - for (auto const& command : module.getCommands()) { + for (auto const& command : newCommands) { // Check all updates. for (auto const& update : command.getUpdates()) { // Check all assignments. @@ -821,7 +829,7 @@ namespace storm { } } - newModules.emplace_back(module.getName(), newBVars, newIVars, module.getCommands()); + newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands); for(auto const& entry : booleanVars) { newConstants.emplace_back(entry.first, entry.second); diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index c00a9fbd2..9adf3b5b8 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -52,12 +52,27 @@ namespace storm { return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber()); } + Update Update::removeIdentityAssignments() const { + std::vector newAssignments; + newAssignments.reserve(getNumberOfAssignments()); + for(auto const& ass : this->assignments) { + if(!ass.isIdentity()) { + newAssignments.push_back(ass); + } + } + return Update(this->globalIndex, this->likelihoodExpression, newAssignments, getFilename(), getLineNumber()); + } + std::ostream& operator<<(std::ostream& stream, Update const& update) { stream << update.getLikelihoodExpression() << " : "; + if(update.getNumberOfAssignments() == 0) { + stream << "True"; + } + uint_fast64_t i = 0; for (auto const& assignment : update.getAssignments()) { stream << assignment; - if (i < update.getAssignments().size() - 1) { + if (i < update.getNumberOfAssignments() - 1) { stream << " & "; } ++i; diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h index 1ea5470f8..7b9ebdbc1 100644 --- a/src/storage/prism/Update.h +++ b/src/storage/prism/Update.h @@ -73,6 +73,12 @@ namespace storm { * @return The resulting update. */ Update substitute(std::map const& substitution) const; + /*! + * Removes all assignments which do not change the variable. + * + * @return The resulting update. + */ + Update removeIdentityAssignments() const; friend std::ostream& operator<<(std::ostream& stream, Update const& assignment); From 3c098f085a29033d8340151aa5a6b836cd34c54d Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 19 Aug 2015 10:17:49 +0200 Subject: [PATCH 3/9] In principal, we need a fixpoint iteration for the static simplification. For now, we just call simplify twice. Former-commit-id: 41d1d6e133544bef66a279c7966684d9e95a56f4 --- src/utility/cli.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index efa026c7e..106ea143c 100644 --- a/src/utility/cli.cpp +++ b/src/utility/cli.cpp @@ -212,7 +212,7 @@ namespace storm { boost::optional program; if (settings.isSymbolicSet()) { std::string const& programFile = settings.getSymbolicModelFilename(); - program = storm::parser::PrismParser::parse(programFile).simplify(); + program = storm::parser::PrismParser::parse(programFile).simplify().simplify(); program->checkValidity(); std::cout << program.get() << std::endl; From ba95065ce37cc43ae8b0e9932be52cc7f45f93be Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Aug 2015 21:04:53 +0200 Subject: [PATCH 4/9] Fixed memory leak by adding destructors for linear equation solvers. Previously, the member unique_ptr<...> gmmxxMatrix from the gmmxx subclasses was not deleted properly Former-commit-id: c21911b56a4f161e7a00582585265ee9e2e8d25f --- src/solver/LinearEquationSolver.h | 5 +++++ src/solver/MinMaxLinearEquationSolver.h | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 43b3f9ad5..61f26294e 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -15,6 +15,11 @@ namespace storm { template class LinearEquationSolver { public: + + virtual ~LinearEquationSolver() { + // Intentionally left empty. + } + /*! * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. * The solution of the set of linear equations will be written to the vector x. Note that the matrix A has diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 2c31f67cb..e9679a6b4 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -19,6 +19,11 @@ namespace storm { template class MinMaxLinearEquationSolver { public: + + virtual ~MinMaxLinearEquationSolver() { + // Intentionally left empty. + } + /*! * Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has * to be given upon construction time of the solver object. From 97c24fe22930e924901d38fc3b2316d18480ed0d Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 24 Aug 2015 11:44:11 +0200 Subject: [PATCH 5/9] solver settings now within solver, minmax refactored to share common variables Former-commit-id: b3c78ae0388158ca57613441d10937c6cbfc226c --- src/solver/MinMaxLinearEquationSolver.cpp | 19 +++++++++++ src/solver/SolverSelectionOptions.cpp | 32 +++++++++++++++++++ src/solver/SolverSelectionOptions.h | 20 ++++++++++++ .../ExtendSettingEnumWithSelectionField.h | 28 ++++++++++++++++ .../solver/MinMaxTechniqueSelectionTest.cpp | 11 +++++++ 5 files changed, 110 insertions(+) create mode 100644 src/solver/MinMaxLinearEquationSolver.cpp create mode 100644 src/solver/SolverSelectionOptions.cpp create mode 100644 src/solver/SolverSelectionOptions.h create mode 100644 src/utility/ExtendSettingEnumWithSelectionField.h create mode 100644 test/functional/solver/MinMaxTechniqueSelectionTest.cpp diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp new file mode 100644 index 000000000..2aad22bda --- /dev/null +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -0,0 +1,19 @@ +#include "MinMaxLinearEquationSolver.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" +#include + +namespace storm { + namespace solver { + AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : + precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackPolicy(trackPolicy) + { + + if(prefTech == MinMaxTechniqueSelection::FROMSETTINGS) { + useValueIteration = (storm::settings::generalSettings().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); + } else { + useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration); + } + } + } +} diff --git a/src/solver/SolverSelectionOptions.cpp b/src/solver/SolverSelectionOptions.cpp new file mode 100644 index 000000000..63e56eda7 --- /dev/null +++ b/src/solver/SolverSelectionOptions.cpp @@ -0,0 +1,32 @@ +#include "src/solver/SolverSelectionOptions.h" + +namespace storm { + namespace solver { + std::string toString(MinMaxTechnique m) { + switch(m) { + case MinMaxTechnique::PolicyIteration: + return "policy"; + case MinMaxTechnique::ValueIteration: + return "value"; + } + + } + std::string toString(LpSolverType t) { + switch(t) { + case LpSolverType::Gurobi: + return "Gurobi"; + case LpSolverType::Glpk: + return "Glpk"; + } + } + + std::string toString(EquationSolverType t) { + switch(t) { + case EquationSolverType::Native: + return "Native"; + case EquationSolverType::Gmmxx: + return "Gmmxx"; + } + } + } +} diff --git a/src/solver/SolverSelectionOptions.h b/src/solver/SolverSelectionOptions.h new file mode 100644 index 000000000..cfba09a15 --- /dev/null +++ b/src/solver/SolverSelectionOptions.h @@ -0,0 +1,20 @@ + +#ifndef SOLVERSELECTIONOPTIONS_H +#define SOLVERSELECTIONOPTIONS_H + + +#include "src/utility/ExtendSettingEnumWithSelectionField.h" + +namespace storm { + namespace solver { + ExtendEnumsWithSelectionField(MinMaxTechnique, PolicyIteration, ValueIteration) + + + ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk) + ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx) + + } +} + +#endif + diff --git a/src/utility/ExtendSettingEnumWithSelectionField.h b/src/utility/ExtendSettingEnumWithSelectionField.h new file mode 100644 index 000000000..997571f6e --- /dev/null +++ b/src/utility/ExtendSettingEnumWithSelectionField.h @@ -0,0 +1,28 @@ +#ifndef EXTENDSETTINGENUMWITHSELECTIONFIELD_H +#define EXTENDSETTINGENUMWITHSELECTIONFIELD_H + + + +#include +#include + + +#define ExtendEnumsWithSelectionField( NAME, ...) \ + enum class NAME : int { __VA_ARGS__ }; \ + enum class NAME##Selection : int { __VA_ARGS__, FROMSETTINGS }; \ + std::string toString(NAME); \ + inline NAME convert(NAME##Selection e) { \ + assert(e != NAME##Selection::FROMSETTINGS); \ + return static_cast< NAME >(e); \ + } \ + inline std::string toString(NAME##Selection e) { \ + if(e == NAME##Selection::FROMSETTINGS) { \ + return "[from settings]"; \ + }\ + else { \ + return toString(convert(e)); \ + } \ + } + +#endif /* EXTENDSETTINGENUMWITHSELECTIONFIELD_H */ + diff --git a/test/functional/solver/MinMaxTechniqueSelectionTest.cpp b/test/functional/solver/MinMaxTechniqueSelectionTest.cpp new file mode 100644 index 000000000..78cc8696e --- /dev/null +++ b/test/functional/solver/MinMaxTechniqueSelectionTest.cpp @@ -0,0 +1,11 @@ +#include "gtest/gtest.h" + +#include "src/solver/MinMaxLinearEquationSolver.h" + +TEST( MinMaxTechnique, Simple ) { + storm::solver::MinMaxTechniqueSelection ts = storm::solver::MinMaxTechniqueSelection::PolicyIteration; + storm::solver::MinMaxTechnique t = storm::solver::MinMaxTechnique::PolicyIteration; + ASSERT_EQ(convert(ts), t); + + +} \ No newline at end of file From faf31156e0b7a7502542cfe142d4b9b28683438c Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 24 Aug 2015 16:36:30 +0200 Subject: [PATCH 6/9] fix for last changes + is probabilistic Former-commit-id: 38df3f515f5ffe3aee5f9d2d1dc6ca97d3a38137 --- src/settings/modules/GeneralSettings.cpp | 20 +++--- src/settings/modules/GeneralSettings.h | 20 +++--- src/settings/modules/GlpkSettings.cpp | 3 +- .../modules/GmmxxEquationSolverSettings.cpp | 3 +- src/settings/modules/GurobiSettings.cpp | 4 +- .../modules/NativeEquationSolverSettings.cpp | 4 +- ...alValueIterationEquationSolverSettings.cpp | 3 +- .../GmmxxMinMaxLinearEquationSolver.cpp | 55 ++++++-------- src/solver/GmmxxMinMaxLinearEquationSolver.h | 18 +---- src/solver/MinMaxLinearEquationSolver.cpp | 8 +++ src/solver/MinMaxLinearEquationSolver.h | 48 ++++++++++++- .../NativeMinMaxLinearEquationSolver.cpp | 72 ++++++++----------- src/solver/NativeMinMaxLinearEquationSolver.h | 19 +---- .../TopologicalMinMaxLinearEquationSolver.cpp | 19 ++--- .../TopologicalMinMaxLinearEquationSolver.h | 4 +- src/storage/SparseMatrix.cpp | 11 +++ src/storage/SparseMatrix.h | 12 +++- src/utility/solver.cpp | 20 +++--- src/utility/solver.h | 2 + src/utility/vector.h | 20 +++++- .../GmmxxMinMaxLinearEquationSolverTest.cpp | 2 +- .../NativeMinMaxLinearEquationSolverTest.cpp | 2 +- 22 files changed, 202 insertions(+), 167 deletions(-) diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 7a9ae2971..1274deebf 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" - +#include "src/solver/SolverSelectionOptions.h" #include "src/exceptions/InvalidSettingsException.h" @@ -241,12 +241,12 @@ namespace storm { return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger(); } - GeneralSettings::EquationSolver GeneralSettings::getEquationSolver() const { + storm::solver::EquationSolverType GeneralSettings::getEquationSolver() const { std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); if (equationSolverName == "gmm++") { - return GeneralSettings::EquationSolver::Gmmxx; + return storm::solver::EquationSolverType::Gmmxx; } else if (equationSolverName == "native") { - return GeneralSettings::EquationSolver::Native; + return storm::solver::EquationSolverType::Native; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); } @@ -255,12 +255,12 @@ namespace storm { return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); } - GeneralSettings::LpSolver GeneralSettings::getLpSolver() const { + storm::solver::LpSolverType GeneralSettings::getLpSolver() const { std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); if (lpSolverName == "gurobi") { - return GeneralSettings::LpSolver::Gurobi; + return storm::solver::LpSolverType::Gurobi; } else if (lpSolverName == "glpk") { - return GeneralSettings::LpSolver::glpk; + return storm::solver::LpSolverType::Glpk; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); } @@ -297,12 +297,12 @@ namespace storm { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } - GeneralSettings::MinMaxTechnique GeneralSettings::getMinMaxEquationSolvingTechnique() const { + storm::solver::MinMaxTechnique GeneralSettings::getMinMaxEquationSolvingTechnique() const { std::string minMaxEquationSolvingTechnique = this->getOption(minMaxEquationSolvingTechniqueOptionName).getArgumentByName("name").getValueAsString(); if (minMaxEquationSolvingTechnique == "valueIteration") { - return GeneralSettings::MinMaxTechnique::ValueIteration; + return storm::solver::MinMaxTechnique::ValueIteration; } else if (minMaxEquationSolvingTechnique == "policyIteration") { - return GeneralSettings::MinMaxTechnique::PolicyIteration; + return storm::solver::MinMaxTechnique::PolicyIteration; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index f2454a28f..d344528af 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -5,6 +5,12 @@ #include "src/settings/modules/ModuleSettings.h" namespace storm { + namespace solver { + enum class EquationSolverType; + enum class LpSolverType; + enum class MinMaxTechnique; + } + namespace settings { namespace modules { @@ -16,14 +22,6 @@ namespace storm { // An enumeration of all engines. enum class Engine { Sparse, Hybrid, Dd }; - // An enumeration of all available LP solvers. - enum class LpSolver { Gurobi, glpk }; - - // An enumeration of all available equation solvers. - enum class EquationSolver { Gmmxx, Native }; - - // An enumeration of all available Min/Max equation solver techniques. - enum class MinMaxTechnique { ValueIteration, PolicyIteration }; /*! * Creates a new set of general settings that is managed by the given manager. @@ -265,7 +263,7 @@ namespace storm { * * @return The selected convergence criterion. */ - EquationSolver getEquationSolver() const; + storm::solver::EquationSolverType getEquationSolver() const; /*! * Retrieves whether a equation solver has been set. @@ -279,7 +277,7 @@ namespace storm { * * @return The selected LP solver. */ - LpSolver getLpSolver() const; + storm::solver::LpSolverType getLpSolver() const; /*! * Retrieves whether the export-to-dot option was set. @@ -350,7 +348,7 @@ namespace storm { * * @return The selected min/max equation solving technique. */ - MinMaxTechnique getMinMaxEquationSolvingTechnique() const; + storm::solver::MinMaxTechnique getMinMaxEquationSolvingTechnique() const; bool check() const override; diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp index 7474feb00..a459ddbb8 100644 --- a/src/settings/modules/GlpkSettings.cpp +++ b/src/settings/modules/GlpkSettings.cpp @@ -6,6 +6,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -34,7 +35,7 @@ namespace storm { bool GlpkSettings::check() const { if (isOutputSet() || isIntegerToleranceSet()) { - STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::glpk, "glpk is not selected as the used LP solver, so setting options for glpk has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::solver::LpSolverType::Glpk, "glpk is not selected as the preferred LP solver, so setting options for glpk might have no effect."); } return true; diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp index dbaf8832a..00526dbf3 100644 --- a/src/settings/modules/GmmxxEquationSolverSettings.cpp +++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp @@ -7,6 +7,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -107,7 +108,7 @@ namespace storm { bool GmmxxEquationSolverSettings::check() const { bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "gmm++ is not selected as the preferred equation solver, so setting options for gmm++ might have no effect."); return true; } diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp index b669a45d3..837c631de 100644 --- a/src/settings/modules/GurobiSettings.cpp +++ b/src/settings/modules/GurobiSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" - +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { namespace modules { @@ -46,7 +46,7 @@ namespace storm { bool GurobiSettings::check() const { if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) { - STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::Gurobi, "Gurobi is not selected as the used LP solver, so setting options for Gurobi has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::solver::LpSolverType::Gurobi, "Gurobi is not selected as the preferred LP solver, so setting options for Gurobi might have no effect."); } return true; diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp index 5584308c5..fb61ddf16 100644 --- a/src/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/settings/modules/NativeEquationSolverSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" - +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -80,7 +80,7 @@ namespace storm { bool NativeEquationSolverSettings::check() const { bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Native || !optionSet, "Native is not selected as the equation solver, so setting options for native has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::solver::EquationSolverType::Native || !optionSet, "Native is not selected as the preferred equation solver, so setting options for native might have no effect."); return true; } diff --git a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp index 1be47979a..a1a00e283 100644 --- a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp +++ b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp @@ -7,6 +7,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -54,7 +55,7 @@ namespace storm { bool TopologicalValueIterationEquationSolverSettings::check() const { bool optionsSet = isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); + //STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); return true; } diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index a92130b7e..b4357b6d4 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -14,27 +14,24 @@ namespace storm { namespace solver { template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), stormMatrix(A), rowGroupIndices(A.getRowGroupIndices()) { - // Get the settings object to customize solving. - storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings(); - storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::generalSettings(); - - // Get appropriate settings. - precision = settings.getPrecision(); - relative = settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative; - maximalNumberOfIterations = settings.getMaximalIterationCount(); - useValueIteration = (generalSettings.getMinMaxEquationSolvingTechnique() == storm::settings::modules::GeneralSettings::MinMaxTechnique::ValueIteration); + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : + MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), \ + storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative,\ + storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique), + gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + + } template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), stormMatrix(A), rowGroupIndices(A.getRowGroupIndices()), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations), useValueIteration(useValueIteration) { + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackPolicy, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { // Intentionally left empty. } template void GmmxxMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { - if (useValueIteration) { + if (this->useValueIteration) { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { @@ -56,18 +53,14 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult); gmm::add(b, *multiplyResult); // Reduce the vector x by applying min/max over all nondeterministic choices. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, rowGroupIndices); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, rowGroupIndices); - } - + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, rowGroupIndices); + // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative); @@ -99,7 +92,7 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - std::vector::index_type> choiceVector(rowGroupIndices.size() - 1); + this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(rowGroupIndices.size() - 1); @@ -126,13 +119,13 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = stormMatrix.selectRowsFromRowGroups(choiceVector, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); - GmmxxLinearEquationSolver gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, precision, maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None, relative, 50); - storm::utility::vector::selectVectorValues(subB, choiceVector, rowGroupIndices, b); + GmmxxLinearEquationSolver gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None, this->relative, 50); + storm::utility::vector::selectVectorValues(subB, this->policy, rowGroupIndices, b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -146,11 +139,8 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, rowGroupIndices, &choiceVector); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, rowGroupIndices, &choiceVector); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, rowGroupIndices, &(this->policy)); + // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); @@ -199,11 +189,8 @@ namespace storm { gmm::add(*b, *multiplyResult); } - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, x, rowGroupIndices); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, x, rowGroupIndices); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, x, rowGroupIndices); + } if (!multiplyResultMemoryProvided) { diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.h b/src/solver/GmmxxMinMaxLinearEquationSolver.h index 4d151d706..b34f761cb 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.h +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.h @@ -20,7 +20,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -31,7 +31,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative = true); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy = false); virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; @@ -41,23 +41,9 @@ namespace storm { // The (gmm++) matrix associated with this equation solver. std::unique_ptr> gmmxxMatrix; - // A reference to the original sparse matrix. - storm::storage::SparseMatrix const& stormMatrix; - // A reference to the row group indices of the original matrix. std::vector const& rowGroupIndices; - // The required precision for the iterative methods. - double precision; - - // Sets whether the relative or absolute error is to be considered for convergence detection. - bool relative; - - // The maximal number of iterations to do before iteration is aborted. - uint_fast64_t maximalNumberOfIterations; - - // Whether value iteration or policy iteration is to be used. - bool useValueIteration; }; } // namespace solver } // namespace storm diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 2aad22bda..680ee7ee0 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -1,6 +1,9 @@ #include "MinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" #include namespace storm { @@ -15,5 +18,10 @@ namespace storm { useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration); } } + + std::vector AbstractMinMaxLinearEquationSolver::getPolicy() const { + STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!"); + return policy; + } } } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index e9679a6b4..6e6887cd8 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -2,7 +2,9 @@ #define STORM_SOLVER_MINMAXLINEAREQUATIONSOLVER_H_ #include - +#include +#include "SolverSelectionOptions.h" +#include "src/storage/sparse/StateType.h" namespace storm { namespace storage { @@ -10,6 +12,38 @@ namespace storm { } namespace solver { + /** + * Abstract base class which provides value-type independent helpers. + */ + class AbstractMinMaxLinearEquationSolver { + + public: + void setPolicyTracking(bool setToTrue=true); + + std::vector getPolicy() const; + + protected: + AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech); + + + /// The required precision for the iterative methods. + double precision; + + /// Sets whether the relative or absolute error is to be considered for convergence detection. + bool relative; + + /// The maximal number of iterations to do before iteration is aborted. + uint_fast64_t maximalNumberOfIterations; + + /// Whether value iteration or policy iteration is to be used. + bool useValueIteration; + + /// Whether we track the policy we generate. + bool trackPolicy; + + /// + mutable std::vector policy; + }; /*! * A interface that represents an abstract nondeterministic linear equation solver. In addition to solving @@ -17,7 +51,14 @@ namespace storm { * provided. */ template - class MinMaxLinearEquationSolver { + class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { + protected: + MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : + AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), + A(matrix) { + // Intentionally left empty. + } + public: virtual ~MinMaxLinearEquationSolver() { @@ -59,6 +100,9 @@ namespace storm { * @return The result of the repeated matrix-vector multiplication as the content of the vector x. */ virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + + protected: + storm::storage::SparseMatrix const& A; }; } // namespace solver diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 22eb207ad..87ee3b043 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -14,30 +14,29 @@ namespace storm { namespace solver { template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : A(A) { - // Get the settings object to customize solving. - storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::generalSettings(); - - // Get appropriate settings. - precision = settings.getPrecision(); - relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; - maximalNumberOfIterations = settings.getMaximalIterationCount(); - useValueIteration = (generalSettings.getMinMaxEquationSolvingTechnique() == storm::settings::modules::GeneralSettings::MinMaxTechnique::ValueIteration); + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : + MinMaxLinearEquationSolver(A, storm::settings::nativeEquationSolverSettings().getPrecision(), \ + storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, \ + storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique) + { + // Intentionally left empty. } template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative) : A(A), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations), useValueIteration(useValueIteration) { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : + MinMaxLinearEquationSolver(A, precision, \ + relative, \ + maximalNumberOfIterations, trackPolicy, tech) { // Intentionally left empty. } template void NativeMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { - if (useValueIteration) { + if (this->useValueIteration) { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { - multiplyResult = new std::vector(A.getRowCount()); + multiplyResult = new std::vector(this->A.getRowCount()); multiplyResultMemoryProvided = false; } std::vector* currentX = &x; @@ -54,21 +53,17 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the // user-specified maximum number of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Compute x' = A*x + b. - A.multiplyWithVector(*currentX, *multiplyResult); + this->A.multiplyWithVector(*currentX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, A.getRowGroupIndices()); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, A.getRowGroupIndices()); - } - + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, this->A.getRowGroupIndices()); + // Determine whether the method converged. - converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(precision), relative); + converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); // Update environment variables. std::swap(currentX, newX); @@ -98,11 +93,11 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - std::vector::index_type> choiceVector(A.getRowGroupIndices().size() - 1); + this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. - std::vector deterministicMultiplyResult(A.getRowGroupIndices().size() - 1); - std::vector subB(A.getRowGroupIndices().size() - 1); + std::vector deterministicMultiplyResult(this->A.getRowGroupIndices().size() - 1); + std::vector subB(this->A.getRowGroupIndices().size() - 1); // Check whether intermediate storage was provided and create it otherwise. bool multiplyResultMemoryProvided = true; @@ -126,13 +121,13 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = A.selectRowsFromRowGroups(choiceVector, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); NativeLinearEquationSolver nativeLinearEquationSolver(submatrix); - storm::utility::vector::selectVectorValues(subB, choiceVector, A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(subB, this->policy, this->A.getRowGroupIndices(), b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -141,16 +136,13 @@ namespace storm { nativeLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult); // Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration. - A.multiplyWithVector(*newX, *multiplyResult); + this->A.multiplyWithVector(*newX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, A.getRowGroupIndices(), &choiceVector); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, A.getRowGroupIndices(), &choiceVector); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(this->policy)); + // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); @@ -166,6 +158,7 @@ namespace storm { } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } + // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. @@ -189,13 +182,13 @@ namespace storm { // If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { - multiplyResult = new std::vector(A.getRowCount()); + multiplyResult = new std::vector(this->A.getRowCount()); multiplyResultMemoryProvided = false; } // Now perform matrix-vector multiplication as long as we meet the bound of the formula. for (uint_fast64_t i = 0; i < n; ++i) { - A.multiplyWithVector(x, *multiplyResult); + this->A.multiplyWithVector(x, *multiplyResult); // Add b if it is non-null. if (b != nullptr) { @@ -204,11 +197,8 @@ namespace storm { // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, x, A.getRowGroupIndices()); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, x, A.getRowGroupIndices()); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, x, this->A.getRowGroupIndices()); + } if (!multiplyResultMemoryProvided) { diff --git a/src/solver/NativeMinMaxLinearEquationSolver.h b/src/solver/NativeMinMaxLinearEquationSolver.h index c3fa66b35..5e297096a 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.h +++ b/src/solver/NativeMinMaxLinearEquationSolver.h @@ -19,7 +19,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -30,27 +30,12 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative = true); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative = true, bool trackPolicy = false); virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; - protected: - // A reference to the matrix the gives the coefficients of the linear equation system. - storm::storage::SparseMatrix const& A; - - // The required precision for the iterative methods. - double precision; - - // Sets whether the relative or absolute error is to be considered for convergence detection. - bool relative; - - // The maximal number of iterations to do before iteration is aborted. - uint_fast64_t maximalNumberOfIterations; - - // Whether value iteration or policy iteration is to be used. - bool useValueIteration; }; } // namespace solver } // namespace storm diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index d3d122e12..d31a02d3e 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -27,19 +27,12 @@ namespace storm { namespace solver { template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : NativeMinMaxLinearEquationSolver(A) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : + NativeMinMaxLinearEquationSolver(A, storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision(), \ + storm::settings::topologicalValueIterationEquationSolverSettings().getMaximalIterationCount(), MinMaxTechniqueSelection::ValueIteration, \ + storm::settings::topologicalValueIterationEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative) + { // Get the settings object to customize solving. - - //storm::settings::Settings* settings = storm::settings::Settings::getInstance(); - auto settings = storm::settings::topologicalValueIterationEquationSolverSettings(); - // Get appropriate settings. - //this->maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger(); - //this->precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); - //this->relative = !settings->isSet("absolute"); - this->maximalNumberOfIterations = settings.getMaximalIterationCount(); - this->precision = settings.getPrecision(); - this->relative = (settings.getConvergenceCriterion() == storm::settings::modules::TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative); - auto generalSettings = storm::settings::generalSettings(); this->enableCuda = generalSettings.isCudaSet(); #ifdef STORM_HAVE_CUDA @@ -48,7 +41,7 @@ namespace storm { } template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeMinMaxLinearEquationSolver(A, precision, maximalNumberOfIterations, relative) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeMinMaxLinearEquationSolver(A, precision, maximalNumberOfIterations, MinMaxTechniqueSelection::ValueIteration ,relative) { // Intentionally left empty. } diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.h b/src/solver/TopologicalMinMaxLinearEquationSolver.h index 4f748672c..be1b844bd 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.h @@ -30,7 +30,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -41,7 +41,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; private: diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 53277ec2d..2c9b2fbe8 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1065,6 +1065,17 @@ namespace storm { return sum; } + template + bool SparseMatrix::isProbabilistic() const { + storm::utility::ConstantsComparator comp; + for(index_type row = 0; row < this->rowCount; ++row) { + if(!comp.isOne(getRowSum(row))) { + return false; + } + } + return true; + } + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { // Check for matching sizes. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 1dd16b3de..71fe4078e 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -33,6 +33,9 @@ namespace storm { // Forward declare matrix class. template class SparseMatrix; + typedef uint_fast64_t SparseMatrixIndexType; + + template class MatrixEntry { public: @@ -128,7 +131,7 @@ namespace storm { template class SparseMatrixBuilder { public: - typedef uint_fast64_t index_type; + typedef SparseMatrixIndexType index_type; typedef ValueType value_type; /*! @@ -300,7 +303,7 @@ namespace storm { friend class storm::solver::TopologicalValueIterationMinMaxLinearEquationSolver; friend class SparseMatrixBuilder; - typedef uint_fast64_t index_type; + typedef SparseMatrixIndexType index_type; typedef ValueType value_type; typedef typename std::vector>::iterator iterator; typedef typename std::vector>::const_iterator const_iterator; @@ -738,6 +741,10 @@ namespace storm { */ value_type getRowSum(index_type row) const; + /*! + * Checks for each row whether it sums to one. + */ + bool isProbabilistic() const; /*! * Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix * of B if B has no entries in position where A has none. Additionally, the matrices must be of equal size. @@ -942,6 +949,7 @@ namespace storm { // A vector indicating the row groups of the matrix. std::vector rowGroupIndices; + }; } // namespace storage diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index b58e74cb5..507a72ba3 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -24,6 +24,8 @@ namespace storm { namespace utility { namespace solver { + + template std::unique_ptr> SymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { return std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs)); @@ -36,10 +38,10 @@ namespace storm { template std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver(); switch (equationSolver) { - case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); - case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Native: return std::unique_ptr>(new storm::solver::NativeLinearEquationSolver(matrix)); default: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); } } @@ -75,10 +77,10 @@ namespace storm { template std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver(); switch (equationSolver) { - case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); - case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); default: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); } } @@ -99,10 +101,10 @@ namespace storm { } std::unique_ptr LpSolverFactory::create(std::string const& name) const { - storm::settings::modules::GeneralSettings::LpSolver lpSolver = storm::settings::generalSettings().getLpSolver(); + storm::solver::LpSolverType lpSolver = storm::settings::generalSettings().getLpSolver(); switch (lpSolver) { - case storm::settings::modules::GeneralSettings::LpSolver::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); - case storm::settings::modules::GeneralSettings::LpSolver::glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); + case storm::solver::LpSolverType::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); + case storm::solver::LpSolverType::Glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); default: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); } } diff --git a/src/utility/solver.h b/src/utility/solver.h index 661bd90ba..66abbd957 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -3,6 +3,7 @@ #include "src/solver/NativeLinearEquationSolver.h" #include "src/storage/dd/DdType.h" +#include "src/utility/ExtendSettingEnumWithSelectionField.h" namespace storm { namespace solver { @@ -22,6 +23,7 @@ namespace storm { namespace utility { namespace solver { + template class SymbolicLinearEquationSolverFactory { public: diff --git a/src/utility/vector.h b/src/utility/vector.h index 634d2bc5a..723550e51 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -333,7 +333,7 @@ namespace storm { } #endif } - + /*! * Reduces the given source vector by selecting the smallest element out of each row group. * @@ -360,6 +360,24 @@ namespace storm { reduceVector(source, target, rowGrouping, std::greater(), choices); } + /*! + * Reduces the given source vector by selecting either the smallest or the largest out of each row group. + * + * @param minimize If true, select the smallest, else select the largest. + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. + * @param choices If non-null, this vector is used to store the choices made during the selection. + */ + template + void reduceVectorMinOrMax(bool minimize, std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { + if(minimize) { + reduceVectorMin(source, target, rowGrouping, choices); + } else { + reduceVectorMax(source, target, rowGrouping, choices); + } + } + /*! * Compares the given elements and determines whether they are equal modulo the given precision. The provided flag * additionaly specifies whether the error is computed in relative or absolute terms. diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index 5b4174e51..6c659e7b7 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -78,7 +78,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector b = { 0.099, 0.5 }; storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings(); - storm::solver::GmmxxMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), false, settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative); + storm::solver::GmmxxMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), storm::solver::MinMaxTechniqueSelection::PolicyIteration, settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative); ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); diff --git a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp index bb7c281c9..b83423ffe 100644 --- a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -79,7 +79,7 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector b = { 0.099, 0.5 }; storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - storm::solver::NativeMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), false, settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative); + storm::solver::NativeMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), storm::solver::MinMaxTechniqueSelection::PolicyIteration, settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative); ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision()); From d4ba7905fa337b9912de5251bd32cbb96a714e05 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 24 Aug 2015 18:25:47 +0200 Subject: [PATCH 7/9] Extra constructor for simple testing. Former-commit-id: 0fcef3d5e71bd7e4d5784c060630952b42b3ba51 --- src/storage/BitVector.cpp | 5 +++++ src/storage/BitVector.h | 5 +++++ test/functional/storage/BitVectorTest.cpp | 15 +++++++++++++++ 3 files changed, 25 insertions(+) diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 9835c54dc..3e1e9bb5b 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -78,6 +78,11 @@ namespace storm { set(begin, end); } + BitVector::BitVector(uint_fast64_t length, std::vector setEntries) : BitVector(length, setEntries.begin(), setEntries.end()) + { + // Intentionally left empty. + } + BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount), bucketVector(bucketCount) { STORM_LOG_ASSERT((bucketCount << 6) == bitCount, "Bit count does not match number of buckets."); } diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index ec4cce693..4c5e64352 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -118,6 +118,11 @@ namespace storm { template BitVector(uint_fast64_t length, InputIterator first, InputIterator last); + /*! + * Creates a bit vector that has exactly the bits set that are given by the vector + */ + BitVector(uint_fast64_t length, std::vector setEntries); + /*! * Performs a deep copy of the given bit vector. * diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index 88715dff7..3dc139fa7 100644 --- a/test/functional/storage/BitVectorTest.cpp +++ b/test/functional/storage/BitVectorTest.cpp @@ -39,6 +39,21 @@ TEST(BitVectorTest, InitFromIterator) { } } +TEST(BitVectorTest, InitFromIntVector) { + std::vector valueVector = {0, 4, 10}; + storm::storage::BitVector vector(32, valueVector); + + ASSERT_EQ(32ul, vector.size()); + + for (uint_fast64_t i = 0; i < 32; ++i) { + if (i == 0 || i == 4 || i == 10) { + ASSERT_TRUE(vector.get(i)); + } else { + ASSERT_FALSE(vector.get(i)); + } + } +} + TEST(BitVectorTest, GetSet) { storm::storage::BitVector vector(32); From da120d9de5a7548f4dae7db620453a4681676aa8 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 24 Aug 2015 18:26:23 +0200 Subject: [PATCH 8/9] Refactored some stuff in constants... Former-commit-id: 3ac9216f73c3e0554ab0ee8de459b6bdf5f4ffe6 --- src/utility/constants.cpp | 112 +++++++++++++++++++------------------- src/utility/constants.h | 10 ++++ 2 files changed, 65 insertions(+), 57 deletions(-) diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 5b5a68348..64f522539 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -25,7 +25,52 @@ namespace storm { return std::numeric_limits::infinity(); } + template + bool isOne(ValueType const& a) { + return a == one(); + } + + template + bool isZero(ValueType const& a) { + return a == zero(); + } + + template + bool isConstant(ValueType const& a) { + return true; + } + #ifdef STORM_HAVE_CARL + template<> + bool isOne(storm::RationalFunction const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::RationalFunction const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::RationalFunction const& a) { + return a.isConstant(); + } + + template<> + bool isOne(storm::Polynomial const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::Polynomial const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::Polynomial const& a) { + return a.isConstant(); + } + template<> storm::RationalFunction infinity() { // FIXME: this does not work. @@ -110,40 +155,17 @@ namespace storm { template<> RationalFunction&& simplify(RationalFunction&& value); - template<> - class ConstantsComparator { - public: - bool isOne(storm::RationalFunction const& value) const; - - bool isZero(storm::RationalFunction const& value) const; - - bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; - - bool isConstant(storm::RationalFunction const& value) const; - }; - - template<> - class ConstantsComparator { - public: - bool isOne(storm::Polynomial const& value) const; - - bool isZero(storm::Polynomial const& value) const; - - bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; - - bool isConstant(storm::Polynomial const& value) const; - }; #endif template bool ConstantsComparator::isOne(ValueType const& value) const { - return value == one(); + return isOne(value); } template bool ConstantsComparator::isZero(ValueType const& value) const { - return value == zero(); + return isZero(value); } template @@ -151,6 +173,12 @@ namespace storm { return value1 == value2; } + template + bool ConstantsComparator::isConstant(T const& value) const { + return isConstant(value); + } + + ConstantsComparator::ConstantsComparator() : precision(static_cast(storm::settings::generalSettings().getPrecision())) { // Intentionally left empty. } @@ -226,40 +254,9 @@ namespace storm { value.simplify(); return std::move(value); } +#endif - bool ConstantsComparator::isOne(storm::RationalFunction const& value) const { - return value.isOne(); - } - - bool ConstantsComparator::isZero(storm::RationalFunction const& value) const { - return value.isZero(); - } - bool ConstantsComparator::isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const { - return value1 == value2; - } - - bool ConstantsComparator::isConstant(storm::RationalFunction const& value) const { - return value.isConstant(); - } - - bool ConstantsComparator::isOne(storm::Polynomial const& value) const { - return value.isOne(); - } - - bool ConstantsComparator::isZero(storm::Polynomial const& value) const { - return value.isZero(); - } - - bool ConstantsComparator::isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const { - return value1 == value2; - } - - bool ConstantsComparator::isConstant(storm::Polynomial const& value) const { - return value.isConstant(); - } -#endif - template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { simplify(matrixEntry.getValue()); @@ -327,6 +324,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class ConstantsComparator; template class ConstantsComparator; + template class ConstantsComparator; template RationalFunction one(); template RationalFunction zero(); diff --git a/src/utility/constants.h b/src/utility/constants.h index 2e5206711..cae1a7a5d 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -30,6 +30,16 @@ namespace storm { template ValueType infinity(); + + template + bool isOne(ValueType const& a); + + template + bool isZero(ValueType const& a); + + template + bool isConstant(ValueType const& a); + template From 707a4f500b0585992ca8fb2a2ce00ebdf4e33474 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 24 Aug 2015 18:26:41 +0200 Subject: [PATCH 9/9] vector sum_if Former-commit-id: 67b2ef9ff6ddffff772624973505dd2494812da2 --- src/utility/vector.h | 16 ++++++++++++++++ test/functional/utility/VectorTest.cpp | 14 ++++++++++++++ 2 files changed, 30 insertions(+) create mode 100644 test/functional/utility/VectorTest.cpp diff --git a/src/utility/vector.h b/src/utility/vector.h index 723550e51..45348dd11 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -249,6 +249,22 @@ namespace storm { return filter(values, fnc); } + /** + * Sum the entries from values that are set to one in the filter vector. + * @param values + * @param filter + * @return The sum of the values with a corresponding one in the filter. + */ + template + VT sum_if(std::vector const& values, storm::storage::BitVector const& filter) { + assert(values.size() >= filter.size()); + VT sum = storm::utility::zero(); + for(uint_fast64_t i : filter) { + sum += values[i]; + } + return sum; + } + /*! * Reduces the given source vector by selecting an element according to the given filter out of each row group. * diff --git a/test/functional/utility/VectorTest.cpp b/test/functional/utility/VectorTest.cpp new file mode 100644 index 000000000..33f3c5cfe --- /dev/null +++ b/test/functional/utility/VectorTest.cpp @@ -0,0 +1,14 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/storage/BitVector.h" +#include "src/utility/vector.h" + +TEST(VectorTest, sum_if) { + std::vector a = {1.0, 2.0, 4.0, 8.0, 16.0}; + storm::storage::BitVector f1(5, {2,4}); + storm::storage::BitVector f2(5, {3,4}); + + ASSERT_EQ(20.0, storm::utility::vector::sum_if(a, f1)); + ASSERT_EQ(24.0, storm::utility::vector::sum_if(a, f2)); + +}