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 bool HybridMdpPrctlModelChecker::canHandle(CheckTask 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 @@ -102,6 +115,11 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::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 + std::unique_ptr HybridMdpPrctlModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer::translate(this->getModel()); + return multiobjective::performPcaa(*sparseModel, checkTask.getFormula()); + } template class HybridMdpPrctlModelChecker>; template class HybridMdpPrctlModelChecker>; 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 computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask 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));