|
|
@ -2,6 +2,8 @@ |
|
|
|
|
|
|
|
#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h" |
|
|
|
|
|
|
|
#include "storm/storage/BitVector.h" |
|
|
|
|
|
|
|
namespace storm { |
|
|
|
|
|
|
|
namespace storage { |
|
|
@ -28,7 +30,7 @@ namespace storm { |
|
|
|
/*! |
|
|
|
* Initializes the helper for a discrete time model with different players (i.e. SMG) |
|
|
|
*/ |
|
|
|
SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player); |
|
|
|
SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition); |
|
|
|
|
|
|
|
/*! TODO |
|
|
|
* Computes the long run average value given the provided state and action based rewards |
|
|
@ -64,7 +66,7 @@ namespace storm { |
|
|
|
std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues); |
|
|
|
|
|
|
|
private: |
|
|
|
std::vector<std::pair<std::string, uint_fast64_t>> player; |
|
|
|
storm::storage::BitVector statesOfCoalition; |
|
|
|
}; |
|
|
|
|
|
|
|
|
|
|
|