diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index a2be16070..5ad26ce62 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -13,7 +13,7 @@ namespace storm { namespace internal { template - BoundedGloballyGameViHelper::GameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + BoundedGloballyGameViHelper::BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { } template @@ -23,12 +23,9 @@ namespace storm { } template - void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliersReachability(env); - // TODO: parse k from the formula - uint64_t k = 3; _b = b; - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x2 = _x1; @@ -40,22 +37,22 @@ namespace storm { } uint64_t iter = 0; - std::vector result = x; - while (iter < k) { + while (iter < upperBound) { ++iter; + performIterationStep(env, dir); - if (storm::utility::resources::isTerminate()) { +/* if (storm::utility::resources::isTerminate()) { break; - } + }*/ } + x = xNew(); - // TODO: do we have to do that by using boundedGlobally? - if (isProduceSchedulerSet()) { +/* if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. performIterationStep(env, dir, &_producedOptimalChoices.get()); - } + }*/ } template @@ -68,12 +65,7 @@ namespace storm { // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - //STORM_LOG_DEBUG("\n" << _transitionMatrix); - //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld())); - //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b)); - //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew())); _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); - //std::cin.get(); } else { // Also keep track of the choices made. _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); @@ -94,7 +86,7 @@ namespace storm { template void BoundedGloballyGameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector psiStates) { - std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); + std::vector filledVector = std::vector(psiStates.size(), storm::utility::zero()); uint bitIndex = 0; for(uint i = 0; i < filledVector.size(); i++) { if (psiStates.get(i)) { diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index f8b079847..413dfb56a 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -23,8 +23,7 @@ namespace storm { void prepareSolversAndMultipliersReachability(const Environment& env); - // TODO: add 'k' as input of the method - maybe the type TimeBound from the formula - void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); + void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound); /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates