From adc5d9ae686136fbc3beb35a1f44e5967a62a03d Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Fri, 30 Jul 2021 01:03:10 +0200
Subject: [PATCH] MA scheduler export

---
 .../csl/SparseMarkovAutomatonCslModelChecker.cpp          | 8 ++++++--
 .../modelchecker/prctl/SparseMdpPrctlModelChecker.cpp     | 2 --
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
index 9ef8c5f1f..5ebc3f8de 100644
--- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
@@ -136,7 +136,6 @@ namespace storm {
 
             STORM_LOG_INFO("Performing ltl probability computations in embedded MDP...");
 
-            // TODO ?
             if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
                 STORM_LOG_TRACE("Writing model to model.dot");
                 std::ofstream modelDot("model.dot");
@@ -153,8 +152,13 @@ namespace storm {
 
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
+            std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            if (checkTask.isProduceSchedulersSet()) {
+                result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler(embeddedMdp)));
+            }
+
             // We can directly return the numericResult vector as the state space of the CTMC and the embedded MDP are exactly the same
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            return result;
         }
 
                 
diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index cba1864d2..f386d416c 100644
--- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -189,7 +189,6 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached);
 
             const SparseMdpModelType& mdp = this->getModel();
-            // TODO ?
             if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
                 STORM_LOG_TRACE("Writing model to model.dot");
                 std::ofstream modelDot("model.dot");
@@ -207,7 +206,6 @@ namespace storm {
 
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
-            //TODO for MA too
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             if (checkTask.isProduceSchedulersSet()) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler(mdp)));