From b896726c4a5d7bd751a35c23dab52c33bf91a98f Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 31 Jul 2019 19:03:20 +0200
Subject: [PATCH] Include choice labels in exported scheduler.

---
 src/storm/storage/Scheduler.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp
index ed118b4ca..fa40732c6 100644
--- a/src/storm/storage/Scheduler.cpp
+++ b/src/storm/storage/Scheduler.cpp
@@ -3,6 +3,7 @@
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotImplementedException.h"
+#include <boost/algorithm/string/join.hpp>
 
 namespace storm {
     namespace storage {
@@ -125,6 +126,7 @@ namespace storm {
             STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler.");
             
             bool const stateValuationsGiven = model != nullptr && model->hasStateValuations();
+            bool const choiceLabelsGiven = model != nullptr && model->hasChoiceLabeling();
             bool const choiceOriginsGiven = model != nullptr && model->hasChoiceOrigins();
             uint_fast64_t widthOfStates = std::to_string(schedulerChoices.front().size()).length();
             if (stateValuationsGiven) {
@@ -181,6 +183,10 @@ namespace storm {
                                 } else {
                                     out << choice.getDeterministicChoice();
                                 }
+                                if (choiceLabelsGiven) {
+                                    auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
+                                    out << " {" << boost::join(choiceLabels, ", ") << "}";
+                                }
                             } else {
                                 bool firstChoice = true;
                                 for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
@@ -195,6 +201,10 @@ namespace storm {
                                     } else {
                                         out << choiceProbPair.first;
                                     }
+                                    if (choiceLabelsGiven) {
+                                        auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(model->getTransitionMatrix().getRowGroupIndices()[state] + choice.getDeterministicChoice());
+                                        out << " {" << boost::join(choiceLabels, ", ") << "}";
+                                    }
                                     out << ")";
                                 }
                             }