Commit to switch workplace.

Former-commit-id: d828f3d255

src/storage/expressions/BaseExpression.cpp

@@ -11,6 +11,14 @@ namespace storm {
             return this->returnType;
         }
         
+        bool BaseExpression::hasNumericalReturnType() const {
+            return this->getReturnType() == ExpressionReturnType::Double || this->getReturnType() == ExpressionReturnType::Int;
+        }
+        
+        bool BaseExpression::hasBooleanReturnType() const {
+            return this->getReturnType() == ExpressionReturnType::Bool;
+        }
+        
         int_fast64_t BaseExpression::evaluateAsInt(Valuation const& evaluation) const {
             LOG_ASSERT(false, "Unable to evaluate expression as integer.");
         }
@@ -23,6 +31,10 @@ namespace storm {
             LOG_ASSERT(false, "Unable to evaluate expression as double.");
         }
         
+        bool BaseExpression::isConstant() const {
+            return false;
+        }
+
         bool BaseExpression::isTrue() const {
             return false;
         }

src/storage/expressions/BaseExpression.h

@@ -1,6 +1,7 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_BASEEXPRESSION_H_
 #define STORM_STORAGE_EXPRESSIONS_BASEEXPRESSION_H_
 
+#include <cstdint>
 #include <memory>
 #include <set>
 
@@ -13,7 +14,7 @@ namespace storm {
         /*!
          * Each node in an expression tree has a uniquely defined type from this enum.
          */
-        enum ExpressionReturnType {undefined, bool_, int_, double_};
+        enum class ExpressionReturnType {Undefined, Bool, Int, Double};
         
         /*!
          * The base class of all expression classes.
@@ -71,7 +72,7 @@ namespace storm {
              *
              * @return True iff the expression is constant.
              */
-            virtual bool isConstant() const = 0;
+            virtual bool isConstant() const;
             
             /*!
              * Checks if the expression is equal to the boolean literal true.
@@ -122,6 +123,20 @@ namespace storm {
              */
             virtual std::unique_ptr<BaseExpression> clone() const = 0;
             
+            /*!
+             * Retrieves whether the expression has a numerical return type, i.e., integer or double.
+             *
+             * @return True iff the expression has a numerical return type.
+             */
+            bool hasNumericalReturnType() const;
+            
+            /*!
+             * Retrieves whether the expression has a boolean return type.
+             *
+             * @return True iff the expression has a boolean return type.
+             */
+            bool hasBooleanReturnType() const;
+            
             /*!
              * Retrieves the return type of the expression.
              *

src/storage/expressions/BinaryBooleanFunctionExpression.cpp

@@ -10,26 +10,14 @@ namespace storm {
             return this->operatorType;
         }
         
-        BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) : BinaryExpression(other), operatorType(other.getOperatorType()) {
-            // Intentionally left empty.
-        }
-        
-        BinaryBooleanFunctionExpression& BinaryBooleanFunctionExpression::operator=(BinaryBooleanFunctionExpression const& other) {
-            if (this != &other) {
-                BinaryExpression::operator=(other);
-                this->operatorType = other.getOperatorType();
-            }
-            return *this;
-        }
-        
         bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const& valuation) const {
             bool firstOperandEvaluation = this->getFirstOperand()->evaluateAsBool(valuation);
             bool secondOperandEvaluation = this->getSecondOperand()->evaluateAsBool(valuation);
             
             bool result;
             switch (this->getOperatorType()) {
-                case AND: result = firstOperandEvaluation && secondOperandEvaluation; break;
-                case OR: result = firstOperandEvaluation || secondOperandEvaluation; break;
+                case OperatorType::And: result = firstOperandEvaluation && secondOperandEvaluation; break;
+                case OperatorType::Or: result = firstOperandEvaluation || secondOperandEvaluation; break;
             }
             
             return result;
@@ -40,7 +28,7 @@ namespace storm {
             std::unique_ptr<BaseExpression> secondOperandSimplified = this->getSecondOperand()->simplify();
             
             switch (this->getOperatorType()) {
-                case AND: if (firstOperandSimplified->isTrue()) {
+                case OperatorType::And: if (firstOperandSimplified->isTrue()) {
                     return secondOperandSimplified;
                 } else if (firstOperandSimplified->isFalse()) {
                     return firstOperandSimplified;
@@ -50,7 +38,7 @@ namespace storm {
                     return secondOperandSimplified;
                 }
                 break;
-                case OR: if (firstOperandSimplified->isTrue()) {
+                case OperatorType::Or: if (firstOperandSimplified->isTrue()) {
                     return firstOperandSimplified;
                 } else if (firstOperandSimplified->isFalse()) {
                     return secondOperandSimplified;
@@ -68,6 +56,8 @@ namespace storm {
             visitor->visit(this);
         }
         
-        virtual std::unique_ptr<BaseExpression> clone() const override;
+        std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(*this));
+        }
     }
 }

src/storage/expressions/BinaryBooleanFunctionExpression.h

@@ -10,7 +10,7 @@ namespace storm {
             /*!
              * An enum type specifying the different operators applicable.
              */
-            enum OperatorType {AND, OR};
+            enum class OperatorType {And, Or};
             
             /*!
              * Creates a binary boolean function expression with the given return type, operands and operator.
@@ -22,11 +22,9 @@ namespace storm {
              */
             BinaryBooleanFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& fistOperand, std::unique_ptr<BaseExpression>&& secondOperand, OperatorType operatorType);
             
-            // Provide custom versions of copy construction and assignment.
-            BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other);
-            BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other);
-            
-            // Create default variants of move construction/assignment and virtual destructor.
+            // Instantiate constructors and assignments with their default implementations.
+            BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) = default;
+            BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other) = default;
             BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression&&) = default;
             BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression&&) = default;
             virtual ~BinaryBooleanFunctionExpression() = default;

src/storage/expressions/BinaryNumericalFunctionExpression.cpp

