allowing multi(...) path formulas in multiobjective model checking

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@@ -177,6 +177,8 @@ namespace storm {
                     preprocessUntilFormula(formula.getSubformula().asUntilFormula(), opInfo, data);
                 } else if (formula.getSubformula().isBoundedUntilFormula()){
                     preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), opInfo, data);
+                } else if (formula.getSubformula().isMultiObjectiveFormula()){
+                    preprocessMultiObjectiveSubformula(formula.getSubformula().asMultiObjectiveFormula(), opInfo, data);
                 } else if (formula.getSubformula().isGloballyFormula()){
                     preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), opInfo, data);
                 } else if (formula.getSubformula().isEventuallyFormula()){
@@ -263,6 +265,15 @@ namespace storm {
                 
             }
             
+            template<typename SparseModelType>
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
+                // Check whether only bounded until formulas are contained
+                for (auto const& f : formula.getSubformulas()) {
+                    STORM_LOG_THROW(f->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "MultiObjective subformulas are only allowed if they all contain bounded until formulas");
+                }
+                data.objectives.back()->formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(formula.asSharedPointer(), opInfo);
+            }
+            
             template<typename SparseModelType>
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
                 

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h

@@ -60,6 +60,7 @@ namespace storm {
                 static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
                 static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr<storm::logic::Formula const> subformula = nullptr);
                 static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
+                static void preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
                 static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data);
                 static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);
                 static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName = boost::none);

src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp

@@ -29,7 +29,7 @@ namespace storm {
                 // set the state action rewards. Also do some sanity checks on the objectives.
                 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
                     auto const& formula = *objectives[objIndex].formula;
-                    if (!(formula.isProbabilityOperatorFormula() && formula.getSubformula().isBoundedUntilFormula())) {
+                    if (!(formula.isProbabilityOperatorFormula() && (formula.getSubformula().isBoundedUntilFormula() || formula.getSubformula().isMultiObjectiveFormula()))) {
                         STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula);
                         STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() || formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula());
                         typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName());
@@ -44,7 +44,7 @@ namespace storm {
                 // Currently, only step bounds are considered.
                 bool containsRewardBoundedObjectives = false;
                 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
-                    if (this->objectives[objIndex].formula->getSubformula().isBoundedUntilFormula()) {
+                    if (this->objectives[objIndex].formula->isProbabilityOperatorFormula()) {
                         containsRewardBoundedObjectives = true;
                         break;
                     }