store tuples of player name and index

Store this instead of only the index. Needed for easier parsing of the
rpatl formulas (prism allows player indices and names!)

src/storm/generator/Choice.cpp

@@ -11,30 +11,30 @@
 
 namespace storm {
     namespace generator {
-        
+
         template<typename ValueType, typename StateType>
         Choice<ValueType, StateType>::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero<ValueType>()), rewards(), labels() {
             // Intentionally left empty.
         }
-        
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::add(Choice const& other) {
             STORM_LOG_THROW(this->markovian == other.markovian, storm::exceptions::InvalidOperationException, "Type of choices do not match.");
             STORM_LOG_THROW(this->actionIndex == other.actionIndex, storm::exceptions::InvalidOperationException, "Action index of choices do not match.");
             STORM_LOG_THROW(this->rewards.size() == other.rewards.size(), storm::exceptions::InvalidOperationException, "Reward value sizes of choices do not match.");
-            
+
             // Add the elements to the distribution.
             this->distribution.add(other.distribution);
-            
+
             // Update the total mass of the choice.
             this->totalMass += other.totalMass;
-            
+
             // Add all reward values.
             auto otherRewIt = other.rewards.begin();
             for (auto& rewardValue : this->rewards) {
                 rewardValue += *otherRewIt;
             }
-            
+
             // Join label sets and origin data if given.
             if (other.labels) {
                 this->addLabels(other.labels.get());
@@ -43,27 +43,27 @@ namespace storm {
                 this->addOriginData(other.originData.get());
             }
         }
-        
+
         template<typename ValueType, typename StateType>
         typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::begin() {
             return distribution.begin();
         }
-        
+
         template<typename ValueType, typename StateType>
         typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::begin() const {
             return distribution.cbegin();
         }
-        
+
         template<typename ValueType, typename StateType>
         typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::end() {
             return distribution.end();
         }
-        
+
         template<typename ValueType, typename StateType>
         typename storm::storage::Distribution<ValueType, StateType>::const_iterator Choice<ValueType, StateType>::end() const {
             return distribution.cend();
         }
-        
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::addLabel(std::string const& newLabel) {
             if (!labels) {
@@ -71,7 +71,7 @@ namespace storm {
             }
             labels->insert(newLabel);
         }
-        
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::addLabels(std::set<std::string> const& newLabels) {
             if (labels) {
@@ -97,8 +97,8 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        bool Choice<ValueType, StateType>::hasPlayerIndex() const {
-            return playerIndex.is_initialized();
+        bool Choice<ValueType, StateType>::hasPlayer() const {
+            return player.is_initialized();
         }
 
         template<typename ValueType, typename StateType>
@@ -113,7 +113,7 @@ namespace storm {
             } else {
                 if (!data.empty()) {
                     // Reaching this point means that the both the existing and the given data are non-empty
-                
+
                     auto existingDataAsIndexSet = boost::any_cast<storm::storage::FlatSet<uint_fast64_t>>(&this->originData.get());
                     if (existingDataAsIndexSet != nullptr) {
                         auto givenDataAsIndexSet = boost::any_cast<storm::storage::FlatSet<uint_fast64_t>>(&data);
@@ -125,63 +125,63 @@ namespace storm {
                 }
             }
         }
-            
+
         template<typename ValueType, typename StateType>
         bool Choice<ValueType, StateType>::hasOriginData() const {
             return originData.is_initialized();
         }
-            
+
         template<typename ValueType, typename StateType>
         boost::any const& Choice<ValueType, StateType>::getOriginData() const {
             return originData.get();
         }
-        
+
         template<typename ValueType, typename StateType>
         uint_fast64_t Choice<ValueType, StateType>::getActionIndex() const {
             return actionIndex;
         }
-        
+
         template<typename ValueType, typename StateType>
         ValueType Choice<ValueType, StateType>::getTotalMass() const {
             return totalMass;
         }
-        
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::addProbability(StateType const& state, ValueType const& value) {
             totalMass += value;
             distribution.addProbability(state, value);
         }
-        
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::addReward(ValueType const& value) {
             rewards.push_back(value);
         }
-        
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::addRewards(std::vector<ValueType>&& values) {
             this->rewards = std::move(values);
         }
-        
+
         template<typename ValueType, typename StateType>
         std::vector<ValueType> const& Choice<ValueType, StateType>::getRewards() const {
             return rewards;
         }
-        
+
         template<typename ValueType, typename StateType>
         bool Choice<ValueType, StateType>::isMarkovian() const {
             return markovian;
         }
-        
+
         template<typename ValueType, typename StateType>
         std::size_t Choice<ValueType, StateType>::size() const {
             return distribution.size();
         }
-        
+
         template<typename ValueType, typename StateType>
         void Choice<ValueType, StateType>::reserve(std::size_t const& size) {
             distribution.reserve(size);
         }
-        
+
         template<typename ValueType, typename StateType>
         std::ostream& operator<<(std::ostream& out, Choice<ValueType, StateType> const& choice) {
             out << "<";
@@ -191,7 +191,7 @@ namespace storm {
             out << ">";
             return out;
         }
-        
+
         template struct Choice<double>;
 
 #ifdef STORM_HAVE_CARL

src/storm/generator/Choice.h

@@ -13,51 +13,51 @@
 
 namespace storm {
     namespace generator {
-        
+
         // A structure holding information about a particular choice.
         template<typename ValueType, typename StateType=uint32_t>
         struct Choice {
         public:
             Choice(uint_fast64_t actionIndex = 0, bool markovian = false);
-            
+
             Choice(Choice const& other) = default;
             Choice& operator=(Choice const& other) = default;
             Choice(Choice&& other) = default;
             Choice& operator=(Choice&& other) = default;
-            
+
             /*!
              * Adds the given choice to the current one.
              */
             void add(Choice const& other);
-            
+
             /*!
              * Returns an iterator to the distribution associated with this choice.
              *
              * @return An iterator to the first element of the distribution.
              */
             typename storm::storage::Distribution<ValueType, StateType>::iterator begin();
-            
+
             /*!
              * Returns an iterator to the distribution associated with this choice.
              *
              * @return An iterator to the first element of the distribution.
              */
             typename storm::storage::Distribution<ValueType, StateType>::const_iterator begin() const;
-            
+
             /*!
              * Returns an iterator past the end of the distribution associated with this choice.
              *
              * @return An iterator past the end of the distribution.
              */
             typename storm::storage::Distribution<ValueType, StateType>::iterator end();
-            
+
             /*!
              * Returns an iterator past the end of the distribution associated with this choice.
              *
              * @return An iterator past the end of the distribution.
              */
             typename storm::storage::Distribution<ValueType, StateType>::const_iterator end() const;
-            
+
             /*!
              * Inserts the contents of this object to the given output stream.
              *
@@ -102,7 +102,7 @@ namespace storm {
             /*!
              * Returns whether there is an index for the player defined for this choice.
              */
-            bool hasPlayerIndex() const;
+            bool hasPlayer() const;
 
             /*!
              * Retrieves the players index associated with this choice

src/storm/logic/Coalition.cpp

@@ -0,0 +1,25 @@
+#include "storm/logic/Coalition.h"
+
+namespace storm {
+    namespace logic {
+
+        Coalition::Coalition(std::vector<boost::variant<std::string, uint_fast64_t>> playerIds) : playerIds(playerIds) {
+            // Intentionally left empty.
+        }
+
+        std::vector<boost::variant<std::string, uint_fast64_t>> Coalition::getPlayerIds() const {
+            return playerIds;
+        }
+
+        std::ostream& operator<<(std::ostream& stream, Coalition const& coalition) {
+            bool firstItem = true;
+            stream << "<<";
+            for (auto const& id : coalition.playerIds) {
+                if(firstItem) { firstItem = false; } else { stream << ","; }
+                stream << id;
+            }
+            stream << ">> ";
+            return stream;
+        }
+    }
+}

src/storm/logic/Coalition.h

@@ -0,0 +1,32 @@
+#ifndef STORM_LOGIC_COALITION_H_
+#define STORM_LOGIC_COALITION_H_
+
+#include <vector>
+#include <string>
+
+#include <boost/optional.hpp>
+#include <boost/variant.hpp>
+#include "storm/storage/BoostTypes.h"
+#include "storm/utility/OsDetection.h"
+
+namespace storm {
+    namespace logic {
+
+        class Coalition {
+        public:
+            Coalition() = default;
+            Coalition(std::vector<boost::variant<std::string, uint_fast64_t>>);
+            Coalition(Coalition const& other) = default;
+
+            std::vector<boost::variant<std::string, uint_fast64_t>> getPlayerIds() const;
+
+            friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition);
+
+        private:
+            std::vector<boost::variant<std::string, uint_fast64_t>> playerIds;
+        };
+    }
+}
+
+
+#endif /* STORM_LOGIC_COALITION_H_ */

src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp

@@ -22,7 +22,7 @@ namespace storm {
         namespace helper {
 
             template <typename ValueType>
-            SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& coalitionIndices) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix), coalitionIndices(coalitionIndices) {
+            SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix), player(player) {
                 // Intentionally left empty.
             }
 

src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h

@@ -27,7 +27,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<uint64_t> const& coalitionIndices);
+                SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player);
 
                 /*!
                  * TODO
@@ -57,7 +57,7 @@ namespace storm {
                 std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues);
 
             private:
-                std::vector<uint64_t> coalitionIndices;
+                std::vector<std::pair<std::string, uint_fast64_t>> player;
             };