@@ -9,43 +9,31 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) : BinaryExpression(other), operatorType(this->getOperatorType()) {
-            // Intentionally left empty.
-        }
-        
-        BinaryNumericalFunctionExpression& BinaryNumericalFunctionExpression::operator=(BinaryNumericalFunctionExpression const& other) {
-            if (this != &other) {
-                BinaryExpression::operator=(other);
-                this->operatorType = other.getOperatorType();
-            }
-            return *this;
-        }
-        
         int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const& valuation) const {
-            LOG_ASSERT(this->getReturnType() == ExpressionReturnType::int_, "Unable to evaluate expression as integer.");
+            LOG_ASSERT(this->getReturnType() == ExpressionReturnType::Int, "Unable to evaluate expression as integer.");
             int_fast64_t firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
             int_fast64_t secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation);
             switch (this->getOperatorType()) {
-                case PLUS: return firstOperandEvaluation + secondOperandEvaluation; break;
-                case MINUS: return firstOperandEvaluation - secondOperandEvaluation; break;
-                case TIMES: return firstOperandEvaluation * secondOperandEvaluation; break;
-                case DIVIDE: return firstOperandEvaluation / secondOperandEvaluation; break;
-                case MIN: return std::min(firstOperandEvaluation, secondOperandEvaluation); break;
-                case MAX: return std::max(firstOperandEvaluation, secondOperandEvaluation); break;
+                case OperatorType::Plus: return firstOperandEvaluation + secondOperandEvaluation; break;
+                case OperatorType::Minus: return firstOperandEvaluation - secondOperandEvaluation; break;
+                case OperatorType::Times: return firstOperandEvaluation * secondOperandEvaluation; break;
+                case OperatorType::Divide: return firstOperandEvaluation / secondOperandEvaluation; break;
+                case OperatorType::Min: return std::min(firstOperandEvaluation, secondOperandEvaluation); break;
+                case OperatorType::Max: return std::max(firstOperandEvaluation, secondOperandEvaluation); break;
             }
         }
         
         double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const& valuation) const {
-            LOG_ASSERT(this->getReturnType() == ExpressionReturnType::int_, "Unable to evaluate expression as integer.");
-            double firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
-            double secondOperandEvaluation = this->getSecondOperand()->evaluateAsInt(valuation);
+            LOG_ASSERT(this->getReturnType() == ExpressionReturnType::Double, "Unable to evaluate expression as double.");
+            double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation);
+            double secondOperandEvaluation = this->getSecondOperand()->evaluateAsDouble(valuation);
             switch (this->getOperatorType()) {
-                case PLUS: return firstOperandEvaluation + secondOperandEvaluation; break;
-                case MINUS: return firstOperandEvaluation - secondOperandEvaluation; break;
-                case TIMES: return firstOperandEvaluation * secondOperandEvaluation; break;
-                case DIVIDE: return firstOperandEvaluation / secondOperandEvaluation; break;
-                case MIN: return std::min(firstOperandEvaluation, secondOperandEvaluation); break;
-                case MAX: return std::max(firstOperandEvaluation, secondOperandEvaluation); break;
+                case OperatorType::Plus: return static_cast<double>(firstOperandEvaluation + secondOperandEvaluation); break;
+                case OperatorType::Minus: return static_cast<double>(firstOperandEvaluation - secondOperandEvaluation); break;
+                case OperatorType::Times: return static_cast<double>(firstOperandEvaluation * secondOperandEvaluation); break;
+                case OperatorType::Divide: return static_cast<double>(firstOperandEvaluation / secondOperandEvaluation); break;
+                case OperatorType::Min: return static_cast<double>(std::min(firstOperandEvaluation, secondOperandEvaluation)); break;
+                case OperatorType::Max: return static_cast<double>(std::max(firstOperandEvaluation, secondOperandEvaluation)); break;
             }
         }
         

src/storage/expressions/BinaryNumericalFunctionExpression.h

@@ -10,7 +10,7 @@ namespace storm {
             /*!
              * An enum type specifying the different operators applicable.
              */
-            enum OperatorType {PLUS, MINUS, TIMES, DIVIDE, MIN, MAX};
+            enum class OperatorType {Plus, Minus, Times, Divide, Min, Max};
             
             /*!
              * Constructs a binary numerical function expression with the given return type, operands and operator.
@@ -22,11 +22,9 @@ namespace storm {
              */
             BinaryNumericalFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& firstOperand, std::unique_ptr<BaseExpression>&& secondOperand, OperatorType operatorType);
             
-            // Provide custom versions of copy construction and assignment.
-            BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other);
-            BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other);
-            
-            // Create default variants of move construction/assignment and virtual destructor.
+            // Instantiate constructors and assignments with their default implementations.
+            BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) = default;
+            BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other) = default;
             BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression&&) = default;
             BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression&&) = default;
             virtual ~BinaryNumericalFunctionExpression() = default;

src/storage/expressions/BinaryRelationExpression.cpp

@@ -5,29 +5,17 @@ namespace storm {
         BinaryRelationExpression::BinaryRelationExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& firstOperand, std::unique_ptr<BaseExpression>&& secondOperand, RelationType relationType) : BinaryExpression(returnType, std::move(firstOperand), std::move(secondOperand)), relationType(relationType) {
             // Intentionally left empty.
         }
-        
-        BinaryRelationExpression::BinaryRelationExpression(BinaryRelationExpression const& other) : BinaryExpression(other), relationType(other.getRelationType()) {
-            // Intentionally left empty.
-        }
-        
-        BinaryRelationExpression& BinaryRelationExpression::operator=(BinaryRelationExpression const& other) {
-            if (this != &other) {
-                BinaryExpression::operator=(other);
-                this->relationType = other.getRelationType();
-            }
-            return *this;
-        }
-        
+                
         bool BinaryRelationExpression::evaluateAsBool(Valuation const& valuation) const {
             double firstOperandEvaluated = this->getFirstOperand()->evaluateAsDouble(valuation);
             double secondOperandEvaluated = this->getSecondOperand()->evaluateAsDouble(valuation);
             switch (this->getRelationType()) {
-                case EQUAL: return firstOperandEvaluated == secondOperandEvaluated; break;
-                case NOT_EQUAL: return firstOperandEvaluated != secondOperandEvaluated; break;
-                case GREATER: return firstOperandEvaluated > secondOperandEvaluated; break;
-                case GREATER_OR_EQUAL: return firstOperandEvaluated >= secondOperandEvaluated; break;
-                case LESS: return firstOperandEvaluated < secondOperandEvaluated; break;
-                case LESS_OR_EQUAL: return firstOperandEvaluated <= secondOperandEvaluated; break;
+                case RelationType::Equal: return firstOperandEvaluated == secondOperandEvaluated; break;
+                case RelationType::NotEqual: return firstOperandEvaluated != secondOperandEvaluated; break;
+                case RelationType::Greater: return firstOperandEvaluated > secondOperandEvaluated; break;
+                case RelationType::GreaterOrEqual: return firstOperandEvaluated >= secondOperandEvaluated; break;
+                case RelationType::Less: return firstOperandEvaluated < secondOperandEvaluated; break;
+                case RelationType::LessOrEqual: return firstOperandEvaluated <= secondOperandEvaluated; break;
             }
         }
         

src/storage/expressions/BinaryRelationExpression.h

@@ -10,7 +10,7 @@ namespace storm {
             /*!
              * An enum type specifying the different relations applicable.
              */
-            enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
+            enum class RelationType {Equal, NotEqual, Less, LessOrEqual, Greater, GreaterOrEqual};
             
             /*!
              * Creates a binary relation expression with the given return type, operands and relation type.
@@ -22,11 +22,9 @@ namespace storm {
              */
             BinaryRelationExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& firstOperand, std::unique_ptr<BaseExpression>&& secondOperand, RelationType relationType);
             
-            // Provide custom versions of copy construction and assignment.
-            BinaryRelationExpression(BinaryRelationExpression const& other);
-            BinaryRelationExpression& operator=(BinaryRelationExpression const& other);
-            
-            // Create default variants of move construction/assignment and virtual destructor.
+            // Instantiate constructors and assignments with their default implementations.
+            BinaryRelationExpression(BinaryRelationExpression const& other) = default;
+            BinaryRelationExpression& operator=(BinaryRelationExpression const& other) = default;
             BinaryRelationExpression(BinaryRelationExpression&&) = default;
             BinaryRelationExpression& operator=(BinaryRelationExpression&&) = default;
             virtual ~BinaryRelationExpression() = default;

src/storage/expressions/BooleanConstantExpression.cpp

@@ -2,21 +2,10 @@
 
 namespace storm {
     namespace expressions {
-        BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::bool_, constantName) {
+        BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Bool, constantName) {
             // Intentionally left empty.
         }
-        
-        BooleanConstantExpression::BooleanConstantExpression(BooleanConstantExpression const& other) : ConstantExpression(other) {
-            // Intentionally left empty.
-        }
-        
-        BooleanConstantExpression& BooleanConstantExpression::operator=(BooleanConstantExpression const& other) {
-            if (this != &other) {
-                ConstantExpression::operator=(other);
-            }
-            return *this;
-        }
-        
+                
         bool BooleanConstantExpression::evaluateAsBool(Valuation const& valuation) const {
             return valuation.getBooleanValue(this->getConstantName());
         }

src/storage/expressions/BooleanConstantExpression.h

@@ -8,18 +8,15 @@ namespace storm {
         class BooleanConstantExpression : public ConstantExpression {
         public:
             /*!
-             * Creates a boolean constant expression with the given return type and constant name.
+             * Creates a boolean constant expression with the given constant name.
              *
-             * @param returnType The return type of the expression.
              * @param constantName The name of the boolean constant associated with this expression.
              */
             BooleanConstantExpression(std::string const& constantName);
             
-            // Provide custom versions of copy construction and assignment.
-            BooleanConstantExpression(BooleanConstantExpression const& other);
-            BooleanConstantExpression& operator=(BooleanConstantExpression const& other);
-            
-            // Create default variants of move construction/assignment and virtual destructor.
+            // Instantiate constructors and assignments with their default implementations.
+            BooleanConstantExpression(BooleanConstantExpression const& other) = default;
+            BooleanConstantExpression& operator=(BooleanConstantExpression const& other) = default;
             BooleanConstantExpression(BooleanConstantExpression&&) = default;
             BooleanConstantExpression& operator=(BooleanConstantExpression&&) = default;
             virtual ~BooleanConstantExpression() = default;

src/storage/expressions/BooleanLiteralExpression.cpp

@@ -0,0 +1,49 @@
+#include "src/storage/expressions/BooleanLiteralExpression.h"
+
+namespace storm {
+    namespace expressions {
+        BooleanLiteralExpression::BooleanLiteralExpression(bool value) : value(value) {
+            // Intentionally left empty.
+        }
+        
+        bool BooleanLiteralExpression::evaluateAsBool(Valuation const& valuation) const {
+            return this->getValue();
+        }
+        
+        bool BooleanLiteralExpression::isConstant() const {
+            return true;
+        }
+        
+        bool BooleanLiteralExpression::isTrue() const {
+            return this->getValue() == true;
+        }
+        
+        bool BooleanLiteralExpression::isFalse() const {
+            return this->getValue() == false;
+        }
+        
+        std::set<std::string> BooleanLiteralExpression::getVariables() const {
+            return {};
+        }
+        
+        std::set<std::string> BooleanLiteralExpression::getConstants() const {
+            return {};
+        }
+        
+        std::unique_ptr<BaseExpression> BooleanLiteralExpression::simplify() const {
+            return this->clone();
+        }
+        
+        void BooleanLiteralExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
+        
+        std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
+        }
+        
+        bool BooleanLiteralExpression::getValue() const {
+            return this->value;
+        }
+    }
+}

src/storage/expressions/BooleanLiteralExpression.h

@@ -0,0 +1,49 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_
+#define STORM_STORAGE_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_
+
+#include "src/storage/expressions/BaseExpression.h"
+
+namespace storm {
+    namespace expressions {
+        class BooleanLiteralExpression : BaseExpression {
+        public:
+            /*!
+             * Creates a boolean literal expression with the given value.
+             *
+             * @param value The value of the boolean literal.
+             */
+            BooleanLiteralExpression(bool value);
+            
+            // Instantiate constructors and assignments with their default implementations.
+            BooleanLiteralExpression(BooleanLiteralExpression const& other) = default;
+            BooleanLiteralExpression& operator=(BooleanLiteralExpression const& other) = default;
+            BooleanLiteralExpression(BooleanLiteralExpression&&) = default;
+            BooleanLiteralExpression& operator=(BooleanLiteralExpression&&) = default;
+            virtual ~BooleanLiteralExpression() = default;
+
+            // Override base class methods.
+            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual bool isConstant() const override;
+            virtual bool isTrue() const override;
+            virtual bool isFalse() const override;
+            virtual std::set<std::string> getVariables() const override;
+            virtual std::set<std::string> getConstants() const override;
+            virtual std::unique_ptr<BaseExpression> simplify() const override;
+            virtual void accept(ExpressionVisitor* visitor) const override;
+            virtual std::unique_ptr<BaseExpression> clone() const override;
+            
+            /*!
+             * Retrieves the value of the boolean literal.
+             *
+             * @return The value of the boolean literal.
+             */
+            bool getValue() const;
+            
+        private:
+            // The value of the boolean literal.
+            bool value;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_ */

src/storage/expressions/ConstantExpression.cpp

@@ -6,30 +6,6 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        ConstantExpression::ConstantExpression(ConstantExpression const& other) : BaseExpression(other), constantName(other.getConstantName()) {
-            // Intentionally left empty.
-        }
-        
-        ConstantExpression& ConstantExpression::operator=(ConstantExpression const& other) {
-            if (this != &other) {
-                BaseExpression::operator=(other);
-                this->constantName = other.getConstantName();
-            }
-            return *this;
-        }
-        
-        bool ConstantExpression::isConstant() const {
-            return false;
-        }
-        
-        bool ConstantExpression::isTrue() const {
-            return false;
-        }
-        
-        bool ConstantExpression::isFalse() const {
-            return false;
-        }
-        
         std::set<std::string> ConstantExpression::getVariables() const {
             return std::set<std::string>();
         }

src/storage/expressions/ConstantExpression.h

@@ -15,19 +15,14 @@ namespace storm {
              */
             ConstantExpression(ExpressionReturnType returnType, std::string const& constantName);
             
-            // Provide custom versions of copy construction and assignment.
-            ConstantExpression(ConstantExpression const& other);
-            ConstantExpression& operator=(ConstantExpression const& other);
-            
-            // Create default variants of move construction/assignment and virtual destructor.
+            // Instantiate constructors and assignments with their default implementations.
+            ConstantExpression(ConstantExpression const& other) = default;
+            ConstantExpression& operator=(ConstantExpression const& other) = default;
             ConstantExpression(ConstantExpression&&) = default;
             ConstantExpression& operator=(ConstantExpression&&) = default;
             virtual ~ConstantExpression() = default;
             
             // Override base class methods.
-            virtual bool isConstant() const override;
-            virtual bool isTrue() const override;
-            virtual bool isFalse() const override;
             virtual std::set<std::string> getVariables() const override;
             virtual std::set<std::string> getConstants() const override;
             virtual std::unique_ptr<BaseExpression> simplify() const override;

src/storage/expressions/DoubleConstantExpression.cpp

@@ -2,8 +2,20 @@
 
 namespace storm {
     namespace expressions {
-        DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(ReturnType::double_, constantName) {
+        DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Double, constantName) {
             // Intentionally left empty.
         }
+        
+        double DoubleConstantExpression::evaluateAsDouble(Valuation const& valuation) const {
+            return valuation.getDoubleValue(this->getConstantName());
+        }
+        
+        std::unique_ptr<BaseExpression> DoubleConstantExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this));
+        }
+        
+        void DoubleConstantExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
     }
 }

src/storage/expressions/DoubleConstantExpression.h

@@ -7,8 +7,24 @@ namespace storm {
     namespace expressions {
         class DoubleConstantExpression : public ConstantExpression {
         public:
+            /*!
+             * Creates a double constant expression with the given constant name.
+             *
+             * @param constantName The name of the double constant associated with this expression.
+             */
             DoubleConstantExpression(std::string const& constantName);
+            
+            // Instantiate constructors and assignments with their default implementations.
+            DoubleConstantExpression(DoubleConstantExpression const& other) = default;
+            DoubleConstantExpression& operator=(DoubleConstantExpression const& other) = default;
+            DoubleConstantExpression(DoubleConstantExpression&&) = default;
+            DoubleConstantExpression& operator=(DoubleConstantExpression&&) = default;
             virtual ~DoubleConstantExpression() = default;
+            
+            // Override base class methods.
+            virtual double evaluateAsDouble(Valuation const& valuation) const;
+            virtual std::unique_ptr<BaseExpression> clone() const;
+            virtual void accept(ExpressionVisitor* visitor) const;
         };
     }
 }

src/storage/expressions/DoubleLiteralExpression.cpp

@@ -0,0 +1,41 @@
+#include "src/storage/expressions/DoubleLiteralExpression.h"
+
+namespace storm {
+    namespace expressions {
+        DoubleLiteralExpression::DoubleLiteralExpression(double value) : value(value) {
+            // Intentionally left empty.
+        }
+        
+        double DoubleLiteralExpression::evaluateAsDouble(Valuation const& valuation) const {
+            return this->getValue();
+        }
+        
+        bool DoubleLiteralExpression::isConstant() const {
+            return true;
+        }
+        
+        std::set<std::string> DoubleLiteralExpression::getVariables() const {
+            return {};
+        }
+        
+        std::set<std::string> DoubleLiteralExpression::getConstants() const {
+            return {};
+        }
+        
+        std::unique_ptr<BaseExpression> DoubleLiteralExpression::simplify() const {
+            return this->clone();
+        }
+        
+        void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
+        
+        std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
+        }
+        
+        double DoubleLiteralExpression::getValue() const {
+            return this->value;
+        }
+    }
+}

src/storage/expressions/DoubleLiteralExpression.h

@@ -0,0 +1,47 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
+#define STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
+
+#include "src/storage/expressions/BaseExpression.h"
+
+namespace storm {
+    namespace expressions {
+        class DoubleLiteralExpression : BaseExpression {
+        public:
+            /*!
+             * Creates an double literal expression with the given value.
+             *
+             * @param value The value of the double literal.
+             */
+            DoubleLiteralExpression(double value);
+            
+            // Instantiate constructors and assignments with their default implementations.
+            DoubleLiteralExpression(DoubleLiteralExpression const& other) = default;
+            DoubleLiteralExpression& operator=(DoubleLiteralExpression const& other) = default;
+            DoubleLiteralExpression(DoubleLiteralExpression&&) = default;
+            DoubleLiteralExpression& operator=(DoubleLiteralExpression&&) = default;
+            virtual ~DoubleLiteralExpression() = default;
+            
+            // Override base class methods.
+            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual bool isConstant() const override;
+            virtual std::set<std::string> getVariables() const override;
+            virtual std::set<std::string> getConstants() const override;
+            virtual std::unique_ptr<BaseExpression> simplify() const override;
+            virtual void accept(ExpressionVisitor* visitor) const override;
+            virtual std::unique_ptr<BaseExpression> clone() const override;
+            
+            /*!
+             * Retrieves the value of the double literal.
+             *
+             * @return The value of the double literal.
+             */
+            double getValue() const;
+            
+        private:
+            // The value of the double literal.
+            double value;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ */

src/storage/expressions/ExpressionVisitor.h

@@ -1,18 +1,36 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_
 #define STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_
 
-#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
-#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/storage/expressions/BooleanConstantExpression.h"
-
 namespace storm {
     namespace expressions {
+        // Forward-declare all expression classes.
+        class BinaryBooleanFunctionExpression;
+        class BinaryNumericalFunctionExpression;
+        class BinaryRelationExpression;
+        class BooleanConstantExpression;
+        class DoubleConstantExpression;
+        class IntegerConstantExpression;
+        class IntegerConstantExpression;
+        class VariableExpression;
+        class UnaryBooleanFunctionExpression;
+        class UnaryNumericalFunctionExpression;
+        class BooleanLiteralExpression;
+        class IntegerLiteralExpression;
+        class DoubleLiteralExpression;
+        
         class ExpressionVisitor {
             virtual void visit(BinaryBooleanFunctionExpression const* expression) = 0;
             virtual void visit(BinaryNumericalFunctionExpression const* expression) = 0;
             virtual void visit(BinaryRelationExpression const* expression) = 0;
             virtual void visit(BooleanConstantExpression const* expression) = 0;
+            virtual void visit(DoubleConstantExpression const* expression) = 0;
+            virtual void visit(IntegerConstantExpression const* expression) = 0;
+            virtual void visit(VariableExpression const* expression) = 0;
+            virtual void visit(UnaryBooleanFunctionExpression const* expression) = 0;
+            virtual void visit(UnaryNumericalFunctionExpression const* expression) = 0;
+            virtual void visit(BooleanLiteralExpression const* expression) = 0;
+            virtual void visit(IntegerLiteralExpression const* expression) = 0;
+            virtual void visit(DoubleLiteralExpression const* expression) = 0;
         };
     }
 }

src/storage/expressions/IntegerConstantExpression.cpp

@@ -2,8 +2,24 @@
 
 namespace storm {
     namespace expressions {
-        IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(ReturnType::int_, constantName) {
+        IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(ExpressionReturnType::Int, constantName) {
             // Intentionally left empty.
         }
+        
+        int_fast64_t IntegerConstantExpression::evaluateAsInteger(Valuation const& valuation) const {
+            return valuation.getIntegerValue(this->getConstantName());
+        }
+        
+        double IntegerConstantExpression::evaluateAsDouble(Valuation const& valuation) const {
+            return static_cast<double>(valuation.getIntegerValue(this->getConstantName()));
+        }
+        
+        std::unique_ptr<BaseExpression> IntegerConstantExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this));
+        }
+        
+        void IntegerConstantExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
     }
 }

src/storage/expressions/IntegerConstantExpression.h

@@ -1,13 +1,31 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
 #define STORM_STORAGE_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
 
+#include "src/storage/expressions/ConstantExpression.h"
+
 namespace storm {
     namespace expressions {
         class IntegerConstantExpression : public ConstantExpression {
         public:
+            /*!
+             * Creates an integer constant expression with the given constant name.
+             *
+             * @param constantName The name of the integer constant associated with this expression.
+             */
             IntegerConstantExpression(std::string const& constantName);
+            
+            // Instantiate constructors and assignments with their default implementations.
+            IntegerConstantExpression(IntegerConstantExpression const& other) = default;
+            IntegerConstantExpression& operator=(IntegerConstantExpression const& other) = default;
+            IntegerConstantExpression(IntegerConstantExpression&&) = default;
+            IntegerConstantExpression& operator=(IntegerConstantExpression&&) = default;
             virtual ~IntegerConstantExpression() = default;
             
+            // Override base class methods.
+            virtual int_fast64_t evaluateAsInteger(Valuation const& valuation) const;
+            virtual double evaluateAsDouble(Valuation const& valuation) const;
+            virtual std::unique_ptr<BaseExpression> clone() const;
+            virtual void accept(ExpressionVisitor* visitor) const;
         };
     }
 }

src/storage/expressions/IntegerLiteralExpression.cpp

@@ -0,0 +1,45 @@
+#include "src/storage/expressions/IntegerLiteralExpression.h"
+
+namespace storm {
+    namespace expressions {
+        IntegerLiteralExpression::IntegerLiteralExpression(int_fast64_t value) : value(value) {
+            // Intentionally left empty.
+        }
+        
+        int_fast64_t IntegerLiteralExpression::evaluateAsInt(Valuation const& valuation) const {
+            return this->getValue();
+        }
+        
+        double IntegerLiteralExpression::evaluateAsDouble(Valuation const& valuation) const {
+            return static_cast<double>(this->getValue());
+        }
+        
+        bool IntegerLiteralExpression::isConstant() const {
+            return true;
+        }
+        
+        std::set<std::string> IntegerLiteralExpression::getVariables() const {
+            return {};
+        }
+        
+        std::set<std::string> IntegerLiteralExpression::getConstants() const {
+            return {};
+        }
+        
+        std::unique_ptr<BaseExpression> IntegerLiteralExpression::simplify() const {
+            return this->clone();
+        }
+        
+        void IntegerLiteralExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
+        
+        std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
+        }
+        
+        int_fast64_t IntegerLiteralExpression::getValue() const {
+            return this->value;
+        }
+    }
+}

src/storage/expressions/IntegerLiteralExpression.h

@@ -0,0 +1,48 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
+#define STORM_STORAGE_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
+
+#include "src/storage/expressions/BaseExpression.h"
+
+namespace storm {
+    namespace expressions {
+        class IntegerLiteralExpression : BaseExpression {
+        public:
+            /*!
+             * Creates an integer literal expression with the given value.
+             *
+             * @param value The value of the integer literal.
+             */
+            IntegerLiteralExpression(int_fast64_t value);
+            
+            // Instantiate constructors and assignments with their default implementations.
+            IntegerLiteralExpression(IntegerLiteralExpression const& other) = default;
+            IntegerLiteralExpression& operator=(IntegerLiteralExpression const& other) = default;
+            IntegerLiteralExpression(IntegerLiteralExpression&&) = default;
+            IntegerLiteralExpression& operator=(IntegerLiteralExpression&&) = default;
+            virtual ~IntegerLiteralExpression() = default;
+            
+            // Override base class methods.
+            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
+            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual bool isConstant() const override;
+            virtual std::set<std::string> getVariables() const override;
+            virtual std::set<std::string> getConstants() const override;
+            virtual std::unique_ptr<BaseExpression> simplify() const override;
+            virtual void accept(ExpressionVisitor* visitor) const override;
+            virtual std::unique_ptr<BaseExpression> clone() const override;
+            
+            /*!
+             * Retrieves the value of the integer literal.
+             *
+             * @return The value of the integer literal.
+             */
+            int_fast64_t getValue() const;
+            
+        private:
+            // The value of the integer literal.
+            int_fast64_t value;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ */

src/storage/expressions/SimpleValuation.h

@@ -3,7 +3,6 @@
 
 #include <memory>
 #include <vector>
-#include <string>
 #include <unordered_map>
 
 #include "src/storage/expressions/Valuation.h"
@@ -12,30 +11,82 @@ namespace storm {
     namespace expressions {
         class SimpleValuation : public Valuation {
         public:
+            /*!
+             * Creates a simple valuation that can hold the given number of boolean, integer and double variables.
+             *
+             * @param booleanVariableCount The number of boolean variables in the valuation.
+             * @param integerVariableCount The number of integer variables in the valuation.
+             * @param doubleVariableCount The number of double variables in the valuation.
+             */
             SimpleValuation(std::size_t booleanVariableCount, std::size_t integerVariableCount, std::size_t doubleVariableCount);
             
+            /*!
+             * Creates a simple evaluation based on the given identifier to index map and value containers for the
+             * different types of variables.
+             *
+             * @param identifierToIndexMap A shared pointer to a mapping from identifier to their local indices in the
+             * value containers.
+             * @param booleanValues The value container for all boolean identifiers.
+             * @param integerValues The value container for all integer identifiers.
+             * @param doubleValues The value container for all double identifiers.
+             */
             SimpleValuation(std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap, std::vector<bool> booleanValues, std::vector<int_fast64_t> integerValues, std::vector<double> doubleValues);
 
+            // Instantiate some constructors and assignments with their default implementations.
             SimpleValuation() = default;
             SimpleValuation(SimpleValuation const&) = default;
             SimpleValuation(SimpleValuation&&) = default;
             SimpleValuation& operator=(SimpleValuation const&) = default;
             SimpleValuation& operator=(SimpleValuation&&) = default;
             
+            /*!
+             * Sets the index of the identifier with the given name to the given value.
+             *
+             * @param name The name of the identifier for which to set the index.
+             * @param index The new index of the identifier.
+             */
             void setIdentifierIndex(std::string const& name, uint_fast64_t index);
             
+            /*!
+             * Sets the value of the boolean identifier with the given name to the given value.
+             *
+             * @param name The name of the boolean identifier whose value to set.
+             * @param value The new value of the boolean identifier.
+             */
             void setBooleanValue(std::string const& name, bool value);
+
+            /*!
+             * Sets the value of the integer identifier with the given name to the given value.
+             *
+             * @param name The name of the integer identifier whose value to set.
+             * @param value The new value of the integer identifier.
+             */
             void setIntegerValue(std::string const& name, int_fast64_t value);
+
+            /*!
+             * Sets the value of the double identifier with the given name to the given value.
+             *
+             * @param name The name of the double identifier whose value to set.
+             * @param value The new value of the double identifier.
+             */
             void setDoubleValue(std::string const& name, double value);
             
+            // Override base class methods.
             virtual bool getBooleanValue(std::string const& name) const override;
             virtual int_fast64_t getIntegerValue(std::string const& name) const override;
             virtual double getDoubleValue(std::string const& name) const override;
             
         private:
+            // A mapping of identifiers to their local indices in the value containers.
             std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap;
+            
+            // The value container for all boolean identifiers.
             std::vector<bool> booleanValues;
+            
+            // The value container for all integer identifiers.
             std::vector<int_fast64_t> integerValues;
+            
+            // The value container for all double identifiers.
             std::vector<double> doubleValues;
         };
     }

src/storage/expressions/SubstitutionVisitor.h

@@ -10,8 +10,6 @@ namespace storm {
         public:
             template<template<typename... Arguments> class MapType>
             Expression substitute(BaseExpression const* expression, MapType<std::string, Expression> const& identifierToExpressionMap);
-            
-            
         };
     }
 }

src/storage/expressions/UnaryBooleanFunctionExpression.cpp

@@ -1,9 +1,42 @@
 #include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
+#include "src/storage/expressions/BooleanLiteralExpression.h"
 
 namespace storm {
     namespace expressions {
-        UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType) : UnaryExpression(returnType, std::move(argument)), functionType(functionType) {
+        UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType) : UnaryExpression(returnType, std::move(operand)), operatorType(operatorType) {
             // Intentionally left empty.
         }
+        
+        OperatorType UnaryBooleanFunctionExpression::getOperatorType() const {
+            return this->operatorType;
+        }
+        
+        bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const& valuation) const {
+            bool operandEvaluated = this->getOperand()->evaluateAsBool(valuation);
+            switch (this->getOperatorType()) {
+                case OperatorType::Not: return !operandEvaluated; break;
+            }
+        }
+        
+        std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::simplify() const {
+            std::unique_ptr<BaseExpression> operandSimplified = this->getOperand()->simplify();
+            switch (this->getOperatorType()) {
+                case OperatorType::Not: if (operandSimplified->isTrue()) {
+                    return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(false));
+                } else {
+                    return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(true));
+                }
+            }
+            
+            return UnaryBooleanFunctionExpression(this->getReturnType(), std::move(operandSimplified), this->getOperatorType());
+        }
+        
+        void UnaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
+        
+        std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(*this));
+        }
     }
 }

src/storage/expressions/UnaryBooleanFunctionExpression.h

@@ -1,19 +1,48 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
 #define STORM_STORAGE_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
 
+#include "src/storage/expressions/UnaryExpression.h"
+
 namespace storm {
     namespace expressions {
         class UnaryBooleanFunctionExpression : public UnaryExpression {
             /*!
              * An enum type specifying the different functions applicable.
              */
-            enum FunctionType {NOT};
+            enum class OperatorType {Not};
             
-            UnaryBooleanFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType);
+            /*!
+             * Creates a unary boolean function expression with the given return type, operand and operator.
+             *
+             * @param returnType The return type of the expression.
+             * @param operand The operand of the expression.
+             * @param operatorType The operator of the expression.
+             */
+            UnaryBooleanFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType);
+
+            // Instantiate constructors and assignments with their default implementations.
+            UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& other) = default;
+            UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression const& other) = default;
+            UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression&&) = default;
+            UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression&&) = default;
             virtual ~UnaryBooleanFunctionExpression() = default;
             
+            // Override base class methods.
+            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual std::unique_ptr<BaseExpression> simplify() const override;
+            virtual void accept(ExpressionVisitor* visitor) const override;
+            virtual std::unique_ptr<BaseExpression> clone() const override;
+
+            /*!
+             * Retrieves the operator associated with this expression.
+             *
+             * @return The operator associated with this expression.
+             */
+            OperatorType getOperatorType() const;
+            
         private:
-            FunctionType FunctionType;
+            // The operator of this expression.
+            OperatorType operatorType;
         };
     }
 }

src/storage/expressions/UnaryExpression.cpp

@@ -2,8 +2,32 @@
 
 namespace storm {
     namespace expressions {
-        UnaryExpression::UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& argument) : BaseExpression(returnType), argument(std::move(argument)) {
+        UnaryExpression::UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand) : BaseExpression(returnType), operand(std::move(operand)) {
             // Intentionally left empty.
         }
+        
+        UnaryExpression::UnaryExpression(UnaryExpression const& other) : BaseExpression(other), operand(other.getOperand()->clone()) {
+            // Intentionally left empty.
+        }
+        
+        UnaryExpression& UnaryExpression::operator=(UnaryExpression const& other) {
+            if (this != &other) {
+                BaseExpression::operator=(other);
+                this->operand = other.getOperand()->clone();
+            }
+            return *this;
+        }
+
+        bool UnaryExpression::isConstant() const {
+            return this->getOperand()->isConstant();
+        }
+        
+        std::set<std::string> UnaryExpression::getVariables() const {
+            return this->getOperand()->getVariables();
+        }
+        
+        std::set<std::string> UnaryExpression::getConstants() const {
+            return this->getOperand()->getVariables();
+        }
     }
 }

