From 2567d070373bdf82d09d9da65597be0d6191d0f6 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 15 Feb 2017 22:33:00 +0100
Subject: [PATCH] hybrid multi-objective model checking.

---
 .../prctl/HybridMdpPrctlModelChecker.cpp      | 20 ++++++++++++++++++-
 .../prctl/HybridMdpPrctlModelChecker.h        |  1 +
 .../SymbolicToSparseTransformer.cpp           |  2 +-
 3 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
index 56aed7679..d42d81251 100644
--- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
@@ -10,10 +10,15 @@
 
 #include "storm/logic/FragmentSpecification.h"
 
+#include "storm/modelchecker/multiobjective/pcaa.h"
+
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 
 #include "storm/settings/modules/GeneralSettings.h"
 
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/transformer/SymbolicToSparseTransformer.h"
+
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 
@@ -32,7 +37,15 @@ namespace storm {
         template<typename ModelType>
         bool HybridMdpPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
+            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false))) {
+                return true;
+            } else {
+                // Check whether we consider a multi-objective formula
+                // For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that all states are considered.
+                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
+            }
+
         }
                 
         template<typename ModelType>
@@ -102,6 +115,11 @@ namespace storm {
             return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
         }
 
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
+            auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ValueType>::translate(this->getModel());
+			return multiobjective::performPcaa(*sparseModel, checkTask.getFormula());
+        }
 
         template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
         template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h
index 426be343b..e14177363 100644
--- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h
+++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h
@@ -35,6 +35,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
 
         private:
             // An object that is used for retrieving linear equation solvers.
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp
index 4cb266354..a8b82133f 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.cpp
+++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp
@@ -34,7 +34,7 @@ namespace storm {
             }
             storm::models::sparse::StateLabeling labelling;
 
-            labelling.addLabel("initial", symbolicMdp.getInitialStates().toVector(odd));
+            labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd));
             labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd));
             for(auto const& label : symbolicMdp.getLabels()) {
                 labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));