step bounded properties for dtmcs in a new helper, and now with support for (extra) lower bounds

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

@@ -0,0 +1,94 @@
+#include "storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h"
+#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.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>
+            SparseDeterministicStepBoundedHorizonHelper<ValueType>::SparseDeterministicStepBoundedHorizonHelper()
+            {
+                // Intentionally left empty.
+            }
+
+            template<typename ValueType>
+            std::vector<ValueType> SparseDeterministicStepBoundedHorizonHelper<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.getRowCount(), storm::utility::zero<ValueType>());
+
+                // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
+                storm::storage::BitVector maybeStates;
+                storm::storage::BitVector makeZeroColumns;
+
+
+                if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
+                    maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
+                } else {
+                    maybeStates = storm::utility::graph::performProbGreater0(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 (lowerBound == 0) {
+                    storm::utility::vector::setVectorValues<ValueType>(result, psiStates,
+                                                                       storm::utility::one<ValueType>());
+                }
+
+                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, true, makeZeroColumns);
+
+                    // Create the vector of one-step probabilities to go to target states.
+                    std::vector<ValueType> b = transitionMatrix.getConstrainedRowSumVector(maybeStates, psiStates);
+
+                    // Create the vector with which to multiply.
+                    std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits());
+
+                    // Perform the matrix vector multiplication
+                    auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
+                    if (lowerBound == 0) {
+                        multiplier->repeatedMultiply(env, subresult, &b, upperBound);
+                    } else {
+                        multiplier->repeatedMultiply(env, subresult, &b, upperBound - lowerBound + 1);
+                        submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true);
+                        multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
+                        b = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
+                        multiplier->repeatedMultiply(env, subresult, &b, lowerBound - 1);
+                    }
+
+
+                    // Set the values of the resulting vector accordingly.
+                    storm::utility::vector::setVectorValues(result, maybeStates, subresult);
+                }
+
+                return result;
+            }
+
+
+            template class SparseDeterministicStepBoundedHorizonHelper<double>;
+            template class SparseDeterministicStepBoundedHorizonHelper<storm::RationalNumber>;
+            template class SparseDeterministicStepBoundedHorizonHelper<storm::RationalFunction>;
+        }
+    }
+}//
+// Created by Sebastian Junges on 8/20/20.
+//
+

src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.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 SparseDeterministicStepBoundedHorizonHelper {
+            public:
+                SparseDeterministicStepBoundedHorizonHelper();
+                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

@@ -1,4 +1,5 @@
 #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h"
 
 #include <vector>
 #include <memory>
@@ -70,13 +71,14 @@ 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.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper time bound, and no lower bound.");
+                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.");
                 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::SparseDtmcPrctlHelper<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::SparseDeterministicStepBoundedHorizonHelper<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());
                 std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
                 return result;
             }

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

@@ -43,44 +43,7 @@
 namespace storm {
     namespace modelchecker {
         namespace helper {
-            template<typename ValueType, typename RewardModelType>
-            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::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.getRowCount(), storm::utility::zero<ValueType>());
-                
-                // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
-                storm::storage::BitVector maybeStates;
-                
-                if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
-                    maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
-                } else {
-                    maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, stepBound);
-                    maybeStates &= ~psiStates;
-                }
-                
-                STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0.");
 
-                storm::utility::vector::setVectorValues<ValueType>(result, psiStates, storm::utility::one<ValueType>());
-                
-                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, true);
-                    
-                    // Create the vector of one-step probabilities to go to target states.
-                    std::vector<ValueType> b = transitionMatrix.getConstrainedRowSumVector(maybeStates, psiStates);
-                    
-                    // Create the vector with which to multiply.
-                    std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits());
-                    
-                    // Perform the matrix vector multiplication
-                    auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
-                    multiplier->repeatedMultiply(env, subresult, &b, stepBound);
-                    
-                    // Set the values of the resulting vector accordingly.
-                    storm::utility::vector::setVectorValues(result, maybeStates, subresult);
-                }
-                
-                return result;
-            }
             
             template<>
             std::map<storm::storage::sparse::state_type, storm::RationalFunction> SparseDtmcPrctlHelper<storm::RationalFunction>::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc<storm::RationalFunction> const& model, std::shared_ptr<storm::logic::OperatorFormula const> rewardBoundedFormula) {

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

@@ -28,8 +28,6 @@ namespace storm {
             class SparseDtmcPrctlHelper {
             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, storm::models::sparse::Dtmc<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> rewardBoundedFormula);
                 
                 static std::vector<ValueType> computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates);