diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp new file mode 100644 index 000000000..baaa3782d --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -0,0 +1,56 @@ +#include "SparseNondeterministicGameInfiniteHorizonHelper.h" + +#include "storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h" + +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/Scheduler.h" + +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" + +#include "storm/utility/solver.h" +#include "storm/utility/vector.h" + +#include "storm/environment/solver/LongRunAverageSolverEnvironment.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + +#include "storm/exceptions/UnmetRequirementException.h" +#include "storm/exceptions/InternalException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& coalitionIndices) : SparseInfiniteHorizonHelper(transitionMatrix), coalitionIndices(coalitionIndices) { + // Intentionally left empty. + } + + template + void SparseNondeterministicGameInfiniteHorizonHelper::createDecomposition() { + STORM_LOG_THROW(false, storm::exceptions::InternalException, "Creating Decompositions of SMGs is currently not possible."); + } + + template + ValueType SparseNondeterministicGameInfiniteHorizonHelper::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) { + + STORM_LOG_THROW(false, storm::exceptions::InternalException, "Computing values for LRA for SMGs components is currently not possible."); + } + + template + std::vector SparseNondeterministicGameInfiniteHorizonHelper::buildAndSolveSsp(Environment const& env, std::vector const& componentLraValues) { + STORM_LOG_THROW(false, storm::exceptions::InternalException, "buildAndSolveSsp not available for SMGs"); + } + + template + std::vector SparseNondeterministicGameInfiniteHorizonHelper::computeLongRunAverageValues(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter) { + STORM_LOG_THROW(false, storm::exceptions::InternalException, "computeLongRunAverageValues not possible yet."); + } + + + template class SparseNondeterministicGameInfiniteHorizonHelper; + template class SparseNondeterministicGameInfiniteHorizonHelper; + + } + } +} diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h new file mode 100644 index 000000000..550d12a47 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h @@ -0,0 +1,66 @@ +#pragma once +#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h" + +namespace storm { + + namespace storage { + template class Scheduler; + } + + namespace modelchecker { + namespace helper { + + /*! + * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system with different players choices. + * @tparam ValueType the type a value can have + */ + template + class SparseNondeterministicGameInfiniteHorizonHelper : public SparseInfiniteHorizonHelper { + + public: + + /*! + * Function mapping from indices to values + */ + typedef typename SparseInfiniteHorizonHelper::ValueGetter ValueGetter; + + /*! + * Initializes the helper for a discrete time model with different players (i.e. SMG) + */ + SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& coalitionIndices); + + /*! + * TODO + */ + std::vector computeLongRunAverageValues(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter); + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + //std::vector const& getProducedOptimalChoices() const; + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return the produced scheduler of the most recent call. + */ + //std::vector& getProducedOptimalChoices(); + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call. + */ + //storm::storage::Scheduler extractScheduler() const; + + void createDecomposition(); + ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component); + std::vector buildAndSolveSsp(Environment const& env, std::vector const& mecLraValues); + + private: + std::vector coalitionIndices; + }; + + + } + } +}