Polished GameFormula and Coalition code

src/storm/logic/Coalition.cpp

@@ -3,18 +3,16 @@
 namespace storm {
     namespace logic {
 
-        Coalition::Coalition(std::vector<boost::variant<std::string, uint64_t>> playerIds) : playerIds(playerIds) {
+        Coalition::Coalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> playerIds) : _playerIds(playerIds) {
             // Intentionally left empty.
         }
 
         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 << ","; }
+            for (auto const& id : coalition._playerIds) {
+                if (firstItem) { firstItem = false; } else { stream << ","; }
                 stream << id;
             }
-            stream << ">> ";
             return stream;
         }
     }

src/storm/logic/Coalition.h

@@ -1,13 +1,10 @@
-#ifndef STORM_LOGIC_COALITION_H_
-#define STORM_LOGIC_COALITION_H_
+#pragma once
 
 #include <vector>
 #include <string>
 
-#include <boost/optional.hpp>
 #include <boost/variant.hpp>
-#include "storm/storage/BoostTypes.h"
-#include "storm/utility/OsDetection.h"
+#include "storm/storage/PlayerIndex.h"
 
 namespace storm {
     namespace logic {
@@ -15,16 +12,13 @@ namespace storm {
         class Coalition {
         public:
             Coalition() = default;
-            Coalition(std::vector<boost::variant<std::string, uint64_t>>);
+            Coalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> playerIds);
             Coalition(Coalition const& other) = default;
 
             friend std::ostream& operator<<(std::ostream& stream, Coalition const& coalition);
 
         private:
-            std::vector<boost::variant<std::string, uint64_t>> playerIds;
+            std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> _playerIds;
         };
     }
 }
-
-
-#endif /* STORM_LOGIC_COALITION_H_ */

src/storm/logic/GameFormula.cpp

@@ -4,7 +4,7 @@
 
 namespace storm {
     namespace logic {
-        GameFormula::GameFormula(Coalition coalition, std::shared_ptr<Formula const> const& subformula) : coalition(coalition), subformula(subformula) {
+        GameFormula::GameFormula(Coalition const& coalition, std::shared_ptr<Formula const> subformula) : UnaryStateFormula(subformula), coalition(coalition) {
             // Intentionally left empty.
         }
 
@@ -12,24 +12,24 @@ namespace storm {
             return true;
         }
 
-        Formula const& GameFormula::getSubformula() const {
-            return *subformula;
+        bool GameFormula::hasQualitativeResult() const {
+            return this->getSubformula().hasQualitativeResult();
         }
 
-        Coalition GameFormula::getCoalition() const {
-            return coalition;
+        bool GameFormula::hasQuantitativeResult() const {
+            return this->getSubformula().hasQuantitativeResult();
         }
 
-        void GameFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
-            this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
+        Coalition const& GameFormula::getCoalition() const {
+            return coalition;
         }
-
+        
         boost::any GameFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
 
         std::ostream& GameFormula::writeToStream(std::ostream& out) const {
-            out << coalition;
+            out << "<<" << coalition << ">> ";
             this->getSubformula().writeToStream(out);
             return out;
         }

src/storm/logic/GameFormula.h

@@ -1,35 +1,31 @@
 #ifndef STORM_LOGIC_GAMEFORMULA_H_
 #define STORM_LOGIC_GAMEFORMULA_H_
 
-#include "storm/logic/Formula.h"
+#include "storm/logic/UnaryStateFormula.h"
 #include "storm/logic/Coalition.h"
 #include <memory>
 
 namespace storm {
     namespace logic {
-        class GameFormula : public Formula {
+        class GameFormula : public UnaryStateFormula {
         public:
-            GameFormula(Coalition coalition, std::shared_ptr<Formula const> const& subFormula);
+            GameFormula(Coalition const& coalition, std::shared_ptr<Formula const> subFormula);
 
-            ~GameFormula() {
+            virtual ~GameFormula() {
                 // Intentionally left empty.
             }
 
-            bool isGameFormula() const;
+            Coalition const& getCoalition() const;
+            virtual bool isGameFormula() const override;
+            virtual bool hasQualitativeResult() const override;
+            virtual bool hasQuantitativeResult() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
-            Formula const& getSubformula() const;
-            Coalition getCoalition() const;
-
-            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
-
-            boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const;
-
-            std::ostream& writeToStream(std::ostream& out) const;
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
 
         private:
             Coalition coalition;
-            std::shared_ptr<Formula const> subformula;
-
         };
     }
 }