src/storage/expressions/UnaryExpression.h

@@ -1,16 +1,44 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_UNARYEXPRESSION_H_
 #define STORM_STORAGE_EXPRESSIONS_UNARYEXPRESSION_H_
 
+#include "src/storage/expressions/BaseExpression.h"
+
 namespace storm {
     namespace expressions {
         class UnaryExpression : public BaseExpression {
         public:
-            UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& argument);
+            /*!
+             * Creates a unary expression with the given return type and operand.
+             *
+             * @param returnType The return type of the expression.
+             * @param operand The operand of the unary expression.
+             */
+            UnaryExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand);
+
+            // Provide custom versions of copy construction and assignment.
+            UnaryExpression(UnaryExpression const& other);
+            UnaryExpression& operator=(UnaryExpression const& other);
+            
+            // Create default variants of move construction/assignment and virtual destructor.
+            UnaryExpression(UnaryExpression&&) = default;
+            UnaryExpression& operator=(UnaryExpression&&) = default;
             virtual ~UnaryExpression() = default;
             
-            std::unique_ptr<BaseExpression> const& getArgument() const;
+            // Override base class methods.
+            virtual bool isConstant() const override;
+            virtual std::set<std::string> getVariables() const override;
+            virtual std::set<std::string> getConstants() const override;
+            
+            /*!
+             * Retrieves the operand of the unary expression.
+             *
+             * @return The operand of the unary expression.
+             */
+            std::unique_ptr<BaseExpression> const& getOperand() const;
+            
         private:
-            std::unique_ptr<BaseExpression> argument;
+            // The operand of the unary expression.
+            std::unique_ptr<BaseExpression> operand;
         };
     }
 }

src/storage/expressions/UnaryNumericalFunctionExpression.cpp

@@ -1,9 +1,41 @@
+#include <cmath>
+
 #include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
 
 namespace storm {
     namespace expressions {
-        UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType) : UnaryExpression(returnType, std::move(argument)), functionType(functionType) {
+        UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType) : UnaryExpression(returnType, std::move(operand)), operatorType(operatorType) {
             // Intentionally left empty.
         }
+        
+        int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const& valuation) const {
+            int_fast64_t operandEvaluated = this->getOperand()->evaluateAsInt(valuation);
+            switch (this->getOperatorType()) {
+                case OperatorType::Minus: return -operandEvaluated; break;
+                case OperatorType::Floor: return std::floor(operandEvaluated); break;
+                case OperatorType::Ceil: return std::ceil(operandEvaluated); break;
+            }
+        }
+        
+        double UnaryNumericalFunctionExpression::evaluateAsDouble(Valuation const& valuation) const {
+            double operandEvaluated = this->getOperand()->evaluateAsDouble(valuation);
+            switch (this->getOperatorType()) {
+                case OperatorType::Minus: return -operandEvaluated; break;
+                case OperatorType::Floor: return std::floor(operandEvaluated); break;
+                case OperatorType::Ceil: return std::ceil(operandEvaluated); break;
+            }
+        }
+        
+        std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::simplify() const {
+            return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getReturnType(), this->getOperand()->simplify(), this->getOperatorType()));
+        }
+        
+        void UnaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
+        
+        std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(*this));
+        }
     }
 }

src/storage/expressions/UnaryNumericalFunctionExpression.h

@@ -1,19 +1,49 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_UNARYNUMERICALFUNCTIONEXPRESSION_H_
 #define STORM_STORAGE_EXPRESSIONS_UNARYNUMERICALFUNCTIONEXPRESSION_H_
 
+#include "src/storage/expressions/UnaryExpression.h"
+
 namespace storm {
     namespace expressions {
         class UnaryNumericalFunctionExpression : public UnaryExpression {
             /*!
              * An enum type specifying the different functions applicable.
              */
-            enum FunctionType {MINUS, FLOOR, CEIL};
+            enum class OperatorType {Minus, Floor, Ceil};
+            
+            /*!
+             * Creates a unary numerical function expression with the given return type, operand and operator.
+             *
+             * @param returnType The return type of the expression.
+             * @param operand The operand of the expression.
+             * @param operatorType The operator of the expression.
+             */
+            UnaryNumericalFunctionExpression(ExpressionReturnType returnType, std::unique_ptr<BaseExpression>&& operand, OperatorType operatorType);
             
-            UnaryNumericalFunctionExpression(ReturnType returnType, std::unique_ptr<BaseExpression>&& argument, FunctionType functionType);
+            // Instantiate constructors and assignments with their default implementations.
+            UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& other) = default;
+            UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression const& other) = default;
+            UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression&&) = default;
+            UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression&&) = default;
             virtual ~UnaryNumericalFunctionExpression() = default;
             
+            // Override base class methods.
+            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
+            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual std::unique_ptr<BaseExpression> simplify() const override;
+            virtual void accept(ExpressionVisitor* visitor) const override;
+            virtual std::unique_ptr<BaseExpression> clone() const override;
+            
+            /*!
+             * Retrieves the operator associated with this expression.
+             *
+             * @return The operator associated with this expression.
+             */
+            OperatorType getOperatorType() const;
+            
         private:
