From 877067cdcca13bd6204b21cddbb7821b30d985eb Mon Sep 17 00:00:00 2001
From: Fabian Russold <fabian.russold@student.tugraz.at>
Date: Fri, 26 Jul 2024 10:29:46 +0200
Subject: [PATCH] SparseSmgRpatlHelper.cpp added return value
---
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 3 +++
.../modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp | 1 -
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
index 29d41b45c..566120827 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -64,6 +64,8 @@ namespace storm {
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(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, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, goal.direction());
+ std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
+ storm::storage::BitVector relevantStates(psiStates.size(), true);
// Initialize the x vector and solution vector result.
// TODO Fabian: maybe relevant states (later)
@@ -93,6 +95,7 @@ namespace storm {
std::vector<ValueType> constrainedChoiceValues;
viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues);
+ return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
assert(false);
}
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
index 10de545e3..5a7109cac 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
@@ -28,7 +28,6 @@ namespace storm {
template <typename ValueType>
void SoundGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& xL, std::vector<ValueType>& xU, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues) {
- // new pair (x_old, x_new) for over_approximation()
prepareSolversAndMultipliers(env);
// Get precision for convergence check.