From b26d9afa8c35a02d5d009f13bc3e912249cd4535 Mon Sep 17 00:00:00 2001
From: Quinten Kock <quinten@quinten.space>
Date: Sun, 3 Mar 2024 18:48:08 +0100
Subject: [PATCH] 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.
---
 .../SparseDeterministicStepBoundedHorizonHelper.cpp           | 2 +-
 .../SparseDeterministicStepBoundedHorizonHelper.h             | 3 +--
 src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp  | 4 ++--
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp
index 529df4e1f0..d7616b0c7d 100644
--- 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
index 42eb687725..35bbebb1a2 100644
--- 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
index e2a5910dc6..df5fc62793 100644
--- 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;
     }