From 8304c897cd17f143cc9846480289f83cb6f73cb1 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Mon, 26 Jul 2021 18:07:44 +0200
Subject: [PATCH] refactored creation of coalitionStates

---
 src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
index c3cb606f2..3f74d8bfc 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
+++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
@@ -70,7 +70,9 @@ namespace storm {
                 std::cout << "Creating Shield for " << checkTask.getShieldingExpression() << std::endl;
             }
 
+            STORM_LOG_THROW(checkTask.isPlayerCoalitionSet(), storm::exceptions::InvalidPropertyException, "No player coalition was set.");
             statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition());
+            std::cout << "Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition." << std::endl;
             statesOfCoalition.complement();
 
             if (subFormula.isRewardOperatorFormula()) {
@@ -209,10 +211,6 @@ namespace storm {
         template<typename SparseSmgModelType>
         std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
             auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
-            // TODO
-            //STORM_LOG_THROW(checkTask.isPlayerCoalitionSet(), storm::exceptions::InvalidPropertyException, "No player coalition was set.");
-            //auto coalitionStates = this->getModel().computeStatesOfCoalition(checkTask.getPlayerCoalition());
-            std::cout << "Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition." << std::endl;
             storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper<ValueType> helper(this->getModel().getTransitionMatrix(), statesOfCoalition);
             storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel());
             auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());