Added support for multi objective formulas

Former-commit-id: 3d98b71049

src/logic/CloneVisitor.cpp

@@ -76,6 +76,14 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f));
         }
         
+        boost::any CloneVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+            std::vector<std::shared_ptr<Formula const>> subformulas;
+            for(uint_fast64_t index = 0; index < f.getNumberOfSubformulas(); ++index){
+                subformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula(index).accept(*this, data)));
+            }
+            return std::static_pointer_cast<Formula>(std::make_shared<MultiObjectiveFormula>(subformulas));
+        }
+        
         boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const {
             std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
             return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(subformula));

src/logic/CloneVisitor.h

@@ -25,6 +25,7 @@ namespace storm {
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;

src/logic/Formula.cpp

@@ -17,6 +17,10 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isMultiObjectiveFormula() const {
+            return false;
+        }
+        
         bool Formula::isBinaryStateFormula() const {
             return false;
         }
@@ -183,6 +187,14 @@ namespace storm {
             return dynamic_cast<StateFormula const&>(*this);
         }
         
+        MultiObjectiveFormula& Formula::asMultiObjectiveFormula() {
+            return dynamic_cast<MultiObjectiveFormula&>(*this);
+        }
+        
+        MultiObjectiveFormula const& Formula::asMultiObjectiveFormula() const {
+            return dynamic_cast<MultiObjectiveFormula const&>(*this);
+        }
+        
         BinaryStateFormula& Formula::asBinaryStateFormula() {
             return dynamic_cast<BinaryStateFormula&>(*this);
         }

src/logic/Formula.h

@@ -46,6 +46,8 @@ namespace storm {
 
             virtual bool isBinaryBooleanStateFormula() const;
             virtual bool isUnaryBooleanStateFormula() const;
+            
+            virtual bool isMultiObjectiveFormula() const;
 
             // Operator formulas.
             virtual bool isOperatorFormula() const;
@@ -101,6 +103,9 @@ namespace storm {
             StateFormula& asStateFormula();
             StateFormula const& asStateFormula() const;
             
+            MultiObjectiveFormula& asMultiObjectiveFormula();
+            MultiObjectiveFormula const& asMultiObjectiveFormula() const;
+            
             BinaryStateFormula& asBinaryStateFormula();
             BinaryStateFormula const& asBinaryStateFormula() const;
             

src/logic/FormulaInformationVisitor.cpp

@@ -61,6 +61,14 @@ namespace storm {
             return FormulaInformation();
         }
         
+        boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+            FormulaInformation result;
+            for(uint_fast64_t index = 0; index < f.getNumberOfSubformulas(); ++index){
+                result.join(boost::any_cast<FormulaInformation>(f.getSubformula(index).accept(*this)));
+            }
+            return result;
+        }
+        
         boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {
             return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).setContainsNextFormula();
         }

src/logic/FormulaInformationVisitor.h

@@ -24,6 +24,7 @@ namespace storm {
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;

src/logic/FormulaVisitor.h

@@ -23,6 +23,7 @@ namespace storm {
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(NextFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0;

src/logic/Formulas.h

@@ -18,6 +18,7 @@
 #include "src/logic/RewardOperatorFormula.h"
 #include "src/logic/StateFormula.h"
 #include "src/logic/LongRunAverageOperatorFormula.h"
+#include "src/logic/MultiObjectiveFormula.h"
 #include "src/logic/TimeOperatorFormula.h"
 #include "src/logic/UnaryBooleanStateFormula.h"
 #include "src/logic/UnaryPathFormula.h"

src/logic/FormulasForwardDeclarations.h

@@ -20,6 +20,7 @@ namespace storm {
         class InstantaneousRewardFormula;
         class LongRunAverageOperatorFormula;
         class LongRunAverageRewardFormula;
+        class MultiObjectiveFormula;
         class NextFormula;
         class OperatorFormula;
         class PathFormula;

src/logic/FragmentChecker.cpp

@@ -159,6 +159,21 @@ namespace storm {
             return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed();
         }
         
+        boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            
+            FragmentSpecification subFormulaFragment(inherited.getSpecification());
+            if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){
+                subFormulaFragment.setMultiObjectiveFormulasAllowed(false);
+            }
+            
+            bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed();
+            for(uint_fast64_t index = 0; index<f.getNumberOfSubformulas(); ++index){
+                result = result && boost::any_cast<bool>(f.getSubformula(index).accept(*this, InheritedInformation(subFormulaFragment)));
+            }
+            return result;
+        }
+        
         boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areNextFormulasAllowed();

src/logic/FragmentChecker.h

@@ -25,6 +25,7 @@ namespace storm {
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;

src/logic/FragmentSpecification.cpp

@@ -83,12 +83,31 @@ namespace storm {
             return csrl;
         }
         
+        FragmentSpecification multiObjective() {
+            FragmentSpecification multiObjective = propositional();
+            
+            multiObjective.setMultiObjectiveFormulasAllowed(true);
+            multiObjective.setProbabilityOperatorsAllowed(true);
+            multiObjective.setUntilFormulasAllowed(true);
+            multiObjective.setReachabilityProbabilityFormulasAllowed(true);
+            multiObjective.setRewardOperatorsAllowed(true);
+            multiObjective.setReachabilityRewardFormulasAllowed(true);
+            multiObjective.setBoundedUntilFormulasAllowed(true);
+            multiObjective.setStepBoundedUntilFormulasAllowed(true);
+            // multiObjective.setTimeBoundedUntilFormulasAllowed(true); //probably better to activate this only when an MA is given...
+            multiObjective.setNestedOperatorsAllowed(false);
+
+            return multiObjective;
+        }
+        
         FragmentSpecification::FragmentSpecification() {
             probabilityOperator = false;
             rewardOperator = false;
             expectedTimeOperator = false;
             longRunAverageOperator = false;
             
+            multiObjectiveFormula = false;
+            
             globallyFormula = false;
             reachabilityProbabilityFormula = false;
             nextFormula = false;
@@ -113,6 +132,7 @@ namespace storm {
             
             nestedOperators = true;
             nestedPathFormulas = false;
+            setNestedMultiObjectiveFormulasAllowed(false);
             onlyEventuallyFormuluasInConditionalFormulas = true;
             stepBoundedUntilFormulas = false;
             timeBoundedUntilFormulas = false;
@@ -164,6 +184,15 @@ namespace storm {
             return *this;
         }
         
+        bool FragmentSpecification::areMultiObjectiveFormulasAllowed() const {
+            return multiObjectiveFormula;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulasAllowed( bool newValue) {
+            this->multiObjectiveFormula = newValue;
+            return *this;
+        }
+        
         bool FragmentSpecification::areGloballyFormulasAllowed() const {
             return globallyFormula;
         }
@@ -334,6 +363,15 @@ namespace storm {
             this->nestedPathFormulas = newValue;
             return *this;
         }
+        
+        bool FragmentSpecification::areNestedMultiObjectiveFormulasAllowed() const {
+            return this->nestedMultiObjectiveFormulas;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setNestedMultiObjectiveFormulasAllowed(bool newValue) {
+            this->nestedMultiObjectiveFormulas = newValue;
+            return *this;
+        }
 
         bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const {
             return this->onlyEventuallyFormuluasInConditionalFormulas;

src/logic/FragmentSpecification.h

@@ -24,6 +24,9 @@ namespace storm {
 
             bool areLongRunAverageOperatorsAllowed() const;
             FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue);
+            
+            bool areMultiObjectiveFormulasAllowed() const;
+            FragmentSpecification& setMultiObjectiveFormulasAllowed( bool newValue);
 
             bool areGloballyFormulasAllowed() const;
             FragmentSpecification& setGloballyFormulasAllowed(bool newValue);
@@ -78,10 +81,13 @@ namespace storm {
 
             bool areNestedOperatorsAllowed() const;
             FragmentSpecification& setNestedOperatorsAllowed(bool newValue);
-
+            
             bool areNestedPathFormulasAllowed() const;
             FragmentSpecification& setNestedPathFormulasAllowed(bool newValue);
             
+            bool areNestedMultiObjectiveFormulasAllowed() const;
+            FragmentSpecification& setNestedMultiObjectiveFormulasAllowed(bool newValue);
+            
             bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const;
             FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue);
 
@@ -114,6 +120,8 @@ namespace storm {
             bool expectedTimeOperator;
             bool longRunAverageOperator;
             
+            bool multiObjectiveFormula;
+            
             bool globallyFormula;
             bool reachabilityProbabilityFormula;
             bool nextFormula;
@@ -139,6 +147,7 @@ namespace storm {
             // Members that indicate certain restrictions.
             bool nestedOperators;
             bool nestedPathFormulas;
+            bool nestedMultiObjectiveFormulas;
             bool onlyEventuallyFormuluasInConditionalFormulas;
             bool stepBoundedUntilFormulas;
             bool timeBoundedUntilFormulas;
@@ -168,6 +177,9 @@ namespace storm {
         
         // CSL + cumulative, instantaneous, reachability and long-run rewards.
         FragmentSpecification csrl();
+        
+        // Multi-Objective formulas.
+        FragmentSpecification multiObjective();
 
     }
 }

src/logic/MultiObjectiveFormula.cpp

@@ -0,0 +1,78 @@
+#include "src/logic/MultiObjectiveFormula.h"
+
+#include "src/logic/FormulaVisitor.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace logic {
+        
+        MultiObjectiveFormula::MultiObjectiveFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas) : subformulas(subformulas) {
+            //Intentionally left empty
+        }
+        
+        MultiObjectiveFormula::~MultiObjectiveFormula() {
+            //Intentionally left empty
+        }
+        
+        bool MultiObjectiveFormula::isMultiObjectiveFormula() const {
+            return true;
+        }
+        
+        bool MultiObjectiveFormula::hasQualitativeResult() const {
+            for(auto const& subformula : this->subformulas){
+                if(subformula->hasQuantitativeResult()){
+                    return false;
+                }
+            }
+            return true;
+        }
+        
+        bool MultiObjectiveFormula::hasQuantitativeResult() const {
+            return !hasQualitativeResult();
+        };
+        
+        Formula const& MultiObjectiveFormula::getSubformula(uint_fast64_t index) const {
+            STORM_LOG_THROW(index < getNumberOfSubformulas(), storm::exceptions::InvalidArgumentException, "Tried to access subformula with index " << index << " but there are only " << this->getNumberOfSubformulas() << " subformulas.");
+            return *this->subformulas[index];
+        }
+        
+        uint_fast64_t MultiObjectiveFormula::getNumberOfSubformulas() const {
+            return this->subformulas.size();
+        }
+        
+        boost::any MultiObjectiveFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        void MultiObjectiveFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            for(auto const& subformula : this->subformulas){
+                subformula->gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            }
+        }
+        
+        void MultiObjectiveFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            for(auto const& subformula : this->subformulas){
+                subformula->gatherAtomicLabelFormulas(atomicLabelFormulas);
+            }
+        }
+        
+        void MultiObjectiveFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            for(auto const& subformula : this->subformulas){
+                subformula->gatherReferencedRewardModels(referencedRewardModels);
+            }
+        }
+        
+        std::ostream& MultiObjectiveFormula::writeToStream(std::ostream &out) const {
+            out << "multi(";
+            for(uint_fast64_t index = 0; index < this->getNumberOfSubformulas(); ++index){
+                if(index>0){
+                    out << ", ";
+                }
+                this->getSubformula(index).writeToStream(out);
+            }
+            out << ")";
+            return out;
+        }
+    }
+}

src/logic/MultiObjectiveFormula.h

@@ -0,0 +1,35 @@
+#ifndef STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_
+#define STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_
+
+#include "src/logic/Formula.h"
+
+namespace storm {
+    namespace logic {
+        class MultiObjectiveFormula : public Formula {
+        public:
+            MultiObjectiveFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas);
+            
+            virtual ~MultiObjectiveFormula();
+            
+            virtual bool isMultiObjectiveFormula() const override;
+            
+            virtual bool hasQualitativeResult() const override;
+            virtual bool hasQuantitativeResult() const override;
+            
+            Formula const& getSubformula(uint_fast64_t index) const;
+            uint_fast64_t getNumberOfSubformulas() const;
+            
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+        private:
+            std::vector<std::shared_ptr<Formula const>> subformulas;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ */

src/logic/ToExpressionVisitor.cpp

@@ -82,6 +82,10 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
         }
         
+        boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
         boost::any ToExpressionVisitor::visit(NextFormula const& f, boost::any const& data) const {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
         }

src/logic/ToExpressionVisitor.h

@@ -25,6 +25,7 @@ namespace storm {
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;

src/parser/FormulaParser.cpp

@@ -36,7 +36,8 @@ namespace storm {
                     ("max", 4)
                     ("F", 5)
                     ("G", 6)
-                    ("X", 7);
+                    ("X", 7)
+                    ("multi", 8);
                 }
             };
             
@@ -144,6 +145,8 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> instantaneousRewardFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageRewardFormula;
             
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> multiObjectiveFormula;
+            
             // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
             boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
             
@@ -166,6 +169,7 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula const> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula);
             std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
             std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
+            std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
             
             // An error handler function.
             phoenix::function<SpiritErrorHandler> handler;
@@ -340,7 +344,10 @@ namespace storm {
             orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
             orStateFormula.name("or state formula");
             
-            stateFormula = (orStateFormula);
+            multiObjectiveFormula = (qi::lit("multi") > qi::lit("(") >> (stateFormula  % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiObjectiveFormula, phoenix::ref(*this), qi::_1)];
+            multiObjectiveFormula.name("Multi-objective formula");
+            
+            stateFormula = (orStateFormula | multiObjectiveFormula);
             stateFormula.name("state formula");
             
             start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
@@ -369,6 +376,7 @@ namespace storm {
             debug(rewardPathFormula);
             debug(cumulativeRewardFormula);
             debug(instantaneousRewardFormula);
+            debug(multiObjectiveFormula);
             */
 
             // Enable error reporting.
@@ -395,6 +403,7 @@ namespace storm {
             qi::on_error<qi::fail>(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(multiObjectiveFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
         }
         
         void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
@@ -519,6 +528,10 @@ namespace storm {
                 return subformula;
             }
         }
+        
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
+        }
 
     } // namespace parser
 } // namespace storm

test/functional/parser/FormulaParserTest.cpp

@@ -148,3 +148,34 @@ TEST(FormulaParserTest, WrongFormatTest) {
     input = "P>0.5 [F y!=0)]";
     EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
 }
+
+TEST(FormulaParserTest, MultiObjectiveFormulaTest) {
+    storm::parser::FormulaParser formulaParser;
+    
+    std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])";
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+    ASSERT_NO_THROW(formulas = formulaParser.parseFromString(input));
+    ASSERT_EQ(1, formulas.size());
+    ASSERT_TRUE(formulas[0]->isMultiObjectiveFormula());
+    storm::logic::MultiObjectiveFormula mof = formulas[0]->asMultiObjectiveFormula();
+    ASSERT_EQ(3, mof.getNumberOfSubformulas());
+    
+    ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula());
+    ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
+    ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
+    ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().hasBound());
+    ASSERT_EQ(0.9, mof.getSubformula(0).asProbabilityOperatorFormula().getBound().threshold);
+    
+    ASSERT_TRUE(mof.getSubformula(1).isRewardOperatorFormula());
+    ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().isEventuallyFormula());
+    ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
+    ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().hasBound());
+    ASSERT_EQ(42, mof.getSubformula(1).asRewardOperatorFormula().getBound().threshold);
+    
+    ASSERT_TRUE(mof.getSubformula(2).isProbabilityOperatorFormula());
+    ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
+    ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
+    ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().hasOptimalityType());
+    ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asProbabilityOperatorFormula().getOptimalityType()));
+
+}