added checking requirements of MinMax solvers to model checker helpers

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

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

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

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.

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;

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

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

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

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>

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

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.

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