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 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 requirements = minMaxLinearEquationSolverFactory.getRequirements(); + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); + solver->setRequirementsChecked(); solver->setCachingEnabled(true); // Perform the actual value iteration @@ -368,7 +374,13 @@ namespace storm { storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates); std::vector x(numberOfSspStates); + + // Check for requirements of the solver. + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); + solver->setRequirementsChecked(); solver->solveEquations(dir, x, b); // Prepare result vector. @@ -570,11 +582,16 @@ namespace storm { std::vector w = v; std::vector x(aProbabilistic.getRowGroupCount(), storm::utility::zero()); std::vector b = probabilisticChoiceRewards; + + // Check for requirements of the solver. + std::vector 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, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); + // Check for requirements of the solver. + std::vector requirements = linearEquationSolverFactory.getRequirements(); + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + std::unique_ptr> 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, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); + // Check for requirements of the solver. + std::vector requirements = linearEquationSolverFactory.getRequirements(); + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + std::unique_ptr> 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, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); + // Check for requirements of the solver. + std::vector 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> 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 std::pair, boost::optional>> SparseMdpPrctlHelper::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues, boost::optional>&& hintChoices, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { + // Check for requirements of the solver. + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + // Set up the solver std::unique_ptr> 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 sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates); + // Check for requirements of the solver. + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + std::vector sspResult(numberOfSspStates); std::unique_ptr> 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(storm::settings::getModule().getPrecision()); std::vector x(mecTransitions.getRowGroupCount(), storm::utility::zero()); std::vector 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> result = std::make_unique>(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> result = std::make_unique>(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 bool MinMaxLinearEquationSolver::solveEquations(OptimizationDirection d, std::vector& x, std::vector 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 - bool MinMaxLinearEquationSolver::getRequirementsChecked() const { - return this->requirementsChecked; + bool MinMaxLinearEquationSolver::isRequirementsCheckedSet() const { + return requirementsChecked; } template @@ -166,6 +167,16 @@ namespace storm { return trackScheduler; } + template + void MinMaxLinearEquationSolverFactory::setRequirementsChecked(bool value) { + this->requirementsChecked = value; + } + + template + bool MinMaxLinearEquationSolverFactory::isRequirementsCheckedSet() const { + return this->requirementsChecked; + } + template void MinMaxLinearEquationSolverFactory::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& x, std::vector const& b) const = 0; @@ -217,8 +217,8 @@ namespace storm { public: MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; - virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const; + std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const; + std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const; virtual std::unique_ptr> create() const = 0; void setTrackScheduler(bool value); @@ -230,10 +230,13 @@ namespace storm { MinMaxMethod const& getMinMaxMethod() const; std::vector getRequirements() const; - + void setRequirementsChecked(bool value = true); + bool isRequirementsCheckedSet() const; + private: bool trackScheduler; MinMaxMethod method; + bool requirementsChecked; }; template 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"));