first steps

Former-commit-id: 12d930813b

src/logic/EventuallyFormula.cpp

@@ -11,6 +11,10 @@ namespace storm {
         }
         
         bool EventuallyFormula::isEventuallyFormula() const {
+            return true;
+        }
+        
+        bool EventuallyFormula::isReachabilityProbabilityFormula() const {
             return context == FormulaContext::Probability;
         }
         
@@ -18,7 +22,7 @@ namespace storm {
             return context == FormulaContext::Reward;
         }
         
-        bool EventuallyFormula::isReachbilityExpectedTimeFormula() const {
+        bool EventuallyFormula::isReachabilityExpectedTimeFormula() const {
             return context == FormulaContext::ExpectedTime;
         }
         
@@ -31,7 +35,7 @@ namespace storm {
         }
         
         bool EventuallyFormula::isExpectedTimePathFormula() const {
-            return this->isReachbilityExpectedTimeFormula();
+            return this->isReachabilityExpectedTimeFormula();
         }
         
         boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {

src/logic/EventuallyFormula.h

@@ -15,8 +15,9 @@ namespace storm {
             }
             
             virtual bool isEventuallyFormula() const override;
+            virtual bool isReachabilityProbabilityFormula() const override;
             virtual bool isReachabilityRewardFormula() const override;
-            virtual bool isReachbilityExpectedTimeFormula() const override;
+            virtual bool isReachabilityExpectedTimeFormula() const override;
             virtual bool isProbabilityPathFormula() const override;
             virtual bool isRewardPathFormula() const override;
             virtual bool isExpectedTimePathFormula() const override;

src/logic/ExpectedTimeOperatorFormula.cpp

@@ -2,22 +2,13 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
-            // Intentionally left empty.
+        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
+            STORM_LOG_THROW(this->getMeasureType() == MeasureType::Expectation || this->getMeasureType() == MeasureType::Variance, storm::exceptions::InvalidPropertyException, "Invalid measure type in ET-operator.");
         }
         
         bool ExpectedTimeOperatorFormula::isExpectedTimeOperatorFormula() const {
@@ -28,12 +19,8 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
-        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
         std::shared_ptr<Formula> ExpectedTimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ExpectedTimeOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+            return std::make_shared<ExpectedTimeOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
         }
         
         std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const {

src/logic/ExpectedTimeOperatorFormula.h

@@ -9,11 +9,7 @@ namespace storm {
     namespace logic {
         class ExpectedTimeOperatorFormula : public OperatorFormula {
         public:
-            ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
             
             virtual ~ExpectedTimeOperatorFormula() {
                 // Intentionally left empty.

src/logic/Formula.cpp

@@ -62,6 +62,10 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isReachabilityProbabilityFormula() const {
+            return false;
+        }
+        
         bool Formula::isGloballyFormula() const {
             return false;
         }
@@ -122,7 +126,7 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isReachbilityExpectedTimeFormula() const {
+        bool Formula::isReachabilityExpectedTimeFormula() const {
             return false;
         }
         
@@ -264,6 +268,22 @@ namespace storm {
             return dynamic_cast<EventuallyFormula const&>(*this);
         }
         
+        EventuallyFormula& Formula::asReachabilityProbabilityFormula() {
+            return dynamic_cast<EventuallyFormula&>(*this);
+        }
+        
+        EventuallyFormula const& Formula::asReachabilityProbabilityFormula() const {
+            return dynamic_cast<EventuallyFormula const&>(*this);
+        }
+        
+        EventuallyFormula& Formula::asReachabilityExpectedTimeFormula() {
+            return dynamic_cast<EventuallyFormula&>(*this);
+        }
+
+        EventuallyFormula const& Formula::asReachabilityExpectedTimeFormula() const {
+            return dynamic_cast<EventuallyFormula const&>(*this);
+        }
+        
         GloballyFormula& Formula::asGloballyFormula() {
             return dynamic_cast<GloballyFormula&>(*this);
         }

src/logic/Formula.h

@@ -65,8 +65,9 @@ namespace storm {
             virtual bool isNextFormula() const;
             virtual bool isUntilFormula() const;
             virtual bool isBoundedUntilFormula() const;
-            virtual bool isEventuallyFormula() const;
             virtual bool isGloballyFormula() const;
+            virtual bool isEventuallyFormula() const;
+            virtual bool isReachabilityProbabilityFormula() const;
 
             // Reward formulas.
             virtual bool isCumulativeRewardFormula() const;
@@ -75,7 +76,7 @@ namespace storm {
             virtual bool isLongRunAverageRewardFormula() const;
             
             // Expected time formulas.
-            virtual bool isReachbilityExpectedTimeFormula() const;
+            virtual bool isReachabilityExpectedTimeFormula() const;
             
             // Type checks for abstract intermediate classes.
             virtual bool isBinaryPathFormula() const;
@@ -126,8 +127,14 @@ namespace storm {
             EventuallyFormula& asEventuallyFormula();
             EventuallyFormula const& asEventuallyFormula() const;
             
+            EventuallyFormula& asReachabilityProbabilityFormula();
+            EventuallyFormula const& asReachabilityProbabilityFormula() const;
+            
             EventuallyFormula& asReachabilityRewardFormula();
             EventuallyFormula const& asReachabilityRewardFormula() const;
+
+            EventuallyFormula& asReachabilityExpectedTimeFormula();
+            EventuallyFormula const& asReachabilityExpectedTimeFormula() const;
             
             GloballyFormula& asGloballyFormula();
             GloballyFormula const& asGloballyFormula() const;

src/logic/FragmentChecker.cpp

@@ -73,7 +73,7 @@ namespace storm {
             }
             if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) {
                 if (f.isConditionalProbabilityFormula()) {
-                    result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula();
+                    result = result && f.getSubformula().isReachabilityProbabilityFormula() && f.getConditionFormula().isReachabilityProbabilityFormula();
                 } else if (f.isConditionalRewardFormula()) {
                     result = result && f.getSubformula().isReachabilityRewardFormula() && f.getConditionFormula().isEventuallyFormula();
                 }
@@ -91,15 +91,15 @@ namespace storm {
         boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = true;
-            if (f.isEventuallyFormula()) {
-                result = inherited.getSpecification().areEventuallyFormulasAllowed();
+            if (f.isReachabilityProbabilityFormula()) {
+                result = inherited.getSpecification().areReachabilityProbabilityFormulasAllowed();
                 if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
                     result = result && !f.getSubformula().isPathFormula();
                 }
             } else if (f.isReachabilityRewardFormula()) {
                 result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed();
                 result = result && f.getSubformula().isStateFormula();
-            } else if (f.isReachbilityExpectedTimeFormula()) {
+            } else if (f.isReachabilityExpectedTimeFormula()) {
                 result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed();
                 result = result && f.getSubformula().isStateFormula();
             }
@@ -111,6 +111,7 @@ namespace storm {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed();
             result = result && f.getSubformula().isExpectedTimePathFormula();
+            result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == MeasureType::Expectation);
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
             } else {
@@ -177,6 +178,7 @@ namespace storm {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areRewardOperatorsAllowed();
             result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula());
+            result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == MeasureType::Expectation);
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
             } else {

src/logic/FragmentSpecification.cpp

@@ -22,7 +22,7 @@ namespace storm {
             
             pctl.setProbabilityOperatorsAllowed(true);
             pctl.setGloballyFormulasAllowed(true);
-            pctl.setEventuallyFormulasAllowed(true);
+            pctl.setReachabilityProbabilityFormulasAllowed(true);
             pctl.setNextFormulasAllowed(true);
             pctl.setUntilFormulasAllowed(true);
             pctl.setBoundedUntilFormulasAllowed(true);
@@ -70,7 +70,7 @@ namespace storm {
             longRunAverageOperator = false;
             
             globallyFormula = false;
-            eventuallyFormula = false;
+            reachabilityProbabilityFormula = false;
             nextFormula = false;
             untilFormula = false;
             boundedUntilFormula = false;
@@ -96,6 +96,7 @@ namespace storm {
             onlyEventuallyFormuluasInConditionalFormulas = true;
             stepBoundedUntilFormulas = false;
             timeBoundedUntilFormulas = false;
+            varianceAsMeasureType = false;
         }
         
         FragmentSpecification FragmentSpecification::copy() const {
@@ -147,12 +148,12 @@ namespace storm {
             return *this;
         }
         
-        bool FragmentSpecification::areEventuallyFormulasAllowed() const {
-            return eventuallyFormula;
+        bool FragmentSpecification::areReachabilityProbabilityFormulasAllowed() const {
+            return reachabilityProbabilityFormula;
         }
         
-        FragmentSpecification& FragmentSpecification::setEventuallyFormulasAllowed(bool newValue) {
-            this->eventuallyFormula = newValue;
+        FragmentSpecification& FragmentSpecification::setReachabilityProbabilityFormulasAllowed(bool newValue) {
+            this->reachabilityProbabilityFormula = newValue;
             return *this;
         }
         
@@ -355,5 +356,14 @@ namespace storm {
             return *this;
         }
         
+        bool FragmentSpecification::isVarianceMeasureTypeAllowed() const {
+            return varianceAsMeasureType;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setVarianceMeasureTypeAllowed(bool newValue) {
+            this->varianceAsMeasureType = newValue;
+            return *this;
+        }
+        
     }
 }

src/logic/FragmentSpecification.h

@@ -28,8 +28,8 @@ namespace storm {
             bool areGloballyFormulasAllowed() const;
             FragmentSpecification& setGloballyFormulasAllowed(bool newValue);
 
-            bool areEventuallyFormulasAllowed() const;
-            FragmentSpecification& setEventuallyFormulasAllowed(bool newValue);
+            bool areReachabilityProbabilityFormulasAllowed() const;
+            FragmentSpecification& setReachabilityProbabilityFormulasAllowed(bool newValue);
 
             bool areNextFormulasAllowed() const;
             FragmentSpecification& setNextFormulasAllowed(bool newValue);
@@ -91,6 +91,9 @@ namespace storm {
             bool areTimeBoundedUntilFormulasAllowed() const;
             FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue);
             
+            bool isVarianceMeasureTypeAllowed() const;
+            FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue);
+            
             FragmentSpecification& setOperatorsAllowed(bool newValue);
             FragmentSpecification& setExpectedTimeAllowed(bool newValue);
             FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
@@ -103,7 +106,7 @@ namespace storm {
             bool longRunAverageOperator;
             
             bool globallyFormula;
-            bool eventuallyFormula;
+            bool reachabilityProbabilityFormula;
             bool nextFormula;
             bool untilFormula;
             bool boundedUntilFormula;
@@ -130,6 +133,7 @@ namespace storm {
             bool onlyEventuallyFormuluasInConditionalFormulas;
             bool stepBoundedUntilFormulas;
             bool timeBoundedUntilFormulas;
+            bool varianceAsMeasureType;
         };
         
         // Propositional.

src/logic/LongRunAverageOperatorFormula.cpp

@@ -2,24 +2,15 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
-            // Intentionally left empty.
+        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
+            STORM_LOG_THROW(this->getMeasureType() == MeasureType::Value, storm::exceptions::InvalidPropertyException, "Invalid measure type in LRA-operator.");
         }
         
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
-            // Intentionally left empty.
-        }
-                
         bool LongRunAverageOperatorFormula::isLongRunAverageOperatorFormula() const {
             return true;
         }
@@ -28,12 +19,8 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
-        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
         std::shared_ptr<Formula> LongRunAverageOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<LongRunAverageOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+            return std::make_shared<LongRunAverageOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
         }
         
         std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const {

src/logic/LongRunAverageOperatorFormula.h

@@ -7,11 +7,7 @@ namespace storm {
     namespace logic {
         class LongRunAverageOperatorFormula : public OperatorFormula {
         public:
-            LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            LongRunAverageOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
             
             virtual ~LongRunAverageOperatorFormula() {
                 // Intentionally left empty.

src/logic/OperatorFormula.cpp

@@ -2,44 +2,67 @@
 
 namespace storm {
     namespace logic {
-        OperatorFormula::OperatorFormula(boost::optional<storm::solver::OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : UnaryStateFormula(subformula), bound(bound), optimalityType(optimalityType) {
+        std::ostream& operator<<(std::ostream& out, MeasureType const& type) {
+            switch (type) {
+                case MeasureType::Value:
+                    out << "val";
+                    break;
+                case MeasureType::Expectation:
+                    out << "exp";
+                    break;
+                case MeasureType::Variance:
+                    out << "var";
+                    break;
+            }
+            return out;
+        }
+        
+        OperatorInformation::OperatorInformation(MeasureType const& measureType, boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection, boost::optional<Bound<double>> const& bound) : measureType(measureType), optimalityType(optimizationDirection), bound(bound) {
+            // Intentionally left empty.
+        }
+        
+        OperatorFormula::OperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : UnaryStateFormula(subformula), operatorInformation(operatorInformation) {
             // Intentionally left empty.
         }
         
         bool OperatorFormula::hasBound() const {
-            return static_cast<bool>(bound);
+            return static_cast<bool>(operatorInformation.bound);
         }
         
         ComparisonType OperatorFormula::getComparisonType() const {
-            return bound.get().comparisonType;
+            return operatorInformation.bound.get().comparisonType;
         }
         
         void OperatorFormula::setComparisonType(ComparisonType newComparisonType) {
-            bound.get().comparisonType = newComparisonType;
+            operatorInformation.bound.get().comparisonType = newComparisonType;
         }
         
         double OperatorFormula::getThreshold() const {
-            return bound.get().threshold;
+            return operatorInformation.bound.get().threshold;
         }
         
         void OperatorFormula::setThreshold(double newThreshold) {
-            bound.get().threshold = newThreshold;
+            operatorInformation.bound.get().threshold = newThreshold;
         }
         
         Bound<double> const& OperatorFormula::getBound() const {
-            return bound.get();
+            return operatorInformation.bound.get();
         }
         
         void OperatorFormula::setBound(Bound<double> const& newBound) {
-            bound = newBound;
+            operatorInformation.bound = newBound;
         }
         
         bool OperatorFormula::hasOptimalityType() const {
-            return static_cast<bool>(optimalityType);
+            return static_cast<bool>(operatorInformation.optimalityType);
         }
         
         OptimizationDirection const& OperatorFormula::getOptimalityType() const {
-            return optimalityType.get();
+            return operatorInformation.optimalityType.get();
+        }
+        
+        MeasureType OperatorFormula::getMeasureType() const {
+            return operatorInformation.measureType;
         }
         
         bool OperatorFormula::isOperatorFormula() const {
@@ -47,6 +70,7 @@ namespace storm {
         }
         
         std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {
+            out << "[" << this->operatorInformation.measureType << "]";
             if (hasOptimalityType()) {
                 out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max");
             }

src/logic/OperatorFormula.h

@@ -9,14 +9,27 @@
 
 namespace storm {
     namespace logic {
+        enum class MeasureType { Value, Expectation, Variance };
+        
+        std::ostream& operator<<(std::ostream& out, MeasureType const& type);
+        
+        struct OperatorInformation {
+            OperatorInformation(MeasureType const& measureType = MeasureType::Value, boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<double>> const& bound = boost::none);
+
+            MeasureType measureType;
+            boost::optional<storm::solver::OptimizationDirection> optimalityType;
+            boost::optional<Bound<double>> bound;
+        };
+        
         class OperatorFormula : public UnaryStateFormula {
         public:
-            OperatorFormula(boost::optional<storm::solver::OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            OperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
             
             virtual ~OperatorFormula() {
                 // Intentionally left empty.
             }
-            
+
+            // Bound-related accessors.
             bool hasBound() const;
             ComparisonType getComparisonType() const;
             void setComparisonType(ComparisonType newComparisonType);
@@ -24,16 +37,19 @@ namespace storm {
             void setThreshold(double newThreshold);
             Bound<double> const& getBound() const;
             void setBound(Bound<double> const& newBound);
+            
+            // Optimality-type-related accessors.
             bool hasOptimalityType() const;
             storm::solver::OptimizationDirection const& getOptimalityType() const;
             virtual bool isOperatorFormula() const override;
             
+            // Measure-type-related accessors.
+            MeasureType getMeasureType() const;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         protected:
-            std::string operatorSymbol;
-            boost::optional<Bound<double>> bound;
-            boost::optional<storm::solver::OptimizationDirection> optimalityType;
+            OperatorInformation operatorInformation;
         };
     }
 }

src/logic/ProbabilityOperatorFormula.cpp

@@ -2,22 +2,13 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
-            // Intentionally left empty.
+        ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation) {
+            STORM_LOG_THROW(this->getMeasureType() == MeasureType::Value, storm::exceptions::InvalidPropertyException, "Invalid measure type in P-operator.");
         }
         
         bool ProbabilityOperatorFormula::isProbabilityOperatorFormula() const {
@@ -27,13 +18,9 @@ namespace storm {
         boost::any ProbabilityOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-                
-        ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {
-            // Intentionally left empty.
-        }
         
         std::shared_ptr<Formula> ProbabilityOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ProbabilityOperatorFormula>(this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+            return std::make_shared<ProbabilityOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
         }
         
         std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const {

src/logic/ProbabilityOperatorFormula.h

@@ -7,11 +7,7 @@ namespace storm {
     namespace logic {
         class ProbabilityOperatorFormula : public OperatorFormula {
         public:
-            ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            ProbabilityOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation = OperatorInformation());
 
             virtual ~ProbabilityOperatorFormula() {
                 // Intentionally left empty.

src/logic/RewardOperatorFormula.cpp

@@ -2,22 +2,13 @@
 
 #include "src/logic/FormulaVisitor.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
 namespace storm {
     namespace logic {
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) {
-            // Intentionally left empty.
-        }
-        
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional<OptimizationDirection>(optimalityType), bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional<OptimizationDirection>(optimalityType), boost::none, subformula) {
-            // Intentionally left empty.
+        RewardOperatorFormula::RewardOperatorFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<std::string> const& rewardModelName, OperatorInformation const& operatorInformation) : OperatorFormula(subformula, operatorInformation), rewardModelName(rewardModelName) {
+            STORM_LOG_THROW(this->getMeasureType() == MeasureType::Expectation || this->getMeasureType() == MeasureType::Variance, storm::exceptions::InvalidPropertyException, "Invalid measure type in R-operator.");
         }
         
         bool RewardOperatorFormula::isRewardOperatorFormula() const {
@@ -49,12 +40,8 @@ namespace storm {
             this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
-        RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula), rewardModelName(rewardModelName) {
-            // Intentionally left empty.
-        }
-        
         std::shared_ptr<Formula> RewardOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<RewardOperatorFormula>(this->rewardModelName, this->optimalityType, this->bound, this->getSubformula().substitute(substitution));
+            return std::make_shared<RewardOperatorFormula>(this->getSubformula().substitute(substitution), this->rewardModelName, this->operatorInformation);
         }
         
         std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const {

src/logic/RewardOperatorFormula.h

@@ -8,11 +8,7 @@ namespace storm {
     namespace logic {
         class RewardOperatorFormula : public OperatorFormula {
         public:
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, Bound<double> const& bound, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr<Formula const> const& subformula);
-            RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula);
+            RewardOperatorFormula(std::shared_ptr<Formula const> const& subformula, boost::optional<std::string> const& rewardModelName = boost::none, OperatorInformation const& operatorInformation = OperatorInformation());
 
             virtual ~RewardOperatorFormula() {
                 // Intentionally left empty.

src/modelchecker/AbstractModelChecker.cpp

@@ -34,8 +34,8 @@ namespace storm {
             storm::logic::Formula const& formula = checkTask.getFormula();
             if (formula.isBoundedUntilFormula()) {
                 return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(formula.asBoundedUntilFormula()));
-            } else if (formula.isEventuallyFormula()) {
-                return this->computeEventuallyProbabilities(checkTask.substituteFormula(formula.asEventuallyFormula()));
+            } else if (formula.isReachabilityProbabilityFormula()) {
+                return this->computeReachabilityProbabilities(checkTask.substituteFormula(formula.asReachabilityProbabilityFormula()));
             } else if (formula.isGloballyFormula()) {
                 return this->computeGloballyProbabilities(checkTask.substituteFormula(formula.asGloballyFormula()));
             } else if (formula.isUntilFormula()) {
@@ -56,7 +56,7 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
             storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
             return this->computeUntilProbabilities(checkTask.substituteFormula(newFormula));
@@ -81,7 +81,7 @@ namespace storm {
             } else if (rewardFormula.isInstantaneousRewardFormula()) {
                 return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
             } else if (rewardFormula.isReachabilityRewardFormula()) {
-                return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asEventuallyFormula()));
+                return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula()));
             } else if (rewardFormula.isLongRunAverageRewardFormula()) {
                 return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
             } else if (rewardFormula.isConditionalRewardFormula()) {
@@ -205,7 +205,7 @@ namespace storm {
         
 		std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(CheckTask<storm::logic::ExpectedTimeOperatorFormula> const& checkTask) {
             storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula();
-			STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+			STORM_LOG_THROW(stateFormula.getSubformula().isReachabilityExpectedTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
             std::unique_ptr<CheckResult> result = this->computeExpectedTimes(checkTask.substituteFormula(stateFormula.getSubformula().asEventuallyFormula()));
             

src/modelchecker/AbstractModelChecker.h

@@ -38,7 +38,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeProbabilities(CheckTask<storm::logic::Formula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask);

src/parser/FormulaParser.cpp

@@ -88,6 +88,18 @@ namespace storm {
             // A parser used for recognizing the optimality operators.
             optimalityOperatorStruct optimalityOperator_;
             
+            struct measureTypeStruct : qi::symbols<char, storm::logic::MeasureType> {
+                measureTypeStruct() {
+                    add
+                    ("val", storm::logic::MeasureType::Value)
+                    ("exp", storm::logic::MeasureType::Expectation)
+                    ("var", storm::logic::MeasureType::Variance);
+                }
+            };
+
+            // A parser used for recognizing the measure types.
+            measureTypeStruct measureType_;
+            
             // Parser and manager used for recognizing expressions.
             storm::parser::ExpressionParser expressionParser;
             
@@ -97,7 +109,8 @@ namespace storm {
             
             qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
             
-            qi::rule<Iterator, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>>(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+            qi::rule<Iterator, storm::logic::OperatorInformation(storm::logic::MeasureType), qi::locals<storm::logic::MeasureType, boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+            qi::rule<Iterator, storm::logic::MeasureType(), Skipper> measureType;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expectedTimeOperator;
@@ -147,11 +160,11 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
             std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::FormulaContext context) const;
-            std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
-            std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
-            std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
+            storm::logic::OperatorInformation createOperatorInformation(storm::logic::MeasureType const& measureType, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
+            std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
             std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
             std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
             
@@ -301,22 +314,25 @@ namespace storm {
             pathFormula = conditionalFormula(qi::_r1);
             pathFormula.name("path formula");
             
-            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
+            measureType = qi::lit("[") >> measureType_ >> qi::lit("]");
+            measureType.name("measure type");
+            
+            operatorInformation = qi::eps[qi::_a = qi::_r1] >> (-measureType[qi::_a = qi::_1] >> -optimalityOperator_[qi::_b = qi::_1] >> ((relationalOperator_[qi::_c = qi::_1] > qi::double_[qi::_d = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)];
             operatorInformation.name("operator information");
             
-            longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation(storm::logic::MeasureType::Value) > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             longRunAverageOperator.name("long-run average operator");
             
             rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
             rewardModelName.name("reward model name");
             
-            rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+            rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation(storm::logic::MeasureType::Expectation) > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
             rewardOperator.name("reward operator");
             
-            expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            expectedTimeOperator = (qi::lit("ET") > operatorInformation(storm::logic::MeasureType::Expectation) > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             expectedTimeOperator.name("expected time operator");
             
-            probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            probabilityOperator = (qi::lit("P") > operatorInformation(storm::logic::MeasureType::Value) > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             probabilityOperator.name("probability operator");
             
             andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
@@ -459,28 +475,28 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
         }
         
-        std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
+        storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(storm::logic::MeasureType const& measureType, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
             if (comparisonType && threshold) {
-                return std::make_pair(optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
+                return storm::logic::OperatorInformation(measureType, optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
             } else {
-                return std::make_pair(optimizationDirection, boost::none);
+                return storm::logic::OperatorInformation(measureType, optimizationDirection, boost::none);
             }
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(rewardModelName, operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(subformula, operatorInformation));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(operatorInformation.first, operatorInformation.second, subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation));
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {