mdp support for lower step bounds

src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp

@@ -0,0 +1,86 @@
+#include "storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h"
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
+#include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h"
+
+#include "storm/models/sparse/StandardRewardModel.h"
+
+#include "storm/utility/macros.h"
+#include "storm/utility/vector.h"
+#include "storm/utility/graph.h"
+
+#include "storm/storage/expressions/Expression.h"
+#include "storm/solver/Multiplier.h"
+#include "storm/utility/SignalHandler.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+
+            template<typename ValueType>
+            SparseNondeterministicStepBoundedHorizonHelper<ValueType>::SparseNondeterministicStepBoundedHorizonHelper(/*storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions*/)
+            //transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions)
+            {
+                // Intentionally left empty.
+            }
+
+            template<typename ValueType>
+            std::vector<ValueType> SparseNondeterministicStepBoundedHorizonHelper<ValueType>::compute(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates,   uint64_t lowerBound, uint64_t upperBound,  ModelCheckerHint const& hint)
+            {
+                std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                storm::storage::BitVector makeZeroColumns;
+
+
+                // Determine the states that have 0 probability of reaching the target states.
+                storm::storage::BitVector maybeStates;
+                if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
+                    maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
+                } else {
+                    if (goal.minimize()) {
+                        maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, upperBound);
+                    } else {
+                        maybeStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, upperBound);
+                    }
+                    if (lowerBound == 0) {
+                        maybeStates &= ~psiStates;
+                    } else {
+                        makeZeroColumns = psiStates;
+                    }
+
+                }
+
+                STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0.");
+
+                if (!maybeStates.empty()) {
+                    // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
+                    storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false, makeZeroColumns);
+                    std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, psiStates);
+
+                    // Create the vector with which to multiply.
+                    std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits());
+
+                    auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
+                    if (lowerBound == 0) {
+                        multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound);
+                    } else {
+                        multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1);
+                        storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
+                        auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
+                        b = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
+                        multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, lowerBound - 1);
+                    }
+                    // Set the values of the resulting vector accordingly.
+                    storm::utility::vector::setVectorValues(result, maybeStates, subresult);
+                }
+                if (lowerBound == 0) {
+                    storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
+                }
+                return result;
+            }
+
+
+            template class SparseNondeterministicStepBoundedHorizonHelper<double>;
+            template class SparseNondeterministicStepBoundedHorizonHelper<storm::RationalNumber>;
+        }
+    }
+}

src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h

@@ -0,0 +1,25 @@
+#pragma once
+
+
+#include "storm/modelchecker/hints/ModelCheckerHint.h"
+#include "storm/modelchecker/prctl/helper/SolutionType.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/utility/solver.h"
+#include "storm/solver/SolveGoal.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+
+            template<typename ValueType>
+            class SparseNondeterministicStepBoundedHorizonHelper {
+            public:
+                SparseNondeterministicStepBoundedHorizonHelper();
+                std::vector<ValueType> compute(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions,  storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound, ModelCheckerHint const& hint = ModelCheckerHint());
+            private:
+            };
+
+
+        }
+    }
+}

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -71,8 +71,9 @@ namespace storm {
                 auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeRewardBoundedValues(env, this->getModel(), formula);
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             } else {
-                STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete lower time bound.");
-                STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
+                STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
+                STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral.");
+                STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper step bound.");
                 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
                 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
                 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -16,6 +16,7 @@
 
 #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
 #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h"
+#include "storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h"
 #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h"
 
 #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h"
@@ -83,13 +84,15 @@ namespace storm {
                 auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             } else {
-                STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper time bound, and no lower bound.");
+                STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
+                STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral.");
                 STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
                 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
                 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
                 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
                 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
-                std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeStepBoundedUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint());
+                storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper<ValueType> helper;
+                std::vector<ValueType> numericResult = helper.compute(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint());
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             }
         }

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -52,45 +52,7 @@ namespace storm {
     namespace modelchecker {
         namespace helper {
 
-            template<typename ValueType>
-            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeStepBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, ModelCheckerHint const& hint) {
-                std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
-                
-                // Determine the states that have 0 probability of reaching the target states.
-                storm::storage::BitVector maybeStates;
-                if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
-                    maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
-                } else {
-                    if (goal.minimize()) {
-                        maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound);
-                    } else {
-                        maybeStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, stepBound);
-                    }
-                    maybeStates &= ~psiStates;
-                }
-                
-                STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0.");
-                
-                if (!maybeStates.empty()) {
-                    // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-                    storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
-                    std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, psiStates);
-                    
-                    // Create the vector with which to multiply.
-                    std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits());
-                    
-                    auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
-                    multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound);
-                    
-                    // Set the values of the resulting vector accordingly.
-                    storm::utility::vector::setVectorValues(result, maybeStates, subresult);
-                }
-                storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
-                
-                return result;
-            }
-
-
+            
             template<typename ValueType>
             std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(Environment const& env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates) {
                 storm::utility::Stopwatch swAll(true), swBuild, swCheck;

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -38,8 +38,6 @@ namespace storm {
             template <typename ValueType>
             class SparseMdpPrctlHelper {
             public:
-                
-                static std::vector<ValueType> computeStepBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, ModelCheckerHint const& hint = ModelCheckerHint());
 
                 static std::map<storm::storage::sparse::state_type, ValueType> computeRewardBoundedValues(Environment const& env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates);