diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp index 529df4e1f..d7616b0c7 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp @@ -27,7 +27,6 @@ SparseDeterministicStepBoundedHorizonHelper::SparseDeterministicStepB template std::vector SparseDeterministicStepBoundedHorizonHelper::compute(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix 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 SparseDeterministicStepBoundedHorizonHelper::c if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { maybeStates = hint.template asExplicitModelCheckerHint().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 42eb68772..35bbebb1a 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 compute(Environment const& env, storm::solver::SolveGoal&& goal, - storm::storage::SparseMatrix const& transitionMatrix, - storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::SparseMatrix 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 e2a5910dc..df5fc6279 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -101,8 +101,8 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c storm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper helper; std::vector numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), - this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), - pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), checkTask.getHint()); + leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound(), + pathFormula.getNonStrictUpperBound(), checkTask.getHint()); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); return result; }