Save memory when bounded checking sparse DTMC

SparseDeterministicStepBoundedHorizonHelper takes a matrix with the backwards transitions. By constructing this inside the helper we can deallocate it early, reducing peak memory.
moves-rwth · Apr 5, 2024 · b26d9af · b26d9af
1 parent 5c89b2d
commit b26d9af
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 5 deletions.
diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp
@@ -27,7 +27,6 @@ SparseDeterministicStepBoundedHorizonHelper<ValueType>::SparseDeterministicStepB
 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) {
@@ -40,6 +39,7 @@ std::vector<ValueType> SparseDeterministicStepBoundedHorizonHelper<ValueType>::c
     if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
         maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
     } else {
+        auto backwardTransitions = transitionMatrix.transpose(true);
         maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, upperBound);
         if (lowerBound == 0) {
             maybeStates &= ~psiStates;

diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h
@@ -15,8 +15,7 @@ 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::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& phiStates,
                                    storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound,
                                    ModelCheckerHint const& hint = ModelCheckerHint());
 

diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -101,8 +101,8 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c
         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());
+                           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;
     }