Browse Source

smg model now stores the player action indices

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
e998cb669b
  1. 5
      src/storm/models/sparse/Smg.cpp
  2. 2
      src/storm/models/sparse/Smg.h

5
src/storm/models/sparse/Smg.cpp

@ -37,7 +37,6 @@ namespace storm {
storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::getPlayerOfState(uint64_t stateIndex) const {
STORM_LOG_ASSERT(stateIndex < this->getNumberOfStates(), "Invalid state index: " << stateIndex << ".");
return statePlayerIndications[stateIndex];
}
template <typename ValueType, typename RewardModelType>
storm::storage::PlayerIndex Smg<ValueType, RewardModelType>::getPlayerIndex(std::string const& playerName) const {
@ -62,7 +61,7 @@ namespace storm {
for (auto const& pi : coalitionAsIndexSet) {
coalitionAsBitVector.set(pi);
}
// Now create the actual result
storm::storage::BitVector result(this->getNumberOfStates(), false);
for (uint64_t state = 0; state < this->getNumberOfStates(); ++state) {
@ -71,7 +70,7 @@ namespace storm {
result.set(state, true);
}
}
return result;
}

2
src/storm/models/sparse/Smg.h

@ -34,7 +34,7 @@ namespace storm {
storm::storage::PlayerIndex getPlayerOfState(uint64_t stateIndex) const;
storm::storage::PlayerIndex getPlayerIndex(std::string const& playerName) const;
storm::storage::BitVector computeStatesOfCoalition(storm::logic::PlayerCoalition const& coalition) const;
private:
// Assigns the controlling player to each state.
// If a state has storm::storage::INVALID_PLAYER_INDEX, it shall be the case that the choice at that state is unique

Loading…
Cancel
Save