diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
index 1a346333b..3b824341f 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -63,7 +63,7 @@ namespace storm {
template<typename ValueType>
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, statesOfCoalition, goal.direction());
+ storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, goal.direction());
// Initialize the x vector and solution vector result.
// TODO Fabian: maybe relevant states (later)
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
index a3817540b..198550e6f 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
@@ -14,7 +14,7 @@ namespace storm {
namespace internal {
template <typename ValueType>
- SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) {
+ SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) {
// Intentionally left empty.
}
@@ -34,7 +34,6 @@ namespace storm {
// Get precision for convergence check.
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
- STORM_LOG_DEBUG("hello" << "world");
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
//_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
_x1L = xL;
@@ -97,14 +96,48 @@ namespace storm {
_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
+ // restricting the none optimal minimizer choices
+ storage::SparseMatrix<ValueType> restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions);
+
+ // storage::SparseMatrix<ValueType> restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions);
+ STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix);
+
// TODO Fabian: find_MSECs() & deflate()
+ storm::storage::MaximalEndComponentDecomposition<ValueType> MECD = storm::storage::MaximalEndComponentDecomposition<ValueType>(restrictedTransMatrix, _backwardTransitions);
+
+ STORM_LOG_DEBUG("MECD: \n" << MECD);
+ // deflate(MECD,restrictedTransMatrix, xNewU());
+ }
+
+ template <typename ValueType>
+ void SoundGameViHelper<ValueType>::deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU)
+ {
+ /* auto rowGroupIndices = restrictedMatrix.getRowGroupIndices();
+ auto mec_it = MECD.begin();
+
+
+ for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
+ uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
+ ValueType optChoice;
+ if (!_minimizerStates[state]) { // check if current state is maximizer state
+ // getting the optimal minimizer choice for the given state
+ optChoice = *std::min_element(choice_it, choice_it + rowGroupSize);
+
+ for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
+ if (*choice_it > optChoice) {
+ result->set(rowGroupIndices[state] + choice, 0);
+ }
+ }
+ // reducing the xNew() (choiceValues) vector for minimizer states
+ choiceValues[state] = optChoice;
+ }
+ } */
}
template <typename ValueType>
void SoundGameViHelper<ValueType>::reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result)
{
- // result BitVec should be initialized with 1s outside the function
- // restrict rows
+ // result BitVec should be initialized with 1s outside the method
auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices();
auto choice_it = choiceValues.begin();
@@ -137,8 +170,6 @@ namespace storm {
}
}
choiceValues.resize(this->_transitionMatrix.getRowGroupCount());
- STORM_LOG_DEBUG("reduced BitVec: " << *result);
- STORM_LOG_DEBUG("reduced x Vector: " << choiceValues);
}
@@ -177,6 +208,7 @@ namespace storm {
_produceScheduler = value;
}
+
template <typename ValueType>
bool SoundGameViHelper<ValueType>::isProduceSchedulerSet() const {
return _produceScheduler;
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
index 21ec6b464..f140eb734 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
@@ -4,6 +4,7 @@
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/Multiplier.h"
+#include "storm/storage/MaximalEndComponentDecomposition.h"
namespace storm {
class Environment;
@@ -19,7 +20,7 @@ namespace storm {
template <typename ValueType>
class SoundGameViHelper {
public:
- SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection);
+ SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection);
void prepareSolversAndMultipliers(const Environment& env);
@@ -73,9 +74,9 @@ namespace storm {
*/
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
+ void deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU);
+
void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result);
- //
- // für alle minimizer states -> reduce zu optimal actions
/*!
* Checks whether the curently computed value achieves the desired precision
@@ -111,6 +112,7 @@ namespace storm {
std::vector<uint64_t>& getProducedOptimalChoices();
storm::storage::SparseMatrix<ValueType> _transitionMatrix;
+ storm::storage::SparseMatrix<ValueType> _backwardTransitions;
storm::storage::BitVector _statesOfCoalition;
std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;