diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 7fb39bf1d..7571a0862 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -111,14 +111,15 @@ namespace storm { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); - // Initialize the solution vector. - std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); - // Relevant states are safe states - the psiStates. storm::storage::BitVector relevantStates = psiStates; - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); + // Initialize the solution vector. + //std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); + //std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); + std::vector b = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -142,10 +143,12 @@ namespace storm { STORM_LOG_DEBUG("upperBound = " << upperBound); // in case of 'G<1' or 'G<=0' the states with are initially 'safe' are filled with ones - if(upperBound == 0) + if(upperBound > 0) { - x = std::vector(relevantStates.size(), storm::utility::one()); - } else { +/* x = std::vector(relevantStates.size(), storm::utility::one()); + } else {*/ + STORM_LOG_DEBUG("b = " << b); + STORM_LOG_DEBUG("x = " << x); viHelper.performValueIteration(env, x, b, goal.direction(), upperBound); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 177301730..f4bfbabb2 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -19,16 +19,25 @@ namespace storm { template void BoundedGloballyGameViHelper::prepareSolversAndMultipliersReachability(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); +/* _x1IsCurrent = false; +*/ } template void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliersReachability(env); _b = b; +/* _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); +*/ + _x1 = x; _x2 = _x1; +/* STORM_LOG_DEBUG("_b = " << _b); + STORM_LOG_DEBUG("_x1 = " << _x1); + STORM_LOG_DEBUG("_x2 = " << _x2);*/ + if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); @@ -37,15 +46,20 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { - performIterationStep(env, dir); +/* STORM_LOG_DEBUG("After iteration " << iter << ":"); + STORM_LOG_DEBUG("_x1 = " << _x1); + STORM_LOG_DEBUG("_x2 = " << _x2);*/ /* if (storm::utility::resources::isTerminate()) { break; }*/ } +/* x = xNew(); +*/ + x = _x1; /* if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. @@ -58,18 +72,18 @@ namespace storm { if (!_multiplier) { prepareSolversAndMultipliersReachability(env); } - _x1IsCurrent = !_x1IsCurrent; +/* _x1IsCurrent = !_x1IsCurrent;*/ // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, choices, &_statesOfCoalition); } - // compare applyPointwise +/* // compare applyPointwise storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { if(storm::solver::maximize(dir)) { if(a > b) return a; @@ -78,7 +92,7 @@ namespace storm { if(a > b) return a; else return b; } - }); + });*/ } template @@ -129,7 +143,7 @@ namespace storm { return scheduler; } - template +/* template std::vector& BoundedGloballyGameViHelper::xNew() { return _x1IsCurrent ? _x1 : _x2; } @@ -147,7 +161,7 @@ namespace storm { template std::vector const& BoundedGloballyGameViHelper::xOld() const { return _x1IsCurrent ? _x2 : _x1; - } + }*/ template class BoundedGloballyGameViHelper; #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 413dfb56a..1553d369f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -45,12 +45,12 @@ namespace storm { private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - std::vector& xNew(); +/* std::vector& xNew(); std::vector const& xNew() const; std::vector& xOld(); std::vector const& xOld() const; - bool _x1IsCurrent; + bool _x1IsCurrent;*/ /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.