diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp index c14a9ba93..d9e2681a6 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -116,7 +116,7 @@ namespace storm { if (this->isContinuousTime()) { STORM_LOG_THROW(false, storm::exceptions::InternalException, "We cannot handle continuous time games."); } else { - storm::modelchecker::helper::internal::LraViHelper viHelper(mec, this->_transitionMatrix, aperiodicFactor); + storm::modelchecker::helper::internal::LraViHelper viHelper(mec, this->_transitionMatrix, aperiodicFactor, nullptr, nullptr, &statesOfCoalition); return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices); } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 28ace1d81..41b08ac1b 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -26,7 +26,7 @@ namespace storm { namespace internal { template - LraViHelper::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector const* exitRates) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false) { + LraViHelper::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector const* exitRates, storm::storage::BitVector const* statesOfCoalition) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false), _statesOfCoalition(statesOfCoalition) { setComponent(component); // Run through the component and collect some data: @@ -167,6 +167,9 @@ namespace storm { if (env.solver().lra().isMaximalIterationCountSet()) { maxIter = env.solver().lra().getMaximalIterationCount(); } + if(gameNondetTs()) { + STORM_LOG_ASSERT(_statesOfCoalition != nullptr, "Tried to solve LRA problem for a game, but coalition states have not been set."); + } // start the iterations ValueType result = storm::utility::zero(); @@ -218,13 +221,13 @@ namespace storm { } performIterationStep(env, dir, choices); } - std::cout << "result (" << iter << " steps):" << std::endl; + //std::cout << "result (" << iter << " steps):" << std::endl; storm::utility::vector::applyPointwise(xNew(), xNew(), [&iter] (ValueType const& x_i) -> ValueType { return x_i / (double)iter; }); - for(int i = 0; i < xNew().size() ; i++ ) { - std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl; - //if(i == 50) {std::cout << "only showing top 50 lines"; break; } - } - if(gameNondetTs()) result = xOld().at(0) * _uniformizationRate; // TODO is "init" always going to be .at(0) ? + //for(int i = 0; i < xNew().size() ; i++ ) { + // std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl; + // //if(i == 50) {std::cout << "only showing top 50 lines"; break; } + //} + if(gameNondetTs()) result = (xOld().at(0) * _uniformizationRate)/(double)iter; // TODO is "init" always going to be .at(0) ? return result; } @@ -386,10 +389,10 @@ namespace storm { } } else if(gameNondetTs()) { // TODO DRYness? exact same behaviour as case above? if (choices == nullptr) { - _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew()); + _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), nullptr, _statesOfCoalition); } else { std::vector tsChoices(_TsTransitions.getRowGroupCount()); - _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices); + _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices, _statesOfCoalition); setInputModelChoices(*choices, tsChoices); // no components -> no need for that call? } } else { diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h index c800a9976..abd1576de 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h @@ -8,12 +8,12 @@ namespace storm { class Environment; - - + + namespace modelchecker { namespace helper { namespace internal { - + /*! * Specifies differnt kinds of transition types with which this helper can be used * Ts means timed states (cf. Markovian states in a Markov Automaton) and Is means instant states (cf. probabilistic states in a Markov automaton). @@ -45,7 +45,7 @@ namespace storm { public: /// Function mapping from indices to values typedef std::function ValueGetter; - + /*! * Initializes a new VI helper for the provided MEC or BSCC * @param component the MEC or BSCC @@ -55,7 +55,7 @@ namespace storm { * @param exitRates The exit rates of the timed states (relevant for continuous time models). If nullptr, all rates are assumed to be 1 (which corresponds to a discrete time model) * @note All indices and vectors must be w.r.t. the states as described by the provided transition matrix */ - LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates = nullptr, std::vector const* exitRates = nullptr); + LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates = nullptr, std::vector const* exitRates = nullptr, storm::storage::BitVector const* statesOfCoalition = nullptr); /*! * Performs value iteration with the given state- and action values. @@ -69,9 +69,9 @@ namespace storm { * @note it is possible to call this method multiple times with different values. However, other changes to the environment or the optimization direction might not have the expected effect due to caching. */ ValueType performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates = nullptr, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr); - + private: - + /*! * Initializes the value iterations with the provided values. * Resets all information from potential previous calls. @@ -80,7 +80,7 @@ namespace storm { * @param stateValueGetter Function that returns for each global choice index (w.r.t. the input transitions) the value (e.g. reward) for that choice */ void initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates = nullptr); - + /*! * Performs a single iteration step. * @param env The environment. @@ -90,41 +90,41 @@ namespace storm { * @pre when calling this the first time, initializeNewValues must have been called before. Moreover, prepareNextIteration must be called between two calls of this. */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr); - + struct ConvergenceCheckResult { bool isPrecisionAchieved; ValueType currentValue; }; - + /*! * Checks whether the curently computed value achieves the desired precision */ ConvergenceCheckResult checkConvergence(bool relative, ValueType precision) const; - + /*! * Must be called between two calls of performIterationStep. */ void prepareNextIteration(Environment const& env); - + /// Prepares the necessary solvers and multipliers for doing the iterations. void prepareSolversAndMultipliers(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr); - + void setInputModelChoices(std::vector& choices, std::vector const& localMecChoices, bool setChoiceZeroToMarkovianStates = false, bool setChoiceZeroToProbabilisticStates = false) const; - + /// Returns true iff the given state is a timed state bool isTimedState(uint64_t const& inputModelStateIndex) const; - + /// The result for timed states of the most recent iteration std::vector& xNew(); std::vector const& xNew() const; - + /// The result for timed states of the previous iteration std::vector& xOld(); std::vector const& xOld() const; /// @return true iff there potentially is a nondeterministic choice at timed states bool nondetTs() const; - + /// @return true iff there potentially is a nondeterministic choice at instant states. Returns false if there are no instant states. bool nondetIs() const; @@ -132,14 +132,15 @@ namespace storm { bool gameNondetTs() const; void setComponent(ComponentType component); - + // We need to make sure that states/choices will be processed in ascending order typedef std::map> InternalComponentType; - + InternalComponentType _component; storm::storage::SparseMatrix const& _transitionMatrix; storm::storage::BitVector const* _timedStates; // e.g. Markovian states of a Markov automaton. + storm::storage::BitVector const* _statesOfCoalition; bool _hasInstantStates; ValueType _uniformizationRate; storm::storage::SparseMatrix _TsTransitions, _TsToIsTransitions, _IsTransitions, _IsToTsTransitions; @@ -154,4 +155,4 @@ namespace storm { } } } -} \ No newline at end of file +}