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().isTraceSet()) { STORM_LOG_TRACE("Writing model to model.dot"); std::ofstream modelDot("model.dot"); @@ -153,8 +152,13 @@ namespace storm { std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(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(new ExplicitQuantitativeCheckResult(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 ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); const SparseMdpModelType& mdp = this->getModel(); - // TODO ? if (storm::settings::getModule().isTraceSet()) { STORM_LOG_TRACE("Writing model to model.dot"); std::ofstream modelDot("model.dot"); @@ -207,7 +206,6 @@ namespace storm { std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); - //TODO for MA too std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(mdp)));