-            FunctionType FunctionType;
+            // The operator of this expression.
+            OperatorType operatorType;
         };
     }
 }

src/storage/expressions/Valuation.h

@@ -5,10 +5,34 @@
 
 namespace storm {
     namespace expressions {
+        /*!
+         * The base class of all valuations where a valuation assigns a concrete value to all identifiers. This is, for
+         * example, used for evaluating expressions.
+         */
         class Valuation {
         public:
+            /*!
+             * Retrieves the boolean value of the identifier with the given name.
+             *
+             * @param name The name of the boolean identifier whose value to retrieve.
+             * @return The value of the boolean identifier.
+             */
             virtual bool getBooleanValue(std::string const& name) const = 0;
+            
+            /*!
+             * Retrieves the integer value of the identifier with the given name.
+             *
+             * @param name The name of the integer identifier whose value to retrieve.
+             * @return The value of the integer identifier.
+             */
             virtual int_fast64_t getIntegerValue(std::string const& name) const = 0;
+            
+            /*!
+             * Retrieves the double value of the identifier with the given name.
+             *
+             * @param name The name of the double identifier whose value to retrieve.
+             * @return The value of the double identifier.
+             */
             virtual double getDoubleValue(std::string const& name) const = 0;
         };
     }

src/storage/expressions/VariableExpression.cpp

@@ -12,47 +12,38 @@ namespace storm {
         }
         
         int_fast64_t VariableExpression::evaluateAsInt(Valuation const& evaluation) const {
-            LOG_ASSERT((this->getReturnType() == ExpressionReturnType::int_), "Cannot evaluate expression as integer: return type is not an integer.");
+            LOG_ASSERT((this->getReturnType() == ExpressionReturnType::Int), "Cannot evaluate expression as integer: return type is not an integer.");
             return evaluation.getIntegerValue(this->getVariableName());
         }
         
         bool VariableExpression::evaluateAsBool(Valuation const& evaluation) const {
-            LOG_ASSERT((this->getReturnType() == ExpressionReturnType::bool_), "Cannot evaluate expression as integer: return type is not a boolean.");
+            LOG_ASSERT((this->getReturnType() == ExpressionReturnType::Bool), "Cannot evaluate expression as integer: return type is not a boolean.");
             return evaluation.getBooleanValue(this->getVariableName());
         }
         
         double VariableExpression::evaluateAsDouble(Valuation const& evaluation) const {
-            LOG_ASSERT((this->getReturnType() == ExpressionReturnType::double_), "Cannot evaluate expression as integer: return type is not a double.");
+            LOG_ASSERT((this->getReturnType() == ExpressionReturnType::Double), "Cannot evaluate expression as integer: return type is not a double.");
             return evaluation.getDoubleValue(this->getVariableName());
         }
         
-        std::unique_ptr<BaseExpression> VariableExpression::operator+(BaseExpression const& other) const {
-            // FIXME
-            return nullptr;
+        std::set<std::string> VariableExpression::getVariables() const {
+            return {this->getVariableName()};
         }
         
-        std::unique_ptr<BaseExpression> operator-(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> operator-() const;
-        std::unique_ptr<BaseExpression> operator*(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> operator/(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> operator&(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> operator|(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> operator~() const;
+        std::set<std::string> VariableExpression::getConstants() const {
+            return std::set<std::string>();
+        }
         
-        std::unique_ptr<BaseExpression> equals(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> notEquals(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> greater(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> greaterOrEqual(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> less(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> lessOrEqual(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> minimum(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> maximum(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> mod(BaseExpression const& other) const;
-        std::unique_ptr<BaseExpression> floor() const;
-        std::unique_ptr<BaseExpression> ceil() const;
+        std::unique_ptr<BaseExpression> VariableExpression::simplify() const {
+            return this->clone();
+        }
         
-        void visit(ExpressionVisitor* visitor) const;
+        void VariableExpression::accept(ExpressionVisitor* visitor) const {
+            visitor->visit(this);
+        }
         
-        virtual std::unique_ptr<BaseExpression> clonse() const;
+        std::unique_ptr<BaseExpression> VariableExpression::clone() const {
+            return std::unique_ptr<BaseExpression>(new VariableExpression(*this));
+        }
     }
 }

src/storage/expressions/VariableExpression.h

@@ -7,40 +7,33 @@ namespace storm {
     namespace expressions {
         class VariableExpression : public BaseExpression {
             VariableExpression(ExpressionReturnType returnType, std::string const& variableName);
-            virtual ~VariableExpression() = default;
             
+            // Instantiate constructors and assignments with their default implementations.
+            VariableExpression(VariableExpression const&) = default;
+            VariableExpression(VariableExpression&&) = default;
+            VariableExpression& operator=(VariableExpression const&) = default;
+            VariableExpression& operator=(VariableExpression&&) = default;
+            virtual ~VariableExpression() = default;
+
+            // Override base class methods.
+            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
+            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual std::set<std::string> getVariables() const override;
+            virtual std::set<std::string> getConstants() const override;
+            virtual std::unique_ptr<BaseExpression> simplify() const override;
+            virtual void accept(ExpressionVisitor* visitor) const override;
+            virtual std::unique_ptr<BaseExpression> clone() const override;
+
+            /*!
+             * Retrieves the name of the variable associated with this expression.
+             *
+             * @return The name of the variable.
+             */
             std::string const& getVariableName() const;
-            
-            virtual int_fast64_t evaluateAsInt(Valuation const& evaluation) const;
-            virtual bool evaluateAsBool(Valuation const& evaluation) const;
-            virtual double evaluateAsDouble(Valuation const& evaluation) const;
-            
-            virtual std::unique_ptr<BaseExpression> operator+(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> operator-(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> operator-() const;
-            virtual std::unique_ptr<BaseExpression> operator*(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> operator/(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> operator&(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> operator|(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> operator~() const;
-            
-            virtual std::unique_ptr<BaseExpression> equals(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> notEquals(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> greater(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> greaterOrEqual(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> less(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> lessOrEqual(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> minimum(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> maximum(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> mod(BaseExpression const& other) const;
-            virtual std::unique_ptr<BaseExpression> floor() const;
-            virtual std::unique_ptr<BaseExpression> ceil() const;
-            
-            virtual void visit(ExpressionVisitor* visitor) const;
-            
-            virtual std::unique_ptr<BaseExpression> clonse() const;
-            
+
         private:
+            // The variable name associated with this expression.
             std::string variableName;
         };
     }