requiring that multi objective queries have a multi(..) formula at top level.

src/storm/logic/FragmentChecker.cpp

@@ -24,6 +24,9 @@ namespace storm {
             if (specification.isOperatorAtTopLevelRequired()) {
                 result &= f.isOperatorFormula();
             }
+            if (specification.isMultiObjectiveFormulaAtTopLevelRequired()) {
+                result &= f.isMultiObjectiveFormula();
+            }
             
             return result;
         }

src/storm/logic/FragmentSpecification.cpp

@@ -88,6 +88,7 @@ namespace storm {
             FragmentSpecification multiObjective = propositional();
             
             multiObjective.setMultiObjectiveFormulasAllowed(true);
+            multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true);
             multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(true);
             multiObjective.setProbabilityOperatorsAllowed(true);
             multiObjective.setUntilFormulasAllowed(true);
@@ -148,6 +149,7 @@ namespace storm {
             quantitativeOperatorResults = true;
             
             operatorAtTopLevelRequired = false;
+            multiObjectiveFormulaAtTopLevelRequired = false;
             operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
         }
         
@@ -489,6 +491,15 @@ namespace storm {
             return *this;
         }
 
+        bool FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired() const {
+            return multiObjectiveFormulaAtTopLevelRequired;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired(bool newValue) {
+            multiObjectiveFormulaAtTopLevelRequired = newValue;
+            return *this;
+        }
+
         bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const {
             return operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
         }

src/storm/logic/FragmentSpecification.h

@@ -118,6 +118,9 @@ namespace storm {
             bool isOperatorAtTopLevelRequired() const;
             FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue);
             
+            bool isMultiObjectiveFormulaAtTopLevelRequired() const;
+            FragmentSpecification& setMultiObjectiveFormulaAtTopLevelRequired(bool newValue);
+            
             bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const;
             FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue);
             
@@ -170,6 +173,7 @@ namespace storm {
             bool quantitativeOperatorResults;
             bool qualitativeOperatorResults;
             bool operatorAtTopLevelRequired;
+            bool multiObjectiveFormulaAtTopLevelRequired;
             bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
         };
         

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -39,8 +39,8 @@ namespace storm {
             } else {
                 // Check whether we consider a multi-objective formula
                 // For multi-objective model checking, each initial state  requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states.
-                if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+                if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
                 return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
             }
         }

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -48,8 +48,8 @@ namespace storm {
             } else {
                 // Check whether we consider a multi-objective formula
                 // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states.
-                if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
-                if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
+                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+                if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
                 return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
             }
         }