From 4adee85fa5e47775b04e2382edd0c299d7a19a57 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 30 Aug 2017 20:59:20 +0200
Subject: [PATCH] added checking requirements of MinMax solvers to model
checker helpers
---
.../3rdparty/sylvan/src/storm_wrapper.cpp | 2 --
.../UncheckedRequirementException.h | 12 +++++++++++
.../helper/SparseMarkovAutomatonCslHelper.cpp | 21 +++++++++++++++++--
.../prctl/helper/HybridMdpPrctlHelper.cpp | 15 +++++++++++++
.../prctl/helper/SparseMdpPrctlHelper.cpp | 12 +++++++++++
.../IterativeMinMaxLinearEquationSolver.cpp | 1 +
.../solver/LpMinMaxLinearEquationSolver.cpp | 1 +
.../solver/MinMaxLinearEquationSolver.cpp | 17 +++++++++++++--
src/storm/solver/MinMaxLinearEquationSolver.h | 11 ++++++----
.../StandardMinMaxLinearEquationSolver.cpp | 1 +
src/storm/utility/macros.h | 8 ++++++-
.../parser/SparseItemLabelingParserTest.cpp | 6 +++---
12 files changed, 93 insertions(+), 14 deletions(-)
create mode 100644 src/storm/exceptions/UncheckedRequirementException.h
diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
index 09fb51ccf..fb92720d0 100644
--- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp
+++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
@@ -125,8 +125,6 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) {
std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif
- std::cout << "got ptr for eq check " << a << std::endl;
-
return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0;
}
diff --git a/src/storm/exceptions/UncheckedRequirementException.h b/src/storm/exceptions/UncheckedRequirementException.h
new file mode 100644
index 000000000..f902c6ee5
--- /dev/null
+++ b/src/storm/exceptions/UncheckedRequirementException.h
@@ -0,0 +1,12 @@
+#pragma once
+
+#include "storm/exceptions/BaseException.h"
+#include "storm/exceptions/ExceptionMacros.h"
+
+namespace storm {
+ namespace exceptions {
+
+ STORM_NEW_EXCEPTION(UncheckedRequirementException)
+
+ } // namespace exceptions
+} // namespace storm
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index 3aaeec73d..a7d28ecac 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -27,6 +27,7 @@
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm {
namespace modelchecker {
@@ -86,8 +87,13 @@ namespace storm {
}
}
}
-
+
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic);
+ solver->setRequirementsChecked();
solver->setCachingEnabled(true);
// Perform the actual value iteration
@@ -368,7 +374,13 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates);
std::vector<ValueType> x(numberOfSspStates);
+
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix);
+ solver->setRequirementsChecked();
solver->solveEquations(dir, x, b);
// Prepare result vector.
@@ -570,11 +582,16 @@ namespace storm {
std::vector<ValueType> w = v;
std::vector<ValueType> x(aProbabilistic.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> b = probabilisticChoiceRewards;
+
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic));
+ solver->setRequirementsChecked(true);
solver->setCachingEnabled(true);
while (true) {
-
// Compute the expected total rewards for the probabilistic states
solver->solveEquations(dir, x, b);
diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
index b0363cd4e..6a6a15dd7 100644
--- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
@@ -19,6 +19,7 @@
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm {
namespace modelchecker {
@@ -77,7 +78,12 @@ namespace storm {
// Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = linearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first));
+ solver->setRequirementsChecked();
solver->solveEquations(dir, x, explicitRepresentation.second);
// Return a hybrid check result that stores the numerical values explicitly.
@@ -141,6 +147,10 @@ namespace storm {
// Translate the symbolic matrix/vector to their explicit representations.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = linearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first));
solver->repeatedMultiply(dir, x, &explicitRepresentation.second, stepBound);
@@ -267,8 +277,13 @@ namespace storm {
// Translate the symbolic matrix/vector to their explicit representations.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = linearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first));
+ solver->setRequirementsChecked();
solver->solveEquations(dir, x, explicitRepresentation.second);
// Return a hybrid check result that stores the numerical values explicitly.
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 93c1674b0..1e6cfb882 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -29,6 +29,7 @@
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/IllegalFunctionCallException.h"
#include "storm/exceptions/IllegalArgumentException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm {
namespace modelchecker {
@@ -253,8 +254,13 @@ namespace storm {
template<typename ValueType>
std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> SparseMdpPrctlHelper<ValueType>::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>>&& hintValues, boost::optional<std::vector<uint_fast64_t>>&& hintChoices, boost::optional<ValueType> const& lowerResultBound, boost::optional<ValueType> const& upperResultBound) {
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
// Set up the solver
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix);
+ solver->setRequirementsChecked();
if (lowerResultBound) {
solver->setLowerBound(lowerResultBound.get());
}
@@ -651,8 +657,13 @@ namespace storm {
// Finalize the matrix and solve the corresponding system of equations.
storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates);
+ // Check for requirements of the solver.
+ std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements();
+ STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
+
std::vector<ValueType> sspResult(numberOfSspStates);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(std::move(sspMatrix));
+ solver->setRequirementsChecked();
solver->solveEquations(dir, sspResult, b);
// Prepare result vector.
@@ -764,6 +775,7 @@ namespace storm {
ValueType precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>().getPrecision());
std::vector<ValueType> x(mecTransitions.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> xPrime = x;
+
auto solver = minMaxLinearEquationSolverFactory.create(std::move(mecTransitions));
solver->setCachingEnabled(true);
ValueType maxDiff, minDiff;
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index de02a1c79..671e35345 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -469,6 +469,7 @@ namespace storm {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone(), settings);
result->setTrackScheduler(this->isTrackSchedulerSet());
+ result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;
}
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
index 5df72fe28..2f360f513 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
@@ -130,6 +130,7 @@ namespace storm {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone());
result->setTrackScheduler(this->isTrackSchedulerSet());
+ result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;
}
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp
index f1a7b1e3c..011249ec6 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp
@@ -30,6 +30,7 @@ namespace storm {
template<typename ValueType>
bool MinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+ STORM_LOG_WARN_COND_DEBUG(this->isRequirementsCheckedSet(), "The requirements of the solver have not been marked as checked. Please provide the appropriate check or mark the requirements as checked (if applicable).");
return internalSolveEquations(d, x, b);
}
@@ -147,8 +148,8 @@ namespace storm {
}
template<typename ValueType>
- bool MinMaxLinearEquationSolver<ValueType>::getRequirementsChecked() const {
- return this->requirementsChecked;
+ bool MinMaxLinearEquationSolver<ValueType>::isRequirementsCheckedSet() const {
+ return requirementsChecked;
}
template<typename ValueType>
@@ -166,6 +167,16 @@ namespace storm {
return trackScheduler;
}
+ template<typename ValueType>
+ void MinMaxLinearEquationSolverFactory<ValueType>::setRequirementsChecked(bool value) {
+ this->requirementsChecked = value;
+ }
+
+ template<typename ValueType>
+ bool MinMaxLinearEquationSolverFactory<ValueType>::isRequirementsCheckedSet() const {
+ return this->requirementsChecked;
+ }
+
template<typename ValueType>
void MinMaxLinearEquationSolverFactory<ValueType>::setMinMaxMethod(MinMaxMethodSelection const& newMethod) {
if (newMethod == MinMaxMethodSelection::FROMSETTINGS) {
@@ -240,6 +251,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
result->setTrackScheduler(this->isTrackSchedulerSet());
+ result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;
}
@@ -257,6 +269,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
result->setTrackScheduler(this->isTrackSchedulerSet());
+ result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;
}
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h
index 0fe7d8fbe..992bd2cc5 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.h
+++ b/src/storm/solver/MinMaxLinearEquationSolver.h
@@ -181,7 +181,7 @@ namespace storm {
/*!
* Retrieves whether the solver is aware that the requirements were checked.
*/
- bool getRequirementsChecked() const;
+ bool isRequirementsCheckedSet() const;
protected:
virtual bool internalSolveEquations(OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const& b) const = 0;
@@ -217,8 +217,8 @@ namespace storm {
public:
MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
- virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
- virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const;
+ std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
+ std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create() const = 0;
void setTrackScheduler(bool value);
@@ -230,10 +230,13 @@ namespace storm {
MinMaxMethod const& getMinMaxMethod() const;
std::vector<MinMaxLinearEquationSolverRequirement> getRequirements() const;
-
+ void setRequirementsChecked(bool value = true);
+ bool isRequirementsCheckedSet() const;
+
private:
bool trackScheduler;
MinMaxMethod method;
+ bool requirementsChecked;
};
template<typename ValueType>
diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
index 0b3f41a03..4e2eabf03 100644
--- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
@@ -115,6 +115,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
result->setTrackScheduler(this->isTrackSchedulerSet());
+ result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;
}
diff --git a/src/storm/utility/macros.h b/src/storm/utility/macros.h
index 348f6677e..b4f3cb06a 100644
--- a/src/storm/utility/macros.h
+++ b/src/storm/utility/macros.h
@@ -15,9 +15,15 @@ do { \
assert(cond); \
} \
} while (false)
-
+#define STORM_LOG_WARN_COND_DEBUG(cond, message) \
+do { \
+ if (!(cond)) { \
+ STORM_LOG_WARN(message); \
+ } \
+} while (false)
#else
#define STORM_LOG_ASSERT(cond, message)
+#define STORM_LOG_WARN_COND_DEBUG(cond, message)
#endif
// Define STORM_LOG_THROW to always throw the exception with the given message if the condition fails to hold.
diff --git a/src/test/storm/parser/SparseItemLabelingParserTest.cpp b/src/test/storm/parser/SparseItemLabelingParserTest.cpp
index bca1c2201..695b6837b 100644
--- a/src/test/storm/parser/SparseItemLabelingParserTest.cpp
+++ b/src/test/storm/parser/SparseItemLabelingParserTest.cpp
@@ -81,18 +81,18 @@ TEST(SparseItemLabelingParserTest, BasicNondeterministicParsing) {
// Checking whether the parsed labeling is correct
ASSERT_TRUE(labeling.containsLabel("alpha"));
- EXPECT_EQ(2, labeling.getChoices("alpha").getNumberOfSetBits());
+ EXPECT_EQ(2ull, labeling.getChoices("alpha").getNumberOfSetBits());
EXPECT_TRUE(labeling.getChoiceHasLabel("alpha", 0));
EXPECT_TRUE(labeling.getChoiceHasLabel("alpha", 1));
ASSERT_TRUE(labeling.containsLabel("beta"));
- EXPECT_EQ(3, labeling.getChoices("beta").getNumberOfSetBits());
+ EXPECT_EQ(3ull, labeling.getChoices("beta").getNumberOfSetBits());
EXPECT_TRUE(labeling.getChoiceHasLabel("beta", 1));
EXPECT_TRUE(labeling.getChoiceHasLabel("beta", 3));
EXPECT_TRUE(labeling.getChoiceHasLabel("beta", 8));
ASSERT_TRUE(labeling.containsLabel("gamma"));
- EXPECT_EQ(1, labeling.getChoices("gamma").getNumberOfSetBits());
+ EXPECT_EQ(1ull, labeling.getChoices("gamma").getNumberOfSetBits());
EXPECT_TRUE(labeling.getChoiceHasLabel("gamma", 2));
ASSERT_TRUE(labeling.containsLabel("delta"));