Browse Source

fix for playerIndex in Choice

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
44378ac9a1
  1. 4
      src/storm/generator/Choice.cpp
  2. 2
      src/storm/generator/Choice.h

4
src/storm/generator/Choice.cpp

@ -97,8 +97,8 @@ namespace storm {
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
bool Choice<ValueType, StateType>::hasPlayer() const {
return player.is_initialized();
bool Choice<ValueType, StateType>::hasPlayerIndex() const {
return playerIndex.is_initialized();
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>

2
src/storm/generator/Choice.h

@ -102,7 +102,7 @@ namespace storm {
/*! /*!
* Returns whether there is an index for the player defined for this choice. * Returns whether there is an index for the player defined for this choice.
*/ */
bool hasPlayer() const;
bool hasPlayerIndex() const;
/*! /*!
* Retrieves the players index associated with this choice * Retrieves the players index associated with this choice

Loading…
Cancel
Save