From b14c554df26000d8aaa9c889a92740ba221f0ee1 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 27 Jun 2018 15:38:10 +0200
Subject: [PATCH] correct treatment of Markov Automata in scheduler evaluator

---
 .../MultiObjectiveSchedulerEvaluator.cpp      | 23 +++++++++++++++----
 .../MultiObjectiveSchedulerEvaluator.h        |  4 ++++
 2 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp
index f1c78f98d..99a1b5d79 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp
@@ -1,3 +1,4 @@
+#include <storm/transformer/ContinuousToDiscreteTimeModelTransformer.h>
 #include "storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h"
 
 
@@ -27,9 +28,21 @@ namespace storm {
             
             template <class ModelType>
             MultiObjectiveSchedulerEvaluator<ModelType>::MultiObjectiveSchedulerEvaluator(preprocessing::SparseMultiObjectivePreprocessorResult<ModelType>& preprocessorResult) : model(*preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives), currSchedHasBeenChecked(false) {
-                results.resize(this->objectives.size());
+                results.resize(this->objectives.size(), std::vector<ValueType>(getModel().getNumberOfStates()));
                 currSched.resize(this->getModel().getNumberOfStates(), 0);
                 initializeSchedulerIndependentStates();
+                if (getModel().isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                    bool transformMaToMdp = true;
+                    for (auto const& obj : objectives) {
+                        if (!storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType>::preservesFormula(*obj.formula)) {
+                            transformMaToMdp = false;
+                        }
+                    }
+                    if (transformMaToMdp) {
+                        auto modelAsMa = getModel().template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
+                        mdp = storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType>::transform(*modelAsMa);
+                    }
+                }
             }
             
             template <class ModelType>
@@ -71,7 +84,6 @@ namespace storm {
             template<typename ValueType>
             std::unique_ptr<storm::modelchecker::CheckResult> invokeModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
                 if (model->getType() == storm::models::ModelType::Dtmc) {
-                    return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>>(*model->template as<storm::models::sparse::Dtmc<ValueType>>()).check(env, task);
                 } else if(model->getType() == storm::models::ModelType::Ctmc) {
                     return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>>(*model->template as<storm::models::sparse::Ctmc<ValueType>>()).check(env, task);
                 } else {
@@ -87,11 +99,12 @@ namespace storm {
                         scheduler.setChoice(currSched[state], state);
                     }
                     
-                    auto detModel = model.applyScheduler(scheduler, false);
-                    
+                    auto detModel = mdp ? mdp->applyScheduler(scheduler, false) : model.applyScheduler(scheduler, false);
+                    STORM_LOG_ASSERT(detModel->isOfType(storm::models::ModelType::Dtmc), "Model is of unexpected type.");
+                    auto const& dtmc = *(detModel->template as<storm::models::sparse::Dtmc<ValueType>>());
                     for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
                         storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> task(*this->objectives[objIndex].formula, false);
-                        auto res = invokeModelChecker<ValueType>(env, detModel, task);
+                        auto res = storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>>(dtmc).check(env, task);
                         results[objIndex] = std::move(res->template asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
                     }
                     currSchedHasBeenChecked = true;
diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h
index edb68b705..c2e4970aa 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h
@@ -3,6 +3,7 @@
 #include <vector>
 
 #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
+#include "storm/models/sparse/Mdp.h"
 
 namespace storm {
     
@@ -45,6 +46,9 @@ namespace storm {
                 void initializeSchedulerIndependentStates();
                 
                 ModelType const& model;
+                // In case the model is a markov automaton, we transform it to an mdp
+                std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
+                
                 std::vector<Objective<ValueType>> const& objectives;
                 
                 // Indicates for each objective the set of states for which the result is fix (i.e. independent of the scheduler).