Started moving IR and adjusting it to the new expression classes.

Former-commit-id: 24a182701f

CMakeLists.txt

@@ -252,10 +252,8 @@ file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJ
 file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
 file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
 file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp)
+file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp)
 file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp)
-file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp)
-file(GLOB_RECURSE STORM_IR_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.h ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.cpp)
-
 # Test Sources
 # Note that the tests also need the source files, except for the main file
 file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/functional/*.h ${STORM_CPP_TESTS_BASE_PATH}/functional/*.cpp)
@@ -274,8 +272,6 @@ source_group(formula\\csl FILES ${STORM_FORMULA_CSL_FILES})
 source_group(formula\\ltl FILES ${STORM_FORMULA_LTL_FILES})
 source_group(formula\\prctl FILES ${STORM_FORMULA_PRCTL_FILES})
 source_group(generated FILES ${STORM_BUILD_HEADERS})
-source_group(ir FILES ${STORM_IR_FILES})
-source_group(ir\\expressions FILES ${STORM_IR_EXPRESSIONS_FILES})
 source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES})
 source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES})
 source_group(models FILES ${STORM_MODELS_FILES})
@@ -286,6 +282,7 @@ source_group(solver FILES ${STORM_SOLVER_FILES})
 source_group(storage FILES ${STORM_STORAGE_FILES})
 source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES})
 source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES})
+source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES})
 source_group(utility FILES ${STORM_UTILITY_FILES})
 source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES})
 source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES})

src/ir/Assignment.cpp

@@ -1,63 +0,0 @@
-/*
- * Assignment.cpp
- *
- *  Created on: 12.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "Assignment.h"
-#include "src/parser/prismparser/VariableState.h"
-
-namespace storm {
-    namespace ir {
-        
-        Assignment::Assignment() : variableName(), expression() {
-            // Nothing to do here.
-        }
-        
-        Assignment::Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression)
-        : variableName(variableName), expression(std::move(expression)) {
-            // Nothing to do here.
-        }
-        
-        Assignment::Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
-        : variableName(oldAssignment.variableName), expression(oldAssignment.expression->clone(renaming, variableState)) {
-            auto renamingPair = renaming.find(oldAssignment.variableName);
-            if (renamingPair != renaming.end()) {
-                this->variableName = renamingPair->second;
-            }
-        }
-        
-        Assignment::Assignment(Assignment const& otherAssignment) : variableName(otherAssignment.variableName), expression() {
-            if (otherAssignment.expression != nullptr) {
-                expression = otherAssignment.expression->clone();
-            }
-        }
-        
-        Assignment& Assignment::operator=(Assignment const& otherAssignment) {
-            if (this != &otherAssignment) {
-                this->variableName = otherAssignment.variableName;
-                this->expression = otherAssignment.expression->clone();
-            }
-            
-            return *this;
-        }
-        
-        std::string const& Assignment::getVariableName() const {
-            return variableName;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
-            return expression;
-        }
-        
-        std::string Assignment::toString() const {
-            std::stringstream result;
-            result << "(" << variableName << "' = " << expression->toString() << ")";
-            return result.str();
-        }
-        
-    } // namespace ir
-} // namespace storm

src/ir/Assignment.h

@@ -1,98 +0,0 @@
-/*
- * Assignment.h
- *
- *  Created on: 06.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_ASSIGNMENT_H_
-#define STORM_IR_ASSIGNMENT_H_
-
-#include <memory>
-
-#include "expressions/BaseExpression.h"
-
-namespace storm {
-    
-    namespace parser {
-        namespace prism {
-            class VariableState;
-        } // namespace prismparser
-    } // namespace parser
-    
-    namespace ir {
-        
-        /*!
-         * A class representing the assignment of an expression to a variable.
-         */
-        class Assignment {
-        public:
-            /*!
-             * Default constructor. Creates an empty assignment.
-             */
-            Assignment();
-            
-            /*!
-             * Constructs an assignment using the given variable name and expression.
-             *
-             * @param variableName The variable that this assignment targets.
-             * @param expression The expression to assign to the variable.
-             */
-            Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression);
-            
-            /*!
-             * Creates a copy of the given assignment and performs the provided renaming.
-             *
-             * @param oldAssignment The assignment to copy.
-             * @param renaming A mapping from names that are to be renamed to the names they are to be
-             * replaced with.
-             * @param variableState An object knowing about the variables in the system.
-             */
-            Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
-            
-            /*!
-             * Performs a deep-copy of the given assignment.
-             *
-             * @param otherAssignment The assignment to copy.
-             */
-            Assignment(Assignment const& otherAssignment);
-            
-            /*!
-             * Performs a deep-copy of the given assignment and assigns it to the current one.
-             *
-             * @param otherAssignment The assignment to assign.
-             */
-            Assignment& operator=(Assignment const& otherAssignment);
-            
-            /*!
-             * Retrieves the name of the variable that this assignment targets.
-             *
-             * @return The name of the variable that this assignment targets.
-             */
-            std::string const& getVariableName() const;
-            
-            /*!
-             * Retrieves the expression that is assigned to the variable.
-             *
-             * @return The expression that is assigned to the variable.
-             */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getExpression() const;
-            
-            /*!
-             * Retrieves a string representation of this assignment.
-             * @returns a string representation of this assignment.
-             */
-            std::string toString() const;
-            
-        private:
-            // The name of the variable that this assignment targets.
-            std::string variableName;
-            
-            // The expression that is assigned to the variable.
-            std::unique_ptr<storm::ir::expressions::BaseExpression> expression;
-        };
-        
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_ASSIGNMENT_H_ */

src/ir/BooleanVariable.cpp

@@ -1,49 +0,0 @@
-/*
- * BooleanVariable.cpp
- *
- *  Created on: 12.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "BooleanVariable.h"
-#include "src/parser/prismparser/VariableState.h"
-
-namespace storm {
-    namespace ir {
-        
-        BooleanVariable::BooleanVariable() : Variable() {
-            // Nothing to do here.
-        }
-        
-        BooleanVariable::BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
-		: Variable(localIndex, globalIndex, variableName, std::move(initialValue)) {
-            // Nothing to do here.
-        }
-        
-        BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
-        : Variable(oldVariable, newName, newGlobalIndex, renaming, variableState) {
-            // Nothing to do here.
-        }
-        
-        BooleanVariable& BooleanVariable::operator=(BooleanVariable const& otherVariable) {
-            if (this != &otherVariable) {
-                Variable::operator=(otherVariable);
-            }
-            
-            return *this;
-        }
-        
-        std::string BooleanVariable::toString() const {
-            std::stringstream result;
-            result << this->getName() << ": bool";
-            if (this->getInitialValue() != nullptr) {
-                result << " init " << this->getInitialValue()->toString();
-            }
-            result << ";";
-            return result.str();
-        }
-        
-    } // namespace ir
-} // namespace storm

src/ir/BooleanVariable.h

@@ -1,70 +0,0 @@
-/*
- * BooleanVariable.h
- *
- *  Created on: 08.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_BOOLEANVARIABLE_H_
-#define STORM_IR_BOOLEANVARIABLE_H_
-
-#include <memory>
-#include <map>
-
-#include "src/ir/Variable.h"
-
-namespace storm {
-    
-    namespace parser {
-        namespace prism {
-            class VariableState;
-        } // namespace prismparser
-    } // namespace parser
-    
-    namespace ir {
-        
-        /*!
-         * A class representing a boolean variable.
-         */
-        class BooleanVariable : public Variable {
-        public:
-            /*!
-             * Default constructor. Creates a boolean variable without a name.
-             */
-            BooleanVariable();
-            
-            /*!
-             * Creates a boolean variable with the given name and the given initial value.
-             *
-             * @param localIndex A module-local unique index for the variable.
-             * @param globalIndex A globally unique index for the variable.
-             * @param variableName The name of the variable.
-             * @param initialValue The expression that defines the initial value of the variable.
-             */
-            BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
-            
-            /*!
-             * Creates a copy of the given boolean variable and performs the provided renaming.
-             *
-             * @param oldVariable The variable to copy.
-             * @param newName New name of this variable.
-             * @param newGlobalIndex The new global index of the variable.
-             * @param renaming A mapping from names that are to be renamed to the names they are to be
-             * replaced with.
-             * @param variableState An object knowing about the variables in the system.
-             */
-            BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
-            
-            BooleanVariable& operator=(BooleanVariable const& otherVariable);
-            
-            /*!
-             * Retrieves a string representation of this variable.
-             * @returns a string representation of this variable.
-             */
-            std::string toString() const;
-        };
-        
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_BOOLEANVARIABLE_H_ */

src/ir/IR.h

@@ -1,25 +0,0 @@
-/*
- * IR.h
- *
- *  Created on: 06.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_IR_H_
-#define STORM_IR_IR_H_
-
-// Bundle all headers to make it easy to include them.
-#include "expressions/Expressions.h"
-#include "Assignment.h"
-#include "Update.h"
-#include "Command.h"
-#include "Variable.h"
-#include "BooleanVariable.h"
-#include "IntegerVariable.h"
-#include "Module.h"
-#include "StateReward.h"
-#include "TransitionReward.h"
-#include "RewardModel.h"
-#include "Program.h"
-
-#endif /* STORM_IR_IR_H_ */

src/ir/IntegerVariable.cpp

@@ -1,72 +0,0 @@
-/*
- * IntegerVariable.cpp
- *
- *  Created on: 12.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-#include <iostream>
-
-#include "IntegerVariable.h"
-#include "src/parser/prismparser/VariableState.h"
-
-namespace storm {
-    namespace ir {
-        
-        IntegerVariable::IntegerVariable() : lowerBound(), upperBound() {
-            // Nothing to do here.
-        }
-        
-        IntegerVariable::IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
-        : Variable(localIndex, globalIndex, variableName, std::move(initialValue)), lowerBound(std::move(lowerBound)), upperBound(std::move(upperBound)) {
-            // Nothing to do here.
-        }
-        
-        IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
-        : Variable(oldVariable, newName, newGlobalIndex, renaming, variableState), lowerBound(oldVariable.lowerBound->clone(renaming, variableState)), upperBound(oldVariable.upperBound->clone(renaming, variableState)) {
-            // Nothing to do here.
-        }
-        
-        IntegerVariable::IntegerVariable(IntegerVariable const& otherVariable) : Variable(otherVariable.getLocalIndex(), otherVariable.getGlobalIndex(), otherVariable.getName(), nullptr), lowerBound(), upperBound() {
-            if (otherVariable.getInitialValue() != nullptr) {
-                setInitialValue(otherVariable.getInitialValue()->clone());
-            }
-            if (otherVariable.lowerBound != nullptr) {
-                lowerBound = otherVariable.lowerBound->clone();
-            }
-            if (otherVariable.upperBound != nullptr) {
-                upperBound = otherVariable.upperBound->clone();
-            }
-        }
-        
-        IntegerVariable& IntegerVariable::operator=(IntegerVariable const& otherVariable) {
-            if (this != &otherVariable) {
-                Variable::operator=(otherVariable);
-                this->lowerBound = otherVariable.lowerBound->clone();
-                this->upperBound = otherVariable.upperBound->clone();
-            }
-            
-            return *this;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getLowerBound() const {
-            return this->lowerBound;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getUpperBound() const {
-            return this->upperBound;
-        }
-        
-        std::string IntegerVariable::toString() const {
-            std::stringstream result;
-            result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
-            if (this->getInitialValue() != nullptr) {
-                result << " init " + this->getInitialValue()->toString();
-            }
-            result << ";";
-            return result.str();
-        }
-        
-    } // namespace ir
-} // namespace storm

src/ir/IntegerVariable.h

@@ -1,98 +0,0 @@
-/*
- * IntegerVariable.h
- *
- *  Created on: 08.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_INTEGERVARIABLE_H_
-#define STORM_IR_INTEGERVARIABLE_H_
-
-#include <memory>
-
-#include "src/ir/Variable.h"
-#include "expressions/BaseExpression.h"
-
-namespace storm {
-    
-    namespace parser {
-        namespace prism {
-            class VariableState;
-        } // namespace prismparser
-    } // namespace parser
-    
-    namespace ir {
-        
-        /*!
-         * A class representing an integer variable.
-         */
-        class IntegerVariable : public Variable {
-        public:
-            /*!
-             * Default constructor. Creates an integer variable without a name and lower and upper bounds.
-             */
-            IntegerVariable();
-            
-            /*!
-             * Creates a boolean variable with the given name and the given initial value.
-             *
-             * @param localIndex A module-local unique index for the variable.
-             * @param globalIndex A globally unique index for the variable.
-             * @param variableName The name of the variable.
-             * @param lowerBound the lower bound of the domain of the variable.
-             * @param upperBound the upper bound of the domain of the variable.
-             * @param initialValue the expression that defines the initial value of the variable.
-             */
-            IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
-            
-            /*!
-             * Creates a copy of the given integer variable and performs the provided renaming.
-             *
-             * @param oldVariable The variable to copy.
-             * @param newName New name of this variable.
-             * @param newGlobalIndex The new global index of the variable.
-             * @param renaming A mapping from names that are to be renamed to the names they are to be
-             * replaced with.
-             * @param variableState An object knowing about the variables in the system.
-             */
-            IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
-            
-            /*!
-             * Performs a deep-copy of the given variable.
-             *
-             * @param otherVariable The variable to copy.
-             */
-            IntegerVariable(IntegerVariable const& otherVariable);
-            
-            IntegerVariable& operator=(IntegerVariable const& otherVariable);
-            
-            /*!
-             * Retrieves the lower bound for this integer variable.
-             * @returns the lower bound for this integer variable.
-             */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getLowerBound() const;
-            
-            /*!
-             * Retrieves the upper bound for this integer variable.
-             * @returns the upper bound for this integer variable.
-             */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getUpperBound() const;
-            
-            /*!
-             * Retrieves a string representation of this variable.
-             * @returns a string representation of this variable.
-             */
-            std::string toString() const;
-            
-        private:
-            // The lower bound of the domain of the variable.
-            std::unique_ptr<storm::ir::expressions::BaseExpression> lowerBound;
-            
-            // The upper bound of the domain of the variable.
-            std::unique_ptr<storm::ir::expressions::BaseExpression> upperBound;
-        };
-        
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_INTEGERVARIABLE_H_ */

src/ir/Program.h

@@ -1,318 +0,0 @@
-/*
- * Program.h
- *
- *  Created on: 04.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_PROGRAM_H_
-#define STORM_IR_PROGRAM_H_
-
-#include <map>
-#include <vector>
-#include <memory>
-#include <set>
-#include <boost/container/flat_set.hpp>
-
-#include "expressions/BaseExpression.h"
-#include "expressions/BooleanConstantExpression.h"
-#include "expressions/IntegerConstantExpression.h"
-#include "expressions/DoubleConstantExpression.h"
-#include "Module.h"
-#include "RewardModel.h"
-
-namespace storm {
-    namespace ir {
-        
-        /*!
-         * A class representing a program.
-         */
-        class Program {
-        public:
-            
-            /*!
-             * An enum for the different model types.
-             */
-            enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP};
-            
-            /*!
-             * Default constructor. Creates an empty program.
-             */
-            Program();
-            
-            /*!
-             * Creates a program with the given model type, undefined constants, modules, rewards and labels.
-             *
-             * @param modelType The type of the model that this program gives rise to.
-             * @param booleanUndefinedConstantExpressions A map of undefined boolean constants to their
-             * expression nodes.
-             * @param integerUndefinedConstantExpressions A map of undefined integer constants to their
-             * expression nodes.
-             * @param doubleUndefinedConstantExpressions A map of undefined double constants to their
-             * expression nodes.
-             * @param globalBooleanVariables A list of global boolean variables.
-             * @param globalIntegerVariables A list of global integer variables.
-             * @param globalBooleanVariableToIndexMap A mapping from global boolean variable names to the index in the
-             * list of global boolean variables.
-             * @param globalIntegerVariableToIndexMap A mapping from global integer variable names to the index in the
-             * list of global integer variables.
-             * @param modules The modules of the program.
-             * @param rewards The reward models of the program.
-             * @param labels The labels defined for this model.
-             */
-            Program(ModelType modelType,
-                    std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
-                    std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
-                    std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
-                    std::vector<BooleanVariable> const& globalBooleanVariables,
-                    std::vector<IntegerVariable> const& globalIntegerVariables,
-                    std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap,
-                    std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap,
-                    std::vector<storm::ir::Module> const& modules,
-                    std::map<std::string, storm::ir::RewardModel> const& rewards,
-                    std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels);
-            
-            /*!
-             * Performs a deep-copy of the given program.
-             *
-             * @param otherProgram The program to copy.
-             */
-            Program(Program const& otherProgram);
-
-            /*!
-             * Performs a deep-copy of the given program and assigns it to the current one.
-             *
-             * @param otherProgram The program to assign.
-             */
-            Program& operator=(Program const& otherProgram);
-            
-            /*!
-             * Retrieves the number of modules in the program.
-             *
-             * @return The number of modules in the program.
-             */
-            uint_fast64_t getNumberOfModules() const;
-            
-            /*!
-             * Retrieves a reference to the module with the given index.
-             *
-             * @param index The index of the module to retrieve.
-             * @return The module with the given index.
-             */
-            storm::ir::Module const& getModule(uint_fast64_t index) const;
-            
-            /*!
-             * Retrieves the model type of the model.
-             *
-             * @return The type of the model.
-             */
-            ModelType getModelType() const;
-            
-            /*!
-             * Retrieves a string representation of this program.
-             *
-             * @return A string representation of this program.
-             */
-            std::string toString() const;
-            
-            /*!
-             * Retrieves a reference to the global boolean variable with the given index.
-             *
-             * @return A reference to the global boolean variable with the given index.
-             */
-            storm::ir::BooleanVariable const& getGlobalBooleanVariable(uint_fast64_t index) const;
-            
-            /*!
-             * Retrieves a reference to the global integer variable with the given index.
-             *
-             * @return A reference to the global integer variable with the given index.
-             */
-            storm::ir::IntegerVariable const& getGlobalIntegerVariable(uint_fast64_t index) const;
-            
-            /*!
-             * Retrieves the set of actions present in this module.
-             *
-             * @return The set of actions present in this module.
-             */
-            std::set<std::string> const& getActions() const;
-            
-            /*!
-             * Retrieves the indices of all modules within this program that contain commands that are labelled with the given
-             * action.
-             *
-             * @param action The name of the action the modules are supposed to possess.
-             * @return A set of indices of all matching modules.
-             */
-            std::set<uint_fast64_t> const& getModulesByAction(std::string const& action) const;
-            
-            /*!
-             * Retrieves the index of the module in which the given variable name was declared.
-             *
-             * @param variableName The name of the variable to search.
-             * @return The index of the module in which the given variable name was declared.
-             */
-            uint_fast64_t getModuleIndexForVariable(std::string const& variableName) const;
-            
-            /*!
-             * Retrieves the number of global boolean variables of the program.
-             *
-             * @return The number of global boolean variables of the program.
-             */
-            uint_fast64_t getNumberOfGlobalBooleanVariables() const;
-            
-            /*!
-             * Retrieves the number of global integer variables of the program.
-             *
-             * @return The number of global integer variables of the program.
-             */
-            uint_fast64_t getNumberOfGlobalIntegerVariables() const;
-            
-            /*!
-             * Retrieves the reward model with the given name.
-             *
-             * @param name The name of the reward model to return.
-             * @return The reward model with the given name.
-             */
-            storm::ir::RewardModel const& getRewardModel(std::string const& name) const;
-            
-            /*!
-             * Retrieves all labels that are defined by the probabilitic program.
-             *
-             * @return A set of labels that are defined in the program.
-             */
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() const;
-            
-            /*!
-             * Retrieves whether the given constant name is an undefined boolean constant of the program.
-             *
-             * @return True if the given constant name is an undefined boolean constant of the program.
-             */
-            bool hasUndefinedBooleanConstant(std::string const& constantName) const;
-            
-            /*!
-             * Retrieves the expression associated with the given undefined boolean constant.
-             *
-             * @param constantName The name of the undefined boolean constant for which to retrieve the expression.
-             * @return The expression associated with the given undefined boolean constant.
-             */
-            std::unique_ptr<storm::ir::expressions::BooleanConstantExpression> const& getUndefinedBooleanConstantExpression(std::string const& constantName) const;
-            
-            /*!
-             * Retrieves whether the given constant name is an undefined integer constant of the program.
-             *
-             * @return True if the given constant name is an undefined integer constant of the program.
-             */
-            bool hasUndefinedIntegerConstant(std::string const& constantName) const;
-            
-            /*!
-             * Retrieves the expression associated with the given undefined integer constant.
-             *
-             * @param constantName The name of the undefined integer constant for which to retrieve the expression.
-             * @return The expression associated with the given undefined integer constant.
-             */
-            std::unique_ptr<storm::ir::expressions::IntegerConstantExpression> const& getUndefinedIntegerConstantExpression(std::string const& constantName) const;
-
-            /*!
-             * Retrieves whether the given constant name is an undefined double constant of the program.
-             *
-             * @return True if the given constant name is an undefined double constant of the program.
-             */
-            bool hasUndefinedDoubleConstant(std::string const& constantName) const;
-            
-            /*!
-             * Retrieves the expression associated with the given undefined double constant.
-             *
-             * @param constantName The name of the undefined double constant for which to retrieve the expression.
-             * @return The expression associated with the given undefined double constant.
-             */
-            std::unique_ptr<storm::ir::expressions::DoubleConstantExpression> const& getUndefinedDoubleConstantExpression(std::string const& constantName) const;
-            
-            /*!
-             * Retrieves the mapping of undefined boolean constant names to their expression objects.
-             *
-             * @return The mapping of undefined boolean constant names to their expression objects.
-             */
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& getBooleanUndefinedConstantExpressionsMap() const;
-
-            /*!
-             * Retrieves the mapping of undefined integer constant names to their expression objects.
-             *
-             * @return The mapping of undefined integer constant names to their expression objects.
-             */
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& getIntegerUndefinedConstantExpressionsMap() const;
-
-            /*!
-             * Retrieves the mapping of undefined double constant names to their expression objects.
-             *
-             * @return The mapping of undefined double constant names to their expression objects.
-             */
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& getDoubleUndefinedConstantExpressionsMap() const;
-            
-            /*!
-             * Retrieves the global index of the given boolean variable.
-             *
-             * @param variableName The name of the boolean variable whose index to retrieve.
-             */
-            uint_fast64_t getGlobalIndexOfBooleanVariable(std::string const& variableName) const;
-            
-            /*!
-             * Retrieves the global index of the integer boolean variable.
-             *
-             * @param variableName The name of the integer variable whose index to retrieve.
-             */
-            uint_fast64_t getGlobalIndexOfIntegerVariable(std::string const& variableName) const;
-            
-            /*!
-             * Deletes all commands with indices not in the given set from the program.
-             *
-             * @param indexSet The set of indices for which to keep the commands.
-             */
-            void restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet);
-        private:
-            // The type of the model.
-            ModelType modelType;
-            
-            // A map of undefined boolean constants to their expression nodes.
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
-            
-            // A map of undefined integer constants to their expressions nodes.
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions;
-            
-            // A map of undefined double constants to their expressions nodes.
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
-            
-            // A list of global boolean variables.
-            std::vector<BooleanVariable> globalBooleanVariables;
-            
-            // A list of global integer variables.
-            std::vector<IntegerVariable> globalIntegerVariables;
-            
-            // A mapping from global boolean variable names to their indices.
-            std::map<std::string, uint_fast64_t> globalBooleanVariableToIndexMap;
-            
-            // A mapping from global integer variable names to their indices.
-            std::map<std::string, uint_fast64_t> globalIntegerVariableToIndexMap;
-            
-            // The modules associated with the program.
-            std::vector<storm::ir::Module> modules;
-            
-            // The reward models associated with the program.
-            std::map<std::string, storm::ir::RewardModel> rewards;
-            
-            // The labels that are defined for this model.
-            std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> labels;
-            
-            // The set of actions present in this program.
-            std::set<std::string> actions;
-            
-            // A map of actions to the set of modules containing commands labelled with this action.
-            std::map<std::string, std::set<uint_fast64_t>> actionsToModuleIndexMap;
-            
-            // A mapping from variable names to the modules in which they were declared.
-            std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
-        };
-        
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_PROGRAM_H_ */

src/ir/StateReward.cpp

@@ -1,60 +0,0 @@
-/*
- * StateReward.cpp
- *
- *  Created on: 12.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "StateReward.h"
-
-namespace storm {
-    namespace ir {
-        
-        StateReward::StateReward() : statePredicate(), rewardValue() {
-            // Nothing to do here.
-        }
-        
-        StateReward::StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) {
-            // Nothing to do here.
-        }
-        
-        StateReward::StateReward(StateReward const& otherReward) {
-            if (otherReward.statePredicate != nullptr) {
-                statePredicate = otherReward.statePredicate->clone();
-            }
-            if (otherReward.rewardValue != nullptr) {
-                rewardValue = otherReward.rewardValue->clone();
-            }
-        }
-        
-        StateReward& StateReward::operator=(StateReward const& otherReward) {
-            if (this != & otherReward) {
-                if (otherReward.statePredicate != nullptr) {
-                    this->statePredicate = otherReward.statePredicate->clone();
-                }
-                if (otherReward.rewardValue != nullptr) {
-                    this->rewardValue = otherReward.rewardValue->clone();
-                }
-            }
-            
-            return *this;
-        }
-        
-        std::string StateReward::toString() const {
-            std::stringstream result;
-            result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";";
-            return result.str();
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getStatePredicate() const {
-            return this->statePredicate;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getRewardValue() const {
-            return this->rewardValue;
-        }
-        
-    } // namespace ir
-} // namespace storm

src/ir/TransitionReward.cpp

@@ -1,65 +0,0 @@
-/*
- * TransitionReward.cpp
- *
- *  Created on: 12.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "TransitionReward.h"
-
-namespace storm {
-    namespace ir {
-        
-        TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
-            // Nothing to do here.
-        }
-        
-        TransitionReward::TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : commandName(commandName), statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) {
-            // Nothing to do here.
-        }
-        
-        TransitionReward::TransitionReward(TransitionReward const& otherReward) : commandName(otherReward.commandName), statePredicate(), rewardValue() {
-            if (otherReward.statePredicate != nullptr) {
-                statePredicate = otherReward.statePredicate->clone();
-            }
-            if (otherReward.rewardValue != nullptr) {
-                rewardValue = otherReward.rewardValue->clone();
-            }
-        }
-        
-        TransitionReward& TransitionReward::operator=(TransitionReward const& otherReward) {
-            if (this != &otherReward) {
-                this->commandName = otherReward.commandName;
-                if (otherReward.statePredicate != nullptr) {
-                    this->statePredicate = otherReward.statePredicate->clone();
-                }
-                if (otherReward.rewardValue != nullptr) {
-                    this->rewardValue = otherReward.rewardValue->clone();
-                }
-            }
-            
-            return *this;
-        }
-        
-        std::string TransitionReward::toString() const {
-            std::stringstream result;
-            result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";";
-            return result.str();
-        }
-        
-        std::string const& TransitionReward::getActionName() const {
-            return this->commandName;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getStatePredicate() const {
-            return this->statePredicate;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getRewardValue() const {
-            return this->rewardValue;
-        }
-        
-    } // namespace ir
-} // namespace storm

src/ir/Update.cpp

@@ -1,130 +0,0 @@
-/*
- * Update.cpp
- *
- *  Created on: 12.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "Update.h"
-#include "src/parser/prismparser/VariableState.h"
-#include "src/exceptions/OutOfRangeException.h"
-
-namespace storm {
-    namespace ir {
-        
-        Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments(), globalIndex() {
-            // Nothing to do here.
-        }
-        
-        Update::Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments)
-        : likelihoodExpression(std::move(likelihoodExpression)), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
-            // Nothing to do here.
-        }
-        
-        Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState) : globalIndex(newGlobalIndex) {
-            for (auto const& variableAssignmentPair : update.booleanAssignments) {
-                if (renaming.count(variableAssignmentPair.first) > 0) {
-                    this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState);
-                } else {
-                    this->booleanAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState);
-                }
-            }
-            for (auto const& variableAssignmentPair : update.integerAssignments) {
-                if (renaming.count(variableAssignmentPair.first) > 0) {
-                    this->integerAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState);
-                } else {
-                    this->integerAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState);
-                }
-            }
-            this->likelihoodExpression = update.likelihoodExpression->clone(renaming, variableState);
-        }
-        
-        Update::Update(Update const& otherUpdate) : likelihoodExpression(), booleanAssignments(otherUpdate.booleanAssignments), integerAssignments(otherUpdate.integerAssignments), globalIndex(otherUpdate.globalIndex) {
-            if (otherUpdate.likelihoodExpression != nullptr) {
-                likelihoodExpression = otherUpdate.likelihoodExpression->clone();
-            }
-        }
-        
-        Update& Update::operator=(Update const& otherUpdate) {
-            if (this != &otherUpdate) {
-                if (otherUpdate.likelihoodExpression != nullptr) {
-                    this->likelihoodExpression = otherUpdate.likelihoodExpression->clone();
-                }
-                this->booleanAssignments = otherUpdate.booleanAssignments;
-                this->integerAssignments = otherUpdate.integerAssignments;
-                this->globalIndex = otherUpdate.globalIndex;
-            }
-            
-            return *this;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
-            return likelihoodExpression;
-        }
-        
-        uint_fast64_t Update::getNumberOfBooleanAssignments() const {
-            return booleanAssignments.size();
-        }
-        
-        uint_fast64_t Update::getNumberOfIntegerAssignments() const {
-            return integerAssignments.size();
-        }
-        
-        std::map<std::string, storm::ir::Assignment> const& Update::getBooleanAssignments() const {
-            return booleanAssignments;
-        }
-        
-        std::map<std::string, storm::ir::Assignment> const& Update::getIntegerAssignments() const {
-            return integerAssignments;
-        }
-        
-        storm::ir::Assignment const& Update::getBooleanAssignment(std::string const& variableName) const {
-            auto variableAssignmentPair = booleanAssignments.find(variableName);
-            if (variableAssignmentPair == booleanAssignments.end()) {
-                throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '"
-				<< variableName << "' in update " << this->toString() << ".";
-            }
-            
-            return variableAssignmentPair->second;
-        }
-        
-        storm::ir::Assignment const& Update::getIntegerAssignment(std::string const& variableName) const {
-            auto variableAssignmentPair = integerAssignments.find(variableName);
-            if (variableAssignmentPair == integerAssignments.end()) {
-                throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '"
-				<< variableName << "' in update " << this->toString() << ".";
-            }
-            
-            return variableAssignmentPair->second;
-        }
-        
-        uint_fast64_t Update::getGlobalIndex() const {
-            return this->globalIndex;
-        }
-        
-        std::string Update::toString() const {
-            std::stringstream result;
-            result << likelihoodExpression->toString() << " : ";
-            uint_fast64_t i = 0;
-            for (auto const& assignment : booleanAssignments) {
-                result << assignment.second.toString();
-                if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) {
-                    result << " & ";
-                }
-                ++i;
-            }
-            i = 0;
-            for (auto const& assignment : integerAssignments) {
-                result << assignment.second.toString();
-                if (i < integerAssignments.size() - 1) {
-                    result << " & ";
-                }
-                ++i;
-            }
-            return result.str();
-        }
-        
-    } // namespace ir
-} // namespace storm

src/ir/Variable.cpp

@@ -1,74 +0,0 @@
-/*
- * Variable.cpp
- *
- *  Created on: 12.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-#include <map>
-#include <iostream>
-
-#include "Variable.h"
-#include "src/parser/prismparser/VariableState.h"
-
-namespace storm {
-    namespace ir {
-        
-        Variable::Variable() : localIndex(0), globalIndex(0), variableName(), initialValue() {
-            // Nothing to do here.
-        }
-        
-        Variable::Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
-        : localIndex(localIndex), globalIndex(globalIndex), variableName(variableName), initialValue(std::move(initialValue)) {
-            // Nothing to do here.
-        }
-        
-        Variable::Variable(Variable const& otherVariable) : localIndex(otherVariable.localIndex), globalIndex(otherVariable.globalIndex), variableName(otherVariable.variableName), initialValue() {
-            if (otherVariable.initialValue != nullptr) {
-                initialValue = otherVariable.initialValue->clone();
-            }
-        }
-        
-        Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
-        : localIndex(var.getLocalIndex()), globalIndex(newGlobalIndex), variableName(newName), initialValue() {
-            if (var.initialValue != nullptr) {
-                this->initialValue = var.initialValue->clone(renaming, variableState);
-            }
-        }
-        
-        Variable& Variable::operator=(Variable const& otherVariable) {
-            if (this != &otherVariable) {
-                this->localIndex = otherVariable.localIndex;
-                this->globalIndex = otherVariable.globalIndex;
-                this->variableName = otherVariable.variableName;
-                if (otherVariable.initialValue != nullptr) {
-                    this->initialValue = otherVariable.initialValue->clone();
-                }
-            }
-            
-            return *this;
-        }
-        
-        std::string const& Variable::getName() const {
-            return variableName;
-        }
-        
-        uint_fast64_t Variable::getGlobalIndex() const {
-            return globalIndex;
-        }
-        
-        uint_fast64_t Variable::getLocalIndex() const {
-            return localIndex;
-        }
-        
-        std::unique_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
-            return initialValue;
-        }
-        
-        void Variable::setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue) {
-            this->initialValue = std::move(initialValue);
-        }
-        
-    } // namespace ir
-} // namespace storm

src/ir/Variable.h

@@ -1,124 +0,0 @@
-/*
- * Variable.h
- *
- *  Created on: 06.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_VARIABLE_H_
-#define STORM_IR_VARIABLE_H_
-
-#include <string>
-#include <memory>
-
-#include "expressions/BaseExpression.h"
-
-namespace storm {
-    
-    namespace parser {
-        namespace prism {
-            class VariableState;
-        } // namespace prismparser
-    } // namespace parser
-    
-    namespace ir {
-        
-        /*!
-         * A class representing a untyped variable.
-         */
-        class Variable {
-        public:
-            /*!
-             * Default constructor. Creates an unnamed, untyped variable without initial value.
-             */
-            Variable();
-            
-            /*!
-             * Creates an untyped variable with the given name and initial value.
-             *
-             * @param localIndex A module-local index for the variable.
-             * @param globalIndex A globally unique (among the variables of equal type) index for the variable.
-             * @param variableName the name of the variable.
-             * @param initialValue the expression that defines the initial value of the variable.
-             */
-            Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
-            
-            /*!
-             * Creates a copy of the given variable and performs the provided renaming.
-             *
-             * @param oldVariable The variable to copy.
-             * @param newName New name of this variable.
-             * @param newGlobalIndex The new global index of the variable.
-             * @param renaming A mapping from names that are to be renamed to the names they are to be
-             * replaced with.
-             * @param variableState An object knowing about the variables in the system.
-             */
-            Variable(Variable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
-            
-            /*!
-             * Creates a deep-copy of the given variable.
-             *
-             * @param otherVariable The variable to copy.
-             */
-            Variable(Variable const& otherVariable);
-            
-            /*!
-             * Creates a deep-copy of the given variable and assigns it to the current one.
-             */
-            Variable& operator=(Variable const& otherVariable);
-            
-            /*!
-             * Retrieves the name of the variable.
-             *
-             * @return The name of the variable.
-             */
-            std::string const& getName() const;
-            
-            /*!
-             * Retrieves the global index of the variable, i.e. the index in all variables of equal type
-             * of all modules.
-             *
-             * @return The global index of the variable.
-             */
-            uint_fast64_t getGlobalIndex() const;
-            
-            /*!
-             * Retrieves the global index of the variable, i.e. the index in all variables of equal type in
-             * the same module.
-             *
-             * @return The local index of the variable.
-             */
-            uint_fast64_t getLocalIndex() const;
-            
-            /*!
-             * Retrieves the expression defining the initial value of the variable.
-             *
-             * @return The expression defining the initial value of the variable.
-             */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
-            
-            /*!
-             * Sets the initial value to the given expression.
-             *
-             * @param initialValue The new initial value.
-             */
-            void setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue);
-            
-        private:
-            // A unique (among the variables of equal type) index for the variable inside its module.
-            uint_fast64_t localIndex;
-
-            // A unique (among the variables of equal type) index for the variable over all modules.
-            uint_fast64_t globalIndex;
-            
-            // The name of the variable.
-            std::string variableName;
-            
-            // The expression defining the initial value of the variable.
-            std::unique_ptr<storm::ir::expressions::BaseExpression> initialValue;
-        };
-        
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_VARIABLE_H_ */

src/ir/expressions/BaseExpression.cpp

@@ -1,85 +0,0 @@
-/*
- * BaseExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include "BaseExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            BaseExpression::BaseExpression() : type(undefined) {
-                // Nothing to do here.
-            }
-            
-            BaseExpression::BaseExpression(ReturnType type) : type(type) {
-                // Nothing to do here.
-            }
-            
-            BaseExpression::BaseExpression(BaseExpression const& baseExpression) : type(baseExpression.type) {
-                // Nothing to do here.
-            }
-            
-            BaseExpression::~BaseExpression() {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> BaseExpression::substitute(std::unique_ptr<BaseExpression>&& expression, std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
-                BaseExpression* result = expression->performSubstitution(substitution);
-                
-                if (result != expression.get()) {
-                    return std::unique_ptr<BaseExpression>(result);
-                } else {
-                    return std::move(expression);
-                }
-            }
-            
-            int_fast64_t BaseExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (type != int_) {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
-                    << this->getTypeName() << "' as 'int'.";
-                }
-                throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '"
-                << this->getTypeName() << " because evaluation implementation is missing.";
-            }
-            
-            bool BaseExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (type != bool_) {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
-                    << this->getTypeName() << "' as 'bool'.";
-                }
-                throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '"
-                << this->getTypeName() << " because evaluation implementation is missing.";
-            }
-            
-            double BaseExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (type != double_ && type != int_) {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
-                    << this->getTypeName() << "' as 'double'.";
-                }
-                throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '"
-                << this->getTypeName() << " because evaluation implementation is missing.";
-            }
-            
-            std::string BaseExpression::getTypeName() const {
-                switch(type) {
-                    case bool_: return std::string("bool");
-                    case int_: return std::string("int");
-                    case double_: return std::string("double");
-                    default: return std::string("undefined");
-                }
-            }
-            
-            BaseExpression::ReturnType BaseExpression::getType() const {
-                return type;
-            }
-            
-            BaseExpression* BaseExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
-                return this;
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/BaseExpression.h

@@ -1,172 +0,0 @@
-/*
- * BaseExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_
-
-#include <string>
-#include <vector>
-#include <map>
-#include <memory>
-
-#include "src/exceptions/ExpressionEvaluationException.h"
-#include "src/exceptions/NotImplementedException.h"
-#include "ExpressionVisitor.h"
-
-namespace storm {
-    
-    // Forward-declare VariableState.
-	namespace parser {
-		namespace prism {
-			class VariableState;
-		} // namespace prismparser
-	} // namespace parser
-    
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * The base class for all expressions.
-             */
-            class BaseExpression {
-            public:
-                // Forward declare friend classes to allow access to substitute.
-                friend class BinaryExpression;
-                friend class UnaryExpression;
-
-                /*!
-                 * Each node in an expression tree has a uniquely defined type from this enum.
-                 */
-                enum ReturnType {undefined, bool_, int_, double_};
-                
-                /*!
-                 * Creates an expression with undefined type.
-                 */
-                BaseExpression();
-                
-                /*!
-                 * Creates an expression with the given type.
-                 *
-                 * @param type The type of the expression.
-                 */
-                BaseExpression(ReturnType type);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param baseExpression The expression to copy.
-                 */
-                BaseExpression(BaseExpression const& baseExpression);
-                
-                /*!
-                 * Destructor.
-                 */
-                virtual ~BaseExpression();
-                
-                /*!
-                 * Performes a deep-copy of the expression.
-                 *
-                 * @return A deep-copy of the expression.
-                 */
-                virtual std::unique_ptr<BaseExpression> clone() const = 0;
-                
-                /*!
-                 * Copies the expression tree underneath (including) the current node and performs the provided renaming.
-                 *
-                 * @param renaming A mapping from identifier names to strings they are to be replaced with.
-                 * @param variableState An object knowing about the global variable state.
-                 */
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const = 0;
-                
-                /*!
-                 * Performs the given substitution by replacing each variable in the given expression that is a key in
-                 * the map by a copy of the mapped expression.
-                 *
-                 * @param expression The expression in which to perform the substitution.
-                 * @param substitution The substitution to apply.
-                 * @return The resulting expression.
-                 */
-                static std::unique_ptr<BaseExpression> substitute(std::unique_ptr<BaseExpression>&& expression, std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution);
-                
-                /*!
-                 * Retrieves the value of the expression as an integer given the provided variable valuation.
-                 *
-                 * @param variableValues The variable valuation under which to evaluate the expression. If set to null,
-                 * constant expressions can be evaluated without variable values. However, upon encountering a variable
-                 * expression an expression is thrown, because evaluation is impossible without the variable values then.
-                 * @return The value of the expression as an integer.
-                 */
-                virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const;
-                
-                /*!
-                 * Retrieves the value of the expression as a boolean given the provided variable valuation.
-                 *
-                 * @param variableValues The variable valuation under which to evaluate the expression. If set to null,
-                 * constant expressions can be evaluated without variable values. However, upon encountering a variable
-                 * expression an expression is thrown, because evaluation is impossible without the variable values then.
-                 * @return The value of the expression as a boolean.
-                 */
-                virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const;
-                
-                /*!
-                 * Retrieves the value of the expression as a double given the provided variable valuation.
-                 *
-                 * @param variableValues The variable valuation under which to evaluate the expression. If set to null,
-                 * constant expressions can be evaluated without variable values. However, upon encountering a variable
-                 * expression an expression is thrown, because evaluation is impossible without the variable values then.
-                 * @return The value of the expression as a double.
-                 */
-                virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const;
-                
-                /*!
-                 * Acceptor method for visitor pattern.
-                 *
-                 * @param visitor The visitor that is supposed to visit each node of the expression tree.
-                 */
-                virtual void accept(ExpressionVisitor* visitor) = 0;
-                
-                /*!
-                 * Retrieves a string representation of the expression tree underneath the current node.
-                 *
-                 * @return A string representation of the expression tree underneath the current node.
-                 */
-                virtual std::string toString() const = 0;
-                
-                /*!
-                 * Retrieves a string representation of the type to which this node evaluates.
-                 *
-                 * @return A string representation of the type to which this node evaluates.
-                 */
-                std::string getTypeName() const;
-                
-                /*!
-                 * Retrieves the type to which the node evaluates.
-                 *
-                 * @return The type to which the node evaluates.
-                 */
-                ReturnType getType() const;
-                
-            protected:
-                /*!
-                 * Performs the given substitution on the expression, i.e. replaces all variables whose names are keys
-                 * of the map by a copy of the expression they are associated with in the map. This is intended as a helper
-                 * function for substitute.
-                 *
-                 * @param substitution The substitution to perform
-                 */
-                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution);
-                
-            private:
-                // The type to which this node evaluates.
-                ReturnType type;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ */

src/ir/expressions/BinaryBooleanFunctionExpression.cpp

@@ -1,67 +0,0 @@
-/*
- * BinaryBooleanFunctionExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "BinaryBooleanFunctionExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType)
-            : BinaryExpression(bool_, std::move(left), std::move(right)), functionType(functionType) {
-                // Nothing to do here.
-            }
-            
-            BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression)
-            : BinaryExpression(binaryBooleanFunctionExpression), functionType(binaryBooleanFunctionExpression.functionType) {
-                // Nothing to do here.
-            }
-
-            std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType));
-            }
-            
-            std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
-            }
-            
-            bool BinaryBooleanFunctionExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                bool resultLeft = this->getLeft()->getValueAsBool(variableValues);
-                bool resultRight = this->getRight()->getValueAsBool(variableValues);
-                switch(functionType) {
-                    case AND: return resultLeft & resultRight; break;
-                    case OR: return resultLeft | resultRight; break;
-                    default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                        << "Unknown boolean binary operator: '" << functionType << "'.";
-                }
-            }
-            
-            BinaryBooleanFunctionExpression::FunctionType BinaryBooleanFunctionExpression::getFunctionType() const {
-                return functionType;
-            }
-            
-            void BinaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string BinaryBooleanFunctionExpression::toString() const {
-                std::stringstream result;
-                result << "(" << this->getLeft()->toString();
-                switch (functionType) {
-                    case AND: result << " & "; break;
-                    case OR: result << " | "; break;
-                }
-                result << this->getRight()->toString() << ")";
-                
-                return result.str();
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/BinaryBooleanFunctionExpression.h

@@ -1,69 +0,0 @@
-/*
- * BinaryBooleanFunctionExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
-
-#include "BinaryExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a binary function expression of boolean type.
-             */
-            class BinaryBooleanFunctionExpression : public BinaryExpression {
-            public:
-                /*!
-                 * An enum type specifying the different functions applicable.
-                 */
-                enum FunctionType {AND, OR};
-                
-                /*!
-                 * Creates a binary boolean function expression tree node with the given children and function type.
-                 *
-                 * @param left The left child of the node.
-                 * @param right The right child of the node.
-                 * @param functionType The operator that is to be applied to the two children.
-                 */
-                BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param binaryBooleanFunctionExpression The expression to copy.
-                 */
-                BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                /*!
-                 * Retrieves the operator that is associated with this node.
-                 *
-                 * @param The operator that is associated with this node.
-                 */
-                FunctionType getFunctionType() const;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                                
-            private:
-                // The operator that is associated with this node.
-                FunctionType functionType;
-            };
-            
-        } // namespace expressions
-    } // namespace ir    
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ */

src/ir/expressions/BinaryExpression.cpp

@@ -1,52 +0,0 @@
-/*
- * BinaryBooleanFunctionExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include "BinaryExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            BinaryExpression::BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right)
-            : BaseExpression(type), left(std::move(left)), right(std::move(right)) {
-                // Nothing to do here.
-            }
-            
-            BinaryExpression::BinaryExpression(BinaryExpression const& binaryExpression) : BaseExpression(binaryExpression.getType()), left(binaryExpression.left->clone()), right(binaryExpression.right->clone()) {
-                // Nothing to do here.
-            }
-
-            BaseExpression* BinaryExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
-                // Get the new left successor recursively.
-                BaseExpression* newLeftSuccessor = left->performSubstitution(substitution);
-                
-                // If the left successor changed, we need to update it. If it did not change, this must not be executed,
-                // because assigning to the unique_ptr will destroy the current successor immediately.
-                if (newLeftSuccessor != left.get()) {
-                    left = std::unique_ptr<BaseExpression>(newLeftSuccessor);
-                }
-                
-                // Now do the same thing for the right successor.
-                BaseExpression* newRightSuccessor = right->performSubstitution(substitution);
-                if (newRightSuccessor != right.get()) {
-                    right = std::unique_ptr<BaseExpression>(newRightSuccessor);
-                }
-            
-                return this;
-            }
-            
-            std::unique_ptr<BaseExpression> const& BinaryExpression::getLeft() const {
-                return left;
-            }
-            
-            std::unique_ptr<BaseExpression> const& BinaryExpression::getRight() const {
-                return right;
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/BinaryExpression.h

@@ -1,66 +0,0 @@
-/*
- * BinaryExpression.h
- *
- *  Created on: 27.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_
-
-#include "src/ir/expressions/BaseExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a generic binary expression.
-             */
-            class BinaryExpression : public BaseExpression {
-            public:
-                /*!
-                 * Constructs a binary expression with the given type and children.
-                 * @param type The type of the binary expression.
-                 * @param left The left child of the binary expression.
-                 * @param right The right child of the binary expression.
-                 */
-                BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param binaryExpression The expression to copy.
-                 */
-                BinaryExpression(BinaryExpression const& binaryExpression);
-                                
-                /*!
-                 * Retrieves the left child of the expression node.
-                 *
-                 * @return The left child of the expression node.
-                 */
-                std::unique_ptr<BaseExpression> const& getLeft() const;
-                
-                /*!
-                 * Retrieves the right child of the expression node.
-                 *
-                 * @return The right child of the expression node.
-                 */
-                std::unique_ptr<BaseExpression> const& getRight() const;
-                
-            protected:
-                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override;
-                
-            private:
-                // The left child of the binary expression.
-                std::unique_ptr<BaseExpression> left;
-                
-                // The right child of the binary expression.
-                std::unique_ptr<BaseExpression> right;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ */

src/ir/expressions/BinaryNumericalFunctionExpression.cpp

@@ -1,96 +0,0 @@
-/*
- * BinaryBooleanFunctionExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-#include <algorithm>
-
-#include "BinaryNumericalFunctionExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType)
-            : BinaryExpression(type, std::move(left), std::move(right)), functionType(functionType) {
-                // Nothing to do here.
-            }
-            
-            BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression)
-            : BinaryExpression(binaryNumericalFunctionExpression), functionType(binaryNumericalFunctionExpression.functionType) {
-                // Nothing to do here.
-            }
-
-            std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType));
-            }
-
-            std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
-            }
-            
-            BinaryNumericalFunctionExpression::FunctionType BinaryNumericalFunctionExpression::getFunctionType() const {
-                return functionType;
-            }
-            
-            int_fast64_t BinaryNumericalFunctionExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (this->getType() != int_) {
-                    BaseExpression::getValueAsInt(variableValues);
-                }
-                
-                int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues);
-                int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues);
-                switch(functionType) {
-                    case PLUS: return resultLeft + resultRight; break;
-                    case MINUS: return resultLeft - resultRight; break;
-                    case TIMES: return resultLeft * resultRight; break;
-                    case DIVIDE: return resultLeft / resultRight; break;
-                    case MIN: return std::min(resultLeft, resultRight); break;
-                    case MAX: return std::max(resultLeft, resultRight); break;
-                    default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                        << "Unknown numeric binary operator: '" << functionType << "'.";
-                }
-            }
-                        
-            double BinaryNumericalFunctionExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (this->getType() != double_ && this->getType() != int_) {
-                    BaseExpression::getValueAsDouble(variableValues);
-                }
-                
-                double resultLeft = this->getLeft()->getValueAsDouble(variableValues);
-                double resultRight = this->getRight()->getValueAsDouble(variableValues);
-                switch(functionType) {
-                    case PLUS: return resultLeft + resultRight; break;
-                    case MINUS: return resultLeft - resultRight; break;
-                    case TIMES: return resultLeft * resultRight; break;
-                    case DIVIDE: return resultLeft / resultRight; break;
-                    case MIN: return std::min(resultLeft, resultRight); break;
-                    case MAX: return std::max(resultLeft, resultRight); break;
-                    default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                        << "Unknown numeric binary operator: '" << functionType << "'.";
-                }
-            }
-            
-            void BinaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string BinaryNumericalFunctionExpression::toString() const {
-                std::stringstream result;
-                switch (functionType) {
-                    case PLUS: result << "(" << this->getLeft()->toString() << " + " << this->getRight()->toString() << ")"; break;
-                    case MINUS: result << "(" << this->getLeft()->toString() << " - " << this->getRight()->toString() << ")"; break;
-                    case TIMES: result << "(" << this->getLeft()->toString() << " * " << this->getRight()->toString() << ")"; break;
-                    case DIVIDE: result << "(" << this->getLeft()->toString() << " / " << this->getRight()->toString() << ")"; break;
-                    case MIN: result << "min(" << this->getLeft()->toString() << ", " << this->getRight()->toString() << ")"; break;
-                    case MAX: result << "max(" << this->getLeft()->toString() << ", " << this->getRight()->toString() << ")"; break;
-                }
-                return result.str();
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/BinaryNumericalFunctionExpression.h

@@ -1,72 +0,0 @@
-/*
- * BinaryFunctionExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BINARYFUNCTIONEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_BINARYFUNCTIONEXPRESSION_H_
-
-#include "src/ir/expressions/BinaryExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a binary function expression of numerical type.
-             */
-            class BinaryNumericalFunctionExpression : public BinaryExpression {
-            public:
-                /*!
-                 * An enum type specifying the different functions applicable.
-                 */
-                enum FunctionType {PLUS, MINUS, TIMES, DIVIDE, MIN, MAX};
-                
-                /*!
-                 * Creates a binary numerical function expression with the given type, children and function type.
-                 *
-                 * @param type The type of the expression tree node.
-                 * @param left The left child of the expression tree node.
-                 * @param right The right child of the  expression tree node.
-                 * @param functionType The function that is applied to the children of this node.
-                 */
-                BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType);
-                
-                /*!
-                 * Performs a deep-copy of the given expression.
-                 *
-                 * @param binaryNumericalFunctionExpression The expression to copy.
-                 */
-                BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression);
-
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                /*!
-                 * Retrieves the operator that is associated with this node.
-                 *
-                 * @param The operator that is associated with this node.
-                 */
-                FunctionType getFunctionType() const;
-                
-                virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                
-            private:
-                // The operator that is associated with this node.
-                FunctionType functionType;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_BINARYFUNCTIONEXPRESSION_H_ */

src/ir/expressions/BinaryRelationExpression.cpp

@@ -1,75 +0,0 @@
-/*
- * BinaryBooleanFunctionExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "BinaryRelationExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            BinaryRelationExpression::BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType)
-            : BinaryExpression(bool_, std::move(left), std::move(right)), relationType(relationType) {
-                // Nothing to do here.
-            }
-            
-            BinaryRelationExpression::BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression)
-            : BinaryExpression(binaryRelationExpression), relationType(binaryRelationExpression.relationType) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> BinaryRelationExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType));
-            }
-
-            std::unique_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType));
-            }
-            
-            bool BinaryRelationExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues);
-                int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues);
-                switch(relationType) {
-                    case EQUAL: return resultLeft == resultRight; break;
-                    case NOT_EQUAL: return resultLeft != resultRight; break;
-                    case LESS: return resultLeft < resultRight; break;
-                    case LESS_OR_EQUAL: return resultLeft <= resultRight; break;
-                    case GREATER: return resultLeft > resultRight; break;
-                    case GREATER_OR_EQUAL: return resultLeft >= resultRight; break;
-                    default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                        << "Unknown boolean binary relation: '" << relationType << "'.";
-                }
-            }
-            
-            BinaryRelationExpression::RelationType BinaryRelationExpression::getRelationType() const {
-                return relationType;
-            }
-            
-            void BinaryRelationExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string BinaryRelationExpression::toString() const {
-                std::stringstream result;
-                result << "(" << this->getLeft()->toString();
-                switch (relationType) {
-                    case EQUAL: result << " = "; break;
-                    case NOT_EQUAL: result << " != "; break;
-                    case LESS: result << " < "; break;
-                    case LESS_OR_EQUAL: result << " <= "; break;
-                    case GREATER: result << " > "; break;
-                    case GREATER_OR_EQUAL: result << " >= "; break;
-                }
-                result << this->getRight()->toString() << ")";
-                
-                return result.str();
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/BinaryRelationExpression.h

@@ -1,69 +0,0 @@
-/*
- * BinaryRelationExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BINARYRELATIONEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_BINARYRELATIONEXPRESSION_H_
-
-#include "src/ir/expressions/BinaryExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a binary relation expression of boolean type.
-             */
-            class BinaryRelationExpression : public BinaryExpression {
-            public:
-                /*!
-                 * An enum type specifying the different relations applicable.
-                 */
-                enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
-                
-                /*!
-                 * Creates a binary relation expression tree node with the given children and relation type.
-                 *
-                 * @param left The left child of the binary expression.
-                 * @param right The right child of the binary expression.
-                 * @param relationType The type of the relation associated with this node.
-                 */
-                BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param binaryRelationExpression The expression to copy.
-                 */
-                BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                /*!
-                 * Retrieves the relation that is associated with this node.
-                 *
-                 * @param The relation that is associated with this node.
-                 */
-                RelationType getRelationType() const;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                
-            private:
-                // The relation operator associated with this node.
-                RelationType relationType;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_BINARYRELATIONEXPRESSION_H_ */

src/ir/expressions/BooleanConstantExpression.cpp

@@ -1,45 +0,0 @@
-/*
- * BooleanConstantExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include "BooleanConstantExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression<bool>(bool_, constantName) {
-                // Nothing to do here.
-            }
-            
-            BooleanConstantExpression::BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression) : ConstantExpression(booleanConstantExpression) {
-                // Nothing to do here.
-            }
-
-            std::unique_ptr<BaseExpression> BooleanConstantExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this));
-            }
-
-            std::unique_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this));
-            }
-            
-            bool BooleanConstantExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (!this->isDefined()) {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                    << "Boolean constant '" << this->getConstantName() << "' is undefined.";
-                } else {
-                    return this->getValue();
-                }
-            }
-            
-            void BooleanConstantExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/BooleanConstantExpression.h

@@ -1,49 +0,0 @@
-/*
- * BooleanConstantExpression.h
- *
- *  Created on: 04.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_
-
-#include "ConstantExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a boolean constant expression.
-             */
-            class BooleanConstantExpression : public ConstantExpression<bool> {
-            public:
-                /*!
-                 * Creates a boolean constant expression with the given constant name.
-                 *
-                 * @param constantName The name of the constant to use.
-                 */
-                BooleanConstantExpression(std::string const& constantName);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param booleanConstantExpression The expression to copy.
-                 */
-                BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ */

src/ir/expressions/BooleanLiteralExpression.cpp

@@ -1,49 +0,0 @@
-/*
- * BooleanLiteralExpression.cpp
- *
- *  Created on: 04.01.2013
- *      Author: Christian Dehnert
- */
-
-#include "BooleanLiteralExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            BooleanLiteralExpression::BooleanLiteralExpression(bool value) : BaseExpression(bool_), value(value) {
-                // Nothing to do here.
-            }
-            
-            BooleanLiteralExpression::BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression)
-            : BaseExpression(booleanLiteralExpression), value(booleanLiteralExpression.value) {
-                // Nothing to do here.
-            }
-
-            std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
-            }
-                                                       
-            std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(this->value));
-            }
-            
-            bool BooleanLiteralExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                return value;
-            }
-            
-            void BooleanLiteralExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string BooleanLiteralExpression::toString() const {
-                if (value) {
-                    return std::string("true");
-                } else {
-                    return std::string("false");
-                }
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/BooleanLiteralExpression.h

@@ -1,55 +0,0 @@
-/*
- * BooleanLiteralExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_
-
-#include "src/ir/expressions/BaseExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a boolean literal.
-             */
-            class BooleanLiteralExpression : public BaseExpression {
-            public:
-                /*!
-                 * Creates a boolean literal expression with the given value.
-                 *
-                 * @param value The value for the boolean literal.
-                 */
-                BooleanLiteralExpression(bool value);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param booleanLiteralExpression The expression to copy.
-                 */
-                BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                
-            private:
-                // The value of the boolean literal.
-                bool value;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_ */

src/ir/expressions/ConstantExpression.h

@@ -1,132 +0,0 @@
-/*
- * ConstantExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_
-
-#include "BaseExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            // A struct for storing whether the constant was defined and if so, what value it holds.
-            template<class T>
-            struct ConstantDefinitionStruct {
-                /*!
-                 * Constructs a structure indicating that the constant has been defined with the given value.
-                 *
-                 * @param value The value with which the constant was defined.
-                 */
-                ConstantDefinitionStruct(T value) : value(value), defined(true) {
-                   // Nothing to do here. 
-                }
-                
-                /*!
-                 * Constructs a structure indicating that the constant has not yet been defined.
-                 *
-                 * @param value The value with which the constant was defined.
-                 */
-                ConstantDefinitionStruct() : value(), defined(false) {
-                    // Nothing to do here. 
-                }
-                
-                T value;
-                bool defined;
-            };
-            
-            /*!
-             * A class representing a generic constant expression.
-             */
-            template<class T>
-            class ConstantExpression : public BaseExpression {
-            public:
-                /*!
-                 * Constructs a constant expression of the given type with the given constant name.
-                 *
-                 * @param type The type of the constant.
-                 * @param constantName The name of the constant.
-                 */
-                ConstantExpression(ReturnType type, std::string const& constantName) : BaseExpression(type), constantName(constantName), valueStructPointer(new ConstantDefinitionStruct<T>()) {
-                    // Nothing to do here.
-                }
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param constantExpression The expression to copy.
-                 */
-                ConstantExpression(ConstantExpression const& constantExpression) : BaseExpression(constantExpression), constantName(constantExpression.constantName), valueStructPointer(constantExpression.valueStructPointer) {
-                    // Nothing to do here.
-                }
-                
-                /*!
-                 * Retrieves the name of the constant.
-                 *
-                 * @return The name of the constant.
-                 */
-                std::string const& getConstantName() const {
-                    return constantName;
-                }
-                
-                virtual std::string toString() const override {
-                    std::stringstream result;
-                    if (this->valueStructPointer->defined) {
-                        result << this->valueStructPointer->value;
-                    } else {
-                        result << this->getConstantName();
-                    }
-                    return result.str();
-                }
-                
-                /*!
-                 * Retrieves whether the constant is defined or not.
-                 *
-                 * @return True if the constant is defined.
-                 */
-                bool isDefined() const {
-                    return this->valueStructPointer->defined;
-                }
-                
-                /*!
-                 * Retrieves the value of the constant if it is defined.
-                 */
-                T getValue() const {
-                    return this->valueStructPointer->value;
-                }
-                
-                /*!
-                 * Defines the constant using the given value.
-                 *
-                 * @param value The value to use for defining the constant.
-                 */
-                void define(T value) {
-                    this->valueStructPointer->defined = true;
-                    this->valueStructPointer->value = value;
-                }
-                
-                /*!
-                 * Undefines the value that was previously set for this constant (if any).
-                 */
-                void undefine() {
-                    this->valueStructPointer->defined = false;
-                    this->valueStructPointer->value = T();
-                }
-                
-            private:
-                // The name of the constant.
-                std::string constantName;
-                
-                // The definedness status and (if applicable) the value of the constant.
-                std::shared_ptr<ConstantDefinitionStruct<T>> valueStructPointer;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_ */

src/ir/expressions/DoubleConstantExpression.cpp

@@ -1,45 +0,0 @@
-/*
- * DoubleConstantExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include "DoubleConstantExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression<double>(double_, constantName) {
-                // Nothing to do here.
-            }
-            
-            DoubleConstantExpression::DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression) : ConstantExpression(doubleConstantExpression) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> DoubleConstantExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this));
-            }
-            
-            std::unique_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this));
-            }
-            
-            double DoubleConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (!this->isDefined()) {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                    << "Double constant '" << this->getConstantName() << "' is undefined.";
-                } else {
-                    return this->getValue();
-                }
-            }
-            
-            void DoubleConstantExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/DoubleConstantExpression.h

@@ -1,49 +0,0 @@
-/*
- * DoubleConstantExpression.h
- *
- *  Created on: 04.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_
-
-#include "ConstantExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a constant expression of type double.
-             */
-            class DoubleConstantExpression : public ConstantExpression<double> {
-            public:
-                /*!
-                 * Creates a double constant expression with the given constant name.
-                 *
-                 * @param constantName The name of the constant to use.
-                 */
-                DoubleConstantExpression(std::string const& constantName);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param doubleConstantExpression The expression to copy.
-                 */
-                DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ */

src/ir/expressions/DoubleLiteralExpression.cpp

@@ -1,49 +0,0 @@
-/*
- * DoubleLiteralExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "DoubleLiteralExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            DoubleLiteralExpression::DoubleLiteralExpression(double value) : BaseExpression(double_), value(value) {
-                // Nothing to do here.
-            }
-            
-            DoubleLiteralExpression::DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression)
-            : BaseExpression(doubleLiteralExpression), value(doubleLiteralExpression.value) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
-            }
-
-            std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(this->value));
-            }
-            
-            double DoubleLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                return value;
-            }
-            
-            void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string DoubleLiteralExpression::toString() const {
-                std::stringstream result;
-                result << value;
-                return result.str();
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/DoubleLiteralExpression.h

@@ -1,55 +0,0 @@
-/*
- * DoubleLiteralExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_
-
-#include "src/ir/expressions/BaseExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a double literal.
-             */
-            class DoubleLiteralExpression : public BaseExpression {
-            public:
-                /*!
-                 * Creates a double literal expression with the given value.
-                 *
-                 * @param value The value for the double literal.
-                 */
-                DoubleLiteralExpression(double value);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param doubleLiteralExpression The expression to copy.
-                 */
-                DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                
-            private:
-                // The value of the double literal.
-                double value;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ */

src/ir/expressions/ExpressionVisitor.h

@@ -1,49 +0,0 @@
-/*
- * ExpressionVisitor.h
- *
- *  Created on: 26.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_
-#define STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            class BaseExpression;
-            class BinaryBooleanFunctionExpression;
-            class BinaryNumericalFunctionExpression;
-            class BinaryRelationExpression;
-            class BooleanConstantExpression;
-            class BooleanLiteralExpression;
-            class DoubleConstantExpression;
-            class DoubleLiteralExpression;
-            class IntegerConstantExpression;
-            class IntegerLiteralExpression;
-            class UnaryBooleanFunctionExpression;
-            class UnaryNumericalFunctionExpression;
-            class VariableExpression;
-            
-            class ExpressionVisitor {
-            public:
-                virtual void visit(BinaryBooleanFunctionExpression* expression) = 0;
-                virtual void visit(BinaryNumericalFunctionExpression* expression) = 0;
-                virtual void visit(BinaryRelationExpression* expression) = 0;
-                virtual void visit(BooleanConstantExpression* expression) = 0;
-                virtual void visit(BooleanLiteralExpression* expression) = 0;
-                virtual void visit(DoubleConstantExpression* expression) = 0;
-                virtual void visit(DoubleLiteralExpression* expression) = 0;
-                virtual void visit(IntegerConstantExpression* expression) = 0;
-                virtual void visit(IntegerLiteralExpression* expression) = 0;
-                virtual void visit(UnaryBooleanFunctionExpression* expression) = 0;
-                virtual void visit(UnaryNumericalFunctionExpression* expression) = 0;
-                virtual void visit(VariableExpression* expression) = 0;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ */

src/ir/expressions/Expressions.h

@@ -1,26 +0,0 @@
-/*
- * Expressions.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONS_H_
-#define STORM_IR_EXPRESSIONS_EXPRESSIONS_H_
-
-#include "BaseExpression.h"
-#include "BinaryBooleanFunctionExpression.h"
-#include "BinaryNumericalFunctionExpression.h"
-#include "BinaryRelationExpression.h"
-#include "BooleanLiteralExpression.h"
-#include "DoubleLiteralExpression.h"
-#include "IntegerLiteralExpression.h"
-#include "UnaryBooleanFunctionExpression.h"
-#include "UnaryNumericalFunctionExpression.h"
-#include "VariableExpression.h"
-#include "ConstantExpression.h"
-#include "BooleanConstantExpression.h"
-#include "IntegerConstantExpression.h"
-#include "DoubleConstantExpression.h"
-
-#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ */

src/ir/expressions/IntegerConstantExpression.cpp

@@ -1,48 +0,0 @@
-/*
- * IntegerConstantExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include "IntegerConstantExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(int_, constantName) {
-                // Nothing to do here.
-            }
-            
-            IntegerConstantExpression::IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression) : ConstantExpression(integerConstantExpression) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> IntegerConstantExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this));
-            }
-            
-            std::unique_ptr<BaseExpression> IntegerConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this));
-            }
-            
-            double IntegerConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                return static_cast<double>(getValueAsInt(variableValues));
-            }
-            
-            int_fast64_t IntegerConstantExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (!this->isDefined()) {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                    << "Integer constant '" << this->getConstantName() << "' is undefined.";
-                } else {
-                    return this->getValue();
-                }
-            }
-            
-            void IntegerConstantExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/IntegerConstantExpression.h

@@ -1,51 +0,0 @@
-/*
- * IntegerConstantExpression.h
- *
- *  Created on: 04.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_
-
-#include "ConstantExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a constant expression of type integer.
-             */
-            class IntegerConstantExpression : public ConstantExpression<int_fast64_t> {
-            public:
-                /*!
-                 * Creates an integer constant expression with the given constant name.
-                 *
-                 * @param constantName The name of the constant to use.
-                 */
-                IntegerConstantExpression(std::string const& constantName);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param integerConstantExpression The expression to copy.
-                 */
-                IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ */

src/ir/expressions/IntegerLiteralExpression.cpp

@@ -1,53 +0,0 @@
-/*
- * IntegerLiteralExpression.cpp
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "IntegerLiteralExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            IntegerLiteralExpression::IntegerLiteralExpression(int_fast64_t value) : BaseExpression(int_), value(value) {
-                // Nothing to do here.
-            }
-            
-            IntegerLiteralExpression::IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression)
-            : BaseExpression(integerLiteralExpression), value(integerLiteralExpression.value) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
-            }
-            
-            std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(this->value));
-            }
-            
-            double IntegerLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                return static_cast<double>(value);
-            }
-            
-            int_fast64_t IntegerLiteralExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                return value;
-            }
-            
-            void IntegerLiteralExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string IntegerLiteralExpression::toString() const {
-                std::stringstream result;
-                result << value;
-                return result.str();
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/IntegerLiteralExpression.h

@@ -1,57 +0,0 @@
-/*
- * IntegerLiteralExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_
-
-#include "src/ir/expressions/BaseExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing an integer literal.
-             */
-            class IntegerLiteralExpression : public BaseExpression {
-            public:
-                /*!
-                 * Creates an integer literal expression with the given value.
-                 *
-                 * @param value The value for the integer literal.
-                 */
-                IntegerLiteralExpression(int_fast64_t value);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param integerLiteralExpression The expression to copy.
-                 */
-                IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                
-            private:
-                // The value of the double literal.
-                int_fast64_t value;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ */

src/ir/expressions/UnaryBooleanFunctionExpression.cpp

@@ -1,62 +0,0 @@
-/*
- * UnaryBooleanFunctionExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include <sstream>
-
-#include "UnaryBooleanFunctionExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(bool_, std::move(child)), functionType(functionType) {
-                // Nothing to do here.
-            }
-            
-            UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression) : UnaryExpression(unaryBooleanFunctionExpression), functionType(unaryBooleanFunctionExpression.functionType) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType));
-            }
-            
-            std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType));
-            }
-            
-            UnaryBooleanFunctionExpression::FunctionType UnaryBooleanFunctionExpression::getFunctionType() const {
-                return functionType;
-            }
-            
-            bool UnaryBooleanFunctionExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                bool resultChild = this->getChild()->getValueAsBool(variableValues);
-                switch(functionType) {
-                    case NOT: return !resultChild; break;
-                    default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                        << "Unknown boolean unary operator: '" << functionType << "'.";
-                }
-            }
-            
-            void UnaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string UnaryBooleanFunctionExpression::toString() const {
-                std::stringstream result;
-                result << "(";
-                switch (functionType) {
-                    case NOT: result << "!"; break;
-                }
-                result << this->getChild()->toString() << ")";
-                
-                return result.str();
-            }
-
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/UnaryBooleanFunctionExpression.h

@@ -1,68 +0,0 @@
-/*
- * UnaryBooleanFunctionExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_
-
-#include "UnaryExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a unary function expression of boolean type.
-             */
-            class UnaryBooleanFunctionExpression : public UnaryExpression {
-            public:
-                /*!
-                 * An enum type specifying the different functions applicable.
-                 */
-                enum FunctionType {NOT};
-                
-                /*!
-                 * Creates a unary boolean function expression tree node with the given child and function type.
-                 *
-                 * @param child The child of the node.
-                 * @param functionType The operator that is to be applied to the two children.
-                 */
-                UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param unaryBooleanFunctionExpression The expression to copy.
-                 */
-                UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-
-                /*!
-                 * Retrieves the operator that is associated with this node.
-                 *
-                 * @param The operator that is associated with this node.
-                 */
-                FunctionType getFunctionType() const;
-                
-                virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                                
-            private:
-                // The operator that is associated with this node.
-                FunctionType functionType;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ */

src/ir/expressions/UnaryExpression.cpp

@@ -1,39 +0,0 @@
-/*
- * UnaryExpression.cpp
- *
- *  Created on: 27.01.2013
- *      Author: Christian Dehnert
- */
-
-#include "UnaryExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-    
-            UnaryExpression::UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child) : BaseExpression(type), child(std::move(child)) {
-                // Nothing to do here.
-            }
-            
-            UnaryExpression::UnaryExpression(UnaryExpression const& unaryExpression) : BaseExpression(unaryExpression), child(unaryExpression.child->clone()) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> const& UnaryExpression::getChild() const {
-                return child;
-            }
-            
-            BaseExpression* UnaryExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
-                BaseExpression* newChild = child->performSubstitution(substitution);
-                
-                // Only update the child if it changed, because otherwise the child gets destroyed.
-                if (newChild != child.get()) {
-                    child = std::unique_ptr<BaseExpression>(newChild);
-                }
-                
-                return this;
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/UnaryExpression.h

@@ -1,55 +0,0 @@
-/*
- * UnaryExpression.h
- *
- *  Created on: 27.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_
-
-#include "BaseExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a generic unary expression.
-             */
-            class UnaryExpression : public BaseExpression {
-            public:
-                /*!
-                 * Constructs a unary expression with the given type and child.
-                 * @param type The type of the unary expression.
-                 * @param right The child of the unary expression.
-                 */
-                UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param unaryExpression The expression to copy.
-                 */
-                UnaryExpression(UnaryExpression const& unaryExpression);
-                
-                /*!
-                 * Retrieves the child of the expression node.
-                 *
-                 * @return The child of the expression node.
-                 */
-                std::unique_ptr<BaseExpression> const& getChild() const;
-
-            protected:
-                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override;
-                
-            private:
-                // The left child of the unary expression.
-                std::unique_ptr<BaseExpression> child;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ */

src/ir/expressions/UnaryNumericalFunctionExpression.cpp

@@ -1,86 +0,0 @@
-/*
- * UnaryFunctionExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#include <cmath>
-
-#include "UnaryNumericalFunctionExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(type, std::move(child)), functionType(functionType) {
-                // Nothing to do here.
-            }
-            
-            UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression) : UnaryExpression(unaryNumericalFunctionExpression), functionType(unaryNumericalFunctionExpression.functionType) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType));
-            }
-            
-            std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType));
-            }
-            
-            int_fast64_t UnaryNumericalFunctionExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (this->getType() != int_) {
-                    BaseExpression::getValueAsInt(variableValues);
-                }
-                
-                int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues);
-                switch(functionType) {
-                    case MINUS: return -resultChild; break;
-                    case FLOOR: return static_cast<int_fast64_t>(std::floor(resultChild)); break;
-                    case CEIL: return static_cast<int_fast64_t>(std::ceil(resultChild)); break;
-                    default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                        << "Unknown numerical unary operator: '" << functionType << "'.";
-                }
-            }
-            
-            double UnaryNumericalFunctionExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (this->getType() != double_ && this->getType() != int_) {
-                    BaseExpression::getValueAsDouble(variableValues);
-                }
-                
-                double resultChild = this->getChild()->getValueAsDouble(variableValues);
-                switch(functionType) {
-                    case MINUS: return -resultChild; break;
-                    case FLOOR: return std::floor(resultChild); break;
-                    case CEIL: return std::ceil(resultChild); break;
-                    default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
-                        << "Unknown numerical unary operator: '" << functionType << "'.";
-                }
-            }
-            
-            UnaryNumericalFunctionExpression::FunctionType UnaryNumericalFunctionExpression::getFunctionType() const {
-                return functionType;
-            }
-            
-            void UnaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string UnaryNumericalFunctionExpression::toString() const {
-                std::stringstream result;
-                result << "(";
-                switch (functionType) {
-                    case MINUS: result << "-"; break;
-                    case FLOOR: result << "floor("; break;
-                    case CEIL: result << "ceil("; break;
-                }
-                result << this->getChild()->toString() << ")";
-                
-                return result.str();
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-

src/ir/expressions/UnaryNumericalFunctionExpression.h

@@ -1,70 +0,0 @@
-/*
- * UnaryFunctionExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_
-
-#include "UnaryExpression.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            /*!
-             * A class representing a unary function expression of numerical type.
-             */
-            class UnaryNumericalFunctionExpression : public UnaryExpression {
-            public:
-                /*!
-                 * An enum type specifying the different functions applicable.
-                 */
-                enum FunctionType {MINUS, FLOOR, CEIL};
-                
-                /*!
-                 * Creates a unary numerical function expression tree node with the given child and function type.
-                 *
-                 * @param child The child of the node.
-                 * @param functionType The operator that is to be applied to the two children.
-                 */
-                UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param unaryNumericalFunctionExpression The expression to copy.
-                 */
-                UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-                
-                virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-                
-                /*!
-                 * Retrieves the operator that is associated with this node.
-                 *
-                 * @param The operator that is associated with this node.
-                 */
-                FunctionType getFunctionType() const;
-                
-                virtual void accept(ExpressionVisitor* visitor) override;
-                
-                virtual std::string toString() const override;
-                
-            private:
-                // The operator that is associated with this node.
-                FunctionType functionType;
-            };
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ */

src/ir/expressions/VariableExpression.cpp

@@ -1,120 +0,0 @@
-/*
- * VariableExpression.cpp
- *
- *  Created on: 10.06.2013
- *      Author: Christian Dehnert
- */
-
-#include "VariableExpression.h"
-#include "src/parser/prismparser/VariableState.h"
-#include "src/exceptions/ExpressionEvaluationException.h"
-
-namespace storm {
-    namespace ir {
-        namespace expressions {
-            
-            VariableExpression::VariableExpression(ReturnType type, std::string const& variableName) : BaseExpression(type), globalIndex(0), variableName(variableName) {
-                // Nothing to do here.
-            }
-            
-            VariableExpression::VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName)
-            : BaseExpression(type), globalIndex(globalIndex), variableName(variableName) {
-                // Nothing to do here.
-            }
-            
-            VariableExpression::VariableExpression(VariableExpression const& variableExpression) : BaseExpression(variableExpression), globalIndex(variableExpression.globalIndex), variableName(variableExpression.variableName) {
-                // Nothing to do here.
-            }
-            
-            std::unique_ptr<BaseExpression> VariableExpression::clone() const {
-                return std::unique_ptr<BaseExpression>(new VariableExpression(*this));
-            }
-            
-            std::unique_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                // Perform the proper cloning.
-                auto renamingPair = renaming.find(this->variableName);
-                if (renamingPair != renaming.end()) {
-                    if (this->getType() == int_) {
-                        return variableState.getIntegerVariableExpression(renamingPair->second)->clone();
-                    } else {
-                        return variableState.getBooleanVariableExpression(renamingPair->second)->clone();
-                    }
-                } else {
-                    if (this->getType() == int_) {
-                        return variableState.getIntegerVariableExpression(this->variableName)->clone();
-                    } else {
-                        return variableState.getBooleanVariableExpression(this->variableName)->clone();
-                    }
-                }
-            }
-            
-            BaseExpression* VariableExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
-                // If the name of the variable is a key of the map, we need to replace it.
-                auto substitutionIterator = substitution.find(variableName);
-                
-                if (substitutionIterator != substitution.end()) {
-                    std::unique_ptr<BaseExpression> expressionClone = substitutionIterator->second.get().clone();
-                    BaseExpression* rawPointer = expressionClone.release();
-                    return rawPointer;
-                } else {
-                    // Otherwise, we don't need to replace anything.
-                    return this;
-                }
-            }
-            
-            void VariableExpression::accept(ExpressionVisitor* visitor) {
-                visitor->visit(this);
-            }
-            
-            std::string VariableExpression::toString() const {
-                return this->variableName;
-            }
-            
-            int_fast64_t VariableExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (this->getType() != int_) {
-                    BaseExpression::getValueAsInt(variableValues);
-                }
-                
-                if (variableValues != nullptr) {
-                    return variableValues->second[globalIndex];
-                } else {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression involving variables without variable values.";
-                }
-            }
-            
-            bool VariableExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (this->getType() != bool_) {
-                    BaseExpression::getValueAsBool(variableValues);
-                }
-                
-                if (variableValues != nullptr) {
-                    return variableValues->first[globalIndex];
-                } else {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression involving variables without variable values.";
-                }
-            }
-            
-            double VariableExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
-                if (this->getType() != double_ && this->getType() != int_) {
-                    BaseExpression::getValueAsDouble(variableValues);
-                }
-                
-                // Because only int variables can deliver a double value, we only need to check them.
-                if (variableValues != nullptr) {
-                    return static_cast<double>(variableValues->second[globalIndex]);
-                } else {
-                    throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression with variable '" << variableName << "' of type double.";
-                }
-            }
-            
-            std::string const& VariableExpression::getVariableName() const {
-                return variableName;
-            }
-            
-            uint_fast64_t VariableExpression::getGlobalVariableIndex() const {
-                return this->globalIndex;
-            }
-            
-        } // namespace expressions
-    } // namespace ir
-} // namespace storm

src/ir/expressions/VariableExpression.h

@@ -1,98 +0,0 @@
-/*
- * VariableExpression.h
- *
- *  Created on: 03.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_
-#define STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_
-
-#include "BaseExpression.h"
-
-namespace storm {
-	
-    // Forward-declare VariableState.
-	namespace parser {
-		namespace prismparser {
-			class VariableState;
-		} // namespace prismparser
-	} // namespace parser
-    
-	namespace ir {
-		namespace expressions {
-			
-            /*!
-             * A class representing a variable in the expression tree.
-             */
-			class VariableExpression : public BaseExpression {
-			public:
-                /*!
-                 * Creates a variable expression of the given type with the given name. As this variable has no indices
-                 * it is only meant as a dummy and needs to be replaced with a "full" variable expression.
-                 *
-                 * @param type The type of the variable.
-                 * @param variableName The name of the variable.
-                 */
-				VariableExpression(ReturnType type, std::string const& variableName);
-				
-                /*!
-                 * Creates a variable expression of the given type with the given name and indices.
-                 *
-                 * @param type The type of the variable.
-                 * @param globalIndex The global (i.e. program-wide) index of the variable.
-                 * @param variableName The name of the variable.
-                 */
-				VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName);
-                
-                /*!
-                 * Copy-constructs from the given expression.
-                 *
-                 * @param variableExpression The expression to copy.
-                 */
-                VariableExpression(VariableExpression const& variableExpression);
-                
-                virtual std::unique_ptr<BaseExpression> clone() const override;
-                
-				virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-				            
-				virtual void accept(ExpressionVisitor* visitor) override;
-				
-				virtual std::string toString() const override;
-				
-				virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-				
-				virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-				
-				virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
-				
-                /*!
-                 * Retrieves the name of the variable.
-                 *
-                 * @return The name of the variable.
-                 */
-				std::string const& getVariableName() const;
-				
-                /*!
-                 * Retrieves the global (i.e. program-wide) index of the variable.
-                 *
-                 * @return The global index of the variable.
-                 */
-				uint_fast64_t getGlobalVariableIndex() const;
-				            
-            protected:
-                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override;
-                
-			private:
-                // The global index of the variable.
-				uint_fast64_t globalIndex;
-                
-                // The name of the variable.
-				std::string variableName;
-			};
-			
-		} // namespace expressions
-	} // namespace ir
-} // namespace storm
-
-#endif /* STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ */

src/storage/dd/CuddDd.cpp

@@ -7,25 +7,25 @@
 
 namespace storm {
     namespace dd {
-        Dd<CUDD>::Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) {
+        Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariableNames(containedMetaVariableNames) {
             // Intentionally left empty.
         }
         
-        bool Dd<CUDD>::operator==(Dd<CUDD> const& other) const {
+        bool Dd<DdType::CUDD>::operator==(Dd<DdType::CUDD> const& other) const {
             return this->cuddAdd == other.getCuddAdd();
         }
         
-        bool Dd<CUDD>::operator!=(Dd<CUDD> const& other) const {
+        bool Dd<DdType::CUDD>::operator!=(Dd<DdType::CUDD> const& other) const {
             return this->cuddAdd == other.getCuddAdd();
         }
         
-        Dd<CUDD> Dd<CUDD>::operator+(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result += other;
             return result;
         }
         
-        Dd<CUDD>& Dd<CUDD>::operator+=(Dd<CUDD> const& other) {
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator+=(Dd<DdType::CUDD> const& other) {
             this->cuddAdd += other.getCuddAdd();
             
             // Join the variable sets of the two participating DDs.
@@ -34,13 +34,13 @@ namespace storm {
             return *this;
         }
         
-        Dd<CUDD> Dd<CUDD>::operator*(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator*(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result *= other;
             return result;
         }
         
-        Dd<CUDD>& Dd<CUDD>::operator*=(Dd<CUDD> const& other) {
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator*=(Dd<DdType::CUDD> const& other) {
             this->cuddAdd *= other.getCuddAdd();
             
             // Join the variable sets of the two participating DDs.
@@ -49,13 +49,13 @@ namespace storm {
             return *this;
         }
         
-        Dd<CUDD> Dd<CUDD>::operator-(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result -= other;
             return result;
         }
         
-        Dd<CUDD>& Dd<CUDD>::operator-=(Dd<CUDD> const& other) {
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator-=(Dd<DdType::CUDD> const& other) {
             this->cuddAdd -= other.getCuddAdd();
             
             // Join the variable sets of the two participating DDs.
@@ -64,13 +64,13 @@ namespace storm {
             return *this;
         }
         
-        Dd<CUDD> Dd<CUDD>::operator/(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator/(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result /= other;
             return result;
         }
         
-        Dd<CUDD>& Dd<CUDD>::operator/=(Dd<CUDD> const& other) {
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator/=(Dd<DdType::CUDD> const& other) {
             this->cuddAdd = this->cuddAdd.Divide(other.getCuddAdd());
             
             // Join the variable sets of the two participating DDs.
@@ -79,55 +79,55 @@ namespace storm {
             return *this;
         }
         
-        Dd<CUDD> Dd<CUDD>::operator~() const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator~() const {
+            Dd<DdType::CUDD> result(*this);
             result.complement();
             return result;
         }
         
-        Dd<CUDD>& Dd<CUDD>::complement() {
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
             this->cuddAdd = ~this->cuddAdd;
             return *this;
         }
         
-        Dd<CUDD> Dd<CUDD>::equals(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result.cuddAdd = result.cuddAdd.Equals(other.getCuddAdd());
             return result;
         }
         
-        Dd<CUDD> Dd<CUDD>::notEquals(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::notEquals(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result.cuddAdd = result.cuddAdd.NotEquals(other.getCuddAdd());
             return result;
         }
         
-        Dd<CUDD> Dd<CUDD>::less(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::less(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result.cuddAdd = result.cuddAdd.LessThan(other.getCuddAdd());
             return result;
         }
         
-        Dd<CUDD> Dd<CUDD>::lessOrEqual(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::lessOrEqual(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result.cuddAdd = result.cuddAdd.LessThanOrEqual(other.getCuddAdd());
             return result;
         }
         
-        Dd<CUDD> Dd<CUDD>::greater(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result.cuddAdd = result.cuddAdd.GreaterThan(other.getCuddAdd());
             return result;
         }
         
-        Dd<CUDD> Dd<CUDD>::greaterOrEqual(Dd<CUDD> const& other) const {
-            Dd<CUDD> result(*this);
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
             result.cuddAdd = result.cuddAdd.GreaterThanOrEqual(other.getCuddAdd());
             return result;
         }
         
-        void Dd<CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) {
-            Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+        void Dd<DdType::CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) {
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             
             for (auto const& metaVariableName : metaVariableNames) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -136,15 +136,15 @@ namespace storm {
                 }
                 this->getContainedMetaVariableNames().erase(metaVariableName);
                 
-                DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+                DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
                 cubeDd *= metaVariable.getCube();
             }
             
             this->cuddAdd = this->cuddAdd.OrAbstract(cubeDd.getCuddAdd());
         }
         
-        void Dd<CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) {
-            Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+        void Dd<DdType::CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) {
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             
             for (auto const& metaVariableName : metaVariableNames) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -153,15 +153,15 @@ namespace storm {
                 }
                 this->getContainedMetaVariableNames().erase(metaVariableName);
                 
-                DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+                DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
                 cubeDd *= metaVariable.getCube();
             }
             
             this->cuddAdd = this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd());
         }
         
-        void Dd<CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) {
-            Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+        void Dd<DdType::CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) {
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             
             for (auto const& metaVariableName : metaVariableNames) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -170,15 +170,15 @@ namespace storm {
                 }
                 this->getContainedMetaVariableNames().erase(metaVariableName);
                 
-                DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+                DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
                 cubeDd *= metaVariable.getCube();
             }
             
             this->cuddAdd = this->cuddAdd.MinAbstract(cubeDd.getCuddAdd());
         }
         
-        void Dd<CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) {
-            Dd<CUDD> cubeDd(this->getDdManager()->getOne());
+        void Dd<DdType::CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) {
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             
             for (auto const& metaVariableName : metaVariableNames) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -187,19 +187,19 @@ namespace storm {
                 }
                 this->getContainedMetaVariableNames().erase(metaVariableName);
                 
-                DdMetaVariable<CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+                DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
                 cubeDd *= metaVariable.getCube();
             }
             
             this->cuddAdd = this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd());
         }
         
-        void Dd<CUDD>::swapVariables(std::vector<std::pair<std::string, std::string>> const& metaVariablePairs) {
+        void Dd<DdType::CUDD>::swapVariables(std::vector<std::pair<std::string, std::string>> const& metaVariablePairs) {
             std::vector<ADD> from;
             std::vector<ADD> to;
             for (auto const& metaVariablePair : metaVariablePairs) {
-                DdMetaVariable<CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
-                DdMetaVariable<CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
+                DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
+                DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
 
                 // Check if it's legal so swap the meta variables.
                 if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
@@ -230,7 +230,7 @@ namespace storm {
             this->cuddAdd = this->cuddAdd.SwapVariables(from, to);
         }
         
-        Dd<CUDD> Dd<CUDD>::multiplyMatrix(Dd<CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) {
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) {
             std::vector<ADD> summationDdVariables;
             
             // Create the CUDD summation variables.
@@ -245,10 +245,10 @@ namespace storm {
             std::set<std::string> containedMetaVariableNames;
             std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariableNames.begin(), summationMetaVariableNames.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin()));
             
-            return Dd<CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames);
         }
         
-        uint_fast64_t Dd<CUDD>::getNonZeroCount() const {
+        uint_fast64_t Dd<DdType::CUDD>::getNonZeroCount() const {
             std::size_t numberOfDdVariables = 0;
             for (auto const& metaVariableName : this->containedMetaVariableNames) {
                 numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariableName).getNumberOfDdVariables();
@@ -256,39 +256,39 @@ namespace storm {
             return static_cast<uint_fast64_t>(this->cuddAdd.CountMinterm(static_cast<int>(numberOfDdVariables)));
         }
         
-        uint_fast64_t Dd<CUDD>::getLeafCount() const {
+        uint_fast64_t Dd<DdType::CUDD>::getLeafCount() const {
             return static_cast<uint_fast64_t>(this->cuddAdd.CountLeaves());
         }
         
-        uint_fast64_t Dd<CUDD>::getNodeCount() const {
+        uint_fast64_t Dd<DdType::CUDD>::getNodeCount() const {
             return static_cast<uint_fast64_t>(this->cuddAdd.nodeCount());
         }
         
-        double Dd<CUDD>::getMin() const {
+        double Dd<DdType::CUDD>::getMin() const {
             ADD constantMinAdd = this->cuddAdd.FindMin();
             return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
         }
         
-        double Dd<CUDD>::getMax() const {
+        double Dd<DdType::CUDD>::getMax() const {
             ADD constantMaxAdd = this->cuddAdd.FindMax();
             return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
         }
         
-        void Dd<CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) {
+        void Dd<DdType::CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) {
             std::map<std::string, int_fast64_t> metaVariableNameToValueMap;
             metaVariableNameToValueMap.emplace(metaVariableName, variableValue);
             this->setValue(metaVariableNameToValueMap, targetValue);
         }
         
-        void Dd<CUDD>::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) {
+        void Dd<DdType::CUDD>::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) {
             std::map<std::string, int_fast64_t> metaVariableNameToValueMap;
             metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1);
             metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2);
             this->setValue(metaVariableNameToValueMap, targetValue);
         }
         
-        void Dd<CUDD>::setValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) {
-            Dd<CUDD> valueEncoding(this->getDdManager()->getOne());
+        void Dd<DdType::CUDD>::setValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) {
+            Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
             for (auto const& nameValuePair : metaVariableNameToValueMap) {
                 valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
                 // Also record that the DD now contains the meta variable.
@@ -298,9 +298,9 @@ namespace storm {
             this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd);
         }
         
-        double Dd<CUDD>::getValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap) const {
+        double Dd<DdType::CUDD>::getValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap) const {
             std::set<std::string> remainingMetaVariables(this->getContainedMetaVariableNames());
-            Dd<CUDD> valueEncoding(this->getDdManager()->getOne());
+            Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
             for (auto const& nameValuePair : metaVariableNameToValueMap) {
                 valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
                 if (this->containsMetaVariable(nameValuePair.first)) {
@@ -312,29 +312,29 @@ namespace storm {
                 throw storm::exceptions::InvalidArgumentException() << "Cannot evaluate function for which not all inputs were given.";
             }
             
-            Dd<CUDD> value = *this * valueEncoding;
+            Dd<DdType::CUDD> value = *this * valueEncoding;
             value.sumAbstract(this->getContainedMetaVariableNames());
             return static_cast<double>(Cudd_V(value.getCuddAdd().getNode()));
         }
         
-        bool Dd<CUDD>::isOne() const {
+        bool Dd<DdType::CUDD>::isOne() const {
             return *this == this->getDdManager()->getOne();
         }
         
-        bool Dd<CUDD>::isZero() const {
+        bool Dd<DdType::CUDD>::isZero() const {
             return *this == this->getDdManager()->getZero();
         }
         
-        bool Dd<CUDD>::isConstant() const {
+        bool Dd<DdType::CUDD>::isConstant() const {
             return Cudd_IsConstant(this->cuddAdd.getNode());
         }
         
-        bool Dd<CUDD>::containsMetaVariable(std::string const& metaVariableName) const {
+        bool Dd<DdType::CUDD>::containsMetaVariable(std::string const& metaVariableName) const {
             auto const& metaVariable = containedMetaVariableNames.find(metaVariableName);
             return metaVariable != containedMetaVariableNames.end();
         }
         
-        bool Dd<CUDD>::containsMetaVariables(std::set<std::string> metaVariableNames) const {
+        bool Dd<DdType::CUDD>::containsMetaVariables(std::set<std::string> metaVariableNames) const {
             for (auto const& metaVariableName : metaVariableNames) {
                 auto const& metaVariable = containedMetaVariableNames.find(metaVariableName);
                 
@@ -345,15 +345,15 @@ namespace storm {
             return true;
         }
         
-        std::set<std::string> const& Dd<CUDD>::getContainedMetaVariableNames() const {
+        std::set<std::string> const& Dd<DdType::CUDD>::getContainedMetaVariableNames() const {
             return this->containedMetaVariableNames;
         }
         
-        std::set<std::string>& Dd<CUDD>::getContainedMetaVariableNames() {
+        std::set<std::string>& Dd<DdType::CUDD>::getContainedMetaVariableNames() {
             return this->containedMetaVariableNames;
         }
         
-        void Dd<CUDD>::exportToDot(std::string const& filename) const {
+        void Dd<DdType::CUDD>::exportToDot(std::string const& filename) const {
 			std::vector<ADD> cuddAddVector = { this->cuddAdd };
 			if (filename.empty()) {
 				this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
@@ -364,27 +364,27 @@ namespace storm {
             }
         }
         
-        ADD Dd<CUDD>::getCuddAdd() {
+        ADD Dd<DdType::CUDD>::getCuddAdd() {
             return this->cuddAdd;
         }
         
-        ADD const& Dd<CUDD>::getCuddAdd() const {
+        ADD const& Dd<DdType::CUDD>::getCuddAdd() const {
             return this->cuddAdd;
         }
         
-        void Dd<CUDD>::addContainedMetaVariable(std::string const& metaVariableName) {
+        void Dd<DdType::CUDD>::addContainedMetaVariable(std::string const& metaVariableName) {
             this->getContainedMetaVariableNames().insert(metaVariableName);
         }
 
-        void Dd<CUDD>::removeContainedMetaVariable(std::string const& metaVariableName) {
+        void Dd<DdType::CUDD>::removeContainedMetaVariable(std::string const& metaVariableName) {
             this->getContainedMetaVariableNames().erase(metaVariableName);
         }
         
-        std::shared_ptr<DdManager<CUDD>> Dd<CUDD>::getDdManager() const {
+        std::shared_ptr<DdManager<DdType::CUDD>> Dd<DdType::CUDD>::getDdManager() const {
             return this->ddManager;
         }
         
-        std::ostream & operator<<(std::ostream& out, const Dd<CUDD>& dd) {
+        std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
             dd.exportToDot();
             return out;
         }

src/storage/dd/CuddDd.h

@@ -18,18 +18,18 @@ namespace storm {
         template<DdType Type> class DdManager;
         
         template<>
-        class Dd<CUDD> {
+        class Dd<DdType::CUDD> {
         public:
             // Declare the DdManager class as friend so it can access the internals of a DD.
-            friend class DdManager<CUDD>;
+            friend class DdManager<DdType::CUDD>;
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
             Dd() = default;
-            Dd(Dd<CUDD> const& other) = default;
-			Dd& operator=(Dd<CUDD> const& other) = default;
+            Dd(Dd<DdType::CUDD> const& other) = default;
+			Dd& operator=(Dd<DdType::CUDD> const& other) = default;
 #ifndef WINDOWS
-            Dd(Dd<CUDD>&& other) = default;
-            Dd& operator=(Dd<CUDD>&& other) = default;
+            Dd(Dd<DdType::CUDD>&& other) = default;
+            Dd& operator=(Dd<DdType::CUDD>&& other) = default;
 #endif
             
             /*!
@@ -38,7 +38,7 @@ namespace storm {
              * @param other The DD that is to be compared with the current one.
              * @return True if the DDs represent the same function.
              */
-            bool operator==(Dd<CUDD> const& other) const;
+            bool operator==(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Retrieves whether the two DDs represent different functions.
@@ -46,7 +46,7 @@ namespace storm {
              * @param other The DD that is to be compared with the current one.
              * @return True if the DDs represent the different functions.
              */
-            bool operator!=(Dd<CUDD> const& other) const;
+            bool operator!=(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Adds the two DDs.
@@ -54,7 +54,7 @@ namespace storm {
              * @param other The DD to add to the current one.
              * @return The result of the addition.
              */
-            Dd<CUDD> operator+(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> operator+(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Adds the given DD to the current one.
@@ -62,7 +62,7 @@ namespace storm {
              * @param other The DD to add to the current one.
              * @return A reference to the current DD after the operation.
              */
-            Dd<CUDD>& operator+=(Dd<CUDD> const& other);
+            Dd<DdType::CUDD>& operator+=(Dd<DdType::CUDD> const& other);
             
             /*!
              * Multiplies the two DDs.
@@ -70,7 +70,7 @@ namespace storm {
              * @param other The DD to multiply with the current one.
              * @return The result of the multiplication.
              */
-            Dd<CUDD> operator*(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> operator*(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Multiplies the given DD with the current one and assigns the result to the current DD.
@@ -78,7 +78,7 @@ namespace storm {
              * @param other The DD to multiply with the current one.
              * @return A reference to the current DD after the operation.
              */
-            Dd<CUDD>& operator*=(Dd<CUDD> const& other);
+            Dd<DdType::CUDD>& operator*=(Dd<DdType::CUDD> const& other);
             
             /*!
              * Subtracts the given DD from the current one.
@@ -86,7 +86,7 @@ namespace storm {
              * @param other The DD to subtract from the current one.
              * @return The result of the subtraction.
              */
-            Dd<CUDD> operator-(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> operator-(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Subtracts the given DD from the current one and assigns the result to the current DD.
@@ -94,7 +94,7 @@ namespace storm {
              * @param other The DD to subtract from the current one.
              * @return A reference to the current DD after the operation.
              */
-            Dd<CUDD>& operator-=(Dd<CUDD> const& other);
+            Dd<DdType::CUDD>& operator-=(Dd<DdType::CUDD> const& other);
             
             /*!
              * Divides the current DD by the given one.
@@ -102,7 +102,7 @@ namespace storm {
              * @param other The DD by which to divide the current one.
              * @return The result of the division.
              */
-            Dd<CUDD> operator/(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> operator/(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Divides the current DD by the given one and assigns the result to the current DD.
@@ -110,14 +110,14 @@ namespace storm {
              * @param other The DD by which to divide the current one.
              * @return A reference to the current DD after the operation.
              */
-            Dd<CUDD>& operator/=(Dd<CUDD> const& other);
+            Dd<DdType::CUDD>& operator/=(Dd<DdType::CUDD> const& other);
             
             /*!
              * Subtracts the DD from the constant zero function.
              *
              * @return The resulting function represented as a DD.
              */
-            Dd<CUDD> minus() const;
+            Dd<DdType::CUDD> minus() const;
             
             /*!
              * Retrieves the logical complement of the current DD. The result will map all encodings with a value
@@ -125,7 +125,7 @@ namespace storm {
              *
              * @return The logical complement of the current DD.
              */
-            Dd<CUDD> operator~() const;
+            Dd<DdType::CUDD> operator~() const;
             
             /*!
              * Logically complements the current DD. The result will map all encodings with a value
@@ -133,7 +133,7 @@ namespace storm {
              *
              * @return A reference to the current DD after the operation.
              */
-            Dd<CUDD>& complement();
+            Dd<DdType::CUDD>& complement();
             
             /*!
              * Retrieves the function that maps all evaluations to one that have an identical function values.
@@ -141,7 +141,7 @@ namespace storm {
              * @param other The DD with which to perform the operation.
              * @return The resulting function represented as a DD.
              */
-            Dd<CUDD> equals(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> equals(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Retrieves the function that maps all evaluations to one that have distinct function values.
@@ -149,7 +149,7 @@ namespace storm {
              * @param other The DD with which to perform the operation.
              * @return The resulting function represented as a DD.
              */
-            Dd<CUDD> notEquals(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> notEquals(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Retrieves the function that maps all evaluations to one whose function value in the first DD are less
@@ -158,7 +158,7 @@ namespace storm {
              * @param other The DD with which to perform the operation.
              * @return The resulting function represented as a DD.
              */
-            Dd<CUDD> less(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> less(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Retrieves the function that maps all evaluations to one whose function value in the first DD are less or
@@ -167,7 +167,7 @@ namespace storm {
              * @param other The DD with which to perform the operation.
              * @return The resulting function represented as a DD.
              */
-            Dd<CUDD> lessOrEqual(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> lessOrEqual(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater
@@ -176,7 +176,7 @@ namespace storm {
              * @param other The DD with which to perform the operation.
              * @return The resulting function represented as a DD.
              */
-            Dd<CUDD> greater(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> greater(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Retrieves the function that maps all evaluations to one whose function value in the first DD are greater
@@ -185,7 +185,7 @@ namespace storm {
              * @param other The DD with which to perform the operation.
              * @return The resulting function represented as a DD.
              */
-            Dd<CUDD> greaterOrEqual(Dd<CUDD> const& other) const;
+            Dd<DdType::CUDD> greaterOrEqual(Dd<DdType::CUDD> const& other) const;
             
             /*!
              * Existentially abstracts from the given meta variables.
@@ -232,7 +232,7 @@ namespace storm {
              * matrix multiplication.
              * @return A DD representing the result of the matrix-matrix multiplication.
              */
-            Dd<CUDD> multiplyMatrix(Dd<CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames);
+            Dd<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames);
             
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
@@ -378,9 +378,9 @@ namespace storm {
              *
              * A pointer to the manager that is responsible for this DD.
              */
-            std::shared_ptr<DdManager<CUDD>> getDdManager() const;
+            std::shared_ptr<DdManager<DdType::CUDD>> getDdManager() const;
             
-            friend std::ostream & operator<<(std::ostream& out, const Dd<CUDD>& dd);
+            friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
         private:
             /*!
              * Retrieves a reference to the CUDD ADD object associated with this DD.
@@ -417,10 +417,10 @@ namespace storm {
              * @param cuddAdd The CUDD ADD to store.
              * @param
              */
-            Dd(std::shared_ptr<DdManager<CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames = std::set<std::string>());
+            Dd(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, ADD cuddAdd, std::set<std::string> const& containedMetaVariableNames = std::set<std::string>());
             
             // A pointer to the manager responsible for this DD.
-            std::shared_ptr<DdManager<CUDD>> ddManager;
+            std::shared_ptr<DdManager<DdType::CUDD>> ddManager;
             
             // The ADD created by CUDD.
             ADD cuddAdd;

src/storage/dd/CuddDdManager.cpp

@@ -6,29 +6,29 @@
 
 namespace storm {
     namespace dd {
-        DdManager<CUDD>::DdManager() : metaVariableMap(), cuddManager() {
+        DdManager<DdType::CUDD>::DdManager() : metaVariableMap(), cuddManager() {
             // Intentionally left empty.
         }
         
-        Dd<CUDD> DdManager<CUDD>::getOne() {
-            return Dd<CUDD>(this->shared_from_this(), cuddManager.addOne());
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne() {
+            return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addOne());
         }
         
-        Dd<CUDD> DdManager<CUDD>::getZero() {
-            return Dd<CUDD>(this->shared_from_this(), cuddManager.addZero());
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getZero() {
+            return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addZero());
         }
         
-        Dd<CUDD> DdManager<CUDD>::getConstant(double value) {
-            return Dd<CUDD>(this->shared_from_this(), cuddManager.constant(value));
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getConstant(double value) {
+            return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.constant(value));
         }
         
-        Dd<CUDD> DdManager<CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(std::string const& metaVariableName, int_fast64_t value) {
             // Check whether the meta variable exists.
             if (!this->hasMetaVariable(metaVariableName)) {
                 throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
             }
             
-            DdMetaVariable<CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
+            DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
             
             // Check whether the value is legal for this meta variable.
             if (value < metaVariable.getLow() || value > metaVariable.getHigh()) {
@@ -38,9 +38,9 @@ namespace storm {
             // Now compute the encoding relative to the low value of the meta variable.
             value -= metaVariable.getLow();
             
-            std::vector<Dd<CUDD>> const& ddVariables = metaVariable.getDdVariables();
+            std::vector<Dd<DdType::CUDD>> const& ddVariables = metaVariable.getDdVariables();
 
-            Dd<CUDD> result;
+            Dd<DdType::CUDD> result;
             if (value & (1ull << (ddVariables.size() - 1))) {
                 result = ddVariables[0];
             } else {
@@ -58,15 +58,15 @@ namespace storm {
             return result;
         }
         
-        Dd<CUDD> DdManager<CUDD>::getRange(std::string const& metaVariableName) {
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(std::string const& metaVariableName) {
             // Check whether the meta variable exists.
             if (!this->hasMetaVariable(metaVariableName)) {
                 throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
             }
 
-            storm::dd::DdMetaVariable<CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
+            storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
             
-            Dd<CUDD> result = this->getZero();
+            Dd<DdType::CUDD> result = this->getZero();
             
             for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
                 result.setValue(metaVariableName, value, static_cast<double>(1));
@@ -74,22 +74,22 @@ namespace storm {
             return result;
         }
         
-        Dd<CUDD> DdManager<CUDD>::getIdentity(std::string const& metaVariableName) {
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(std::string const& metaVariableName) {
             // Check whether the meta variable exists.
             if (!this->hasMetaVariable(metaVariableName)) {
                 throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
             }
             
-            storm::dd::DdMetaVariable<CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
+            storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
             
-            Dd<CUDD> result = this->getZero();
+            Dd<DdType::CUDD> result = this->getZero();
             for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
                 result.setValue(metaVariableName, value, static_cast<double>(value));
             }
             return result;
         }
 
-        void DdManager<CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
+        void DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
             // Check whether a meta variable already exists.
             if (this->hasMetaVariable(name)) {
                 throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists.";
@@ -102,15 +102,15 @@ namespace storm {
             
             std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
             
-            std::vector<Dd<CUDD>> variables;
+            std::vector<Dd<DdType::CUDD>> variables;
             for (std::size_t i = 0; i < numberOfBits; ++i) {
-                variables.emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
+                variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {name}));
             }
             
-            metaVariableMap.emplace(name, DdMetaVariable<CUDD>(name, low, high, variables, this->shared_from_this()));
+            metaVariableMap.emplace(name, DdMetaVariable<DdType::CUDD>(name, low, high, variables, this->shared_from_this()));
         }
         
-        void DdManager<CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) {
+        void DdManager<DdType::CUDD>::addMetaVariablesInterleaved(std::vector<std::string> const& names, int_fast64_t low, int_fast64_t high) {
             // Make sure that at least one meta variable is added.
             if (names.size() == 0) {
                 throw storm::exceptions::InvalidArgumentException() << "Illegal to add zero meta variables.";
@@ -137,20 +137,20 @@ namespace storm {
             
             // Add the variables in interleaved order.
             std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
-            std::vector<std::vector<Dd<CUDD>>> variables(names.size());
+            std::vector<std::vector<Dd<DdType::CUDD>>> variables(names.size());
             for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
                 for (uint_fast64_t i = 0; i < names.size(); ++i) {
-                    variables[i].emplace_back(Dd<CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]}));
+                    variables[i].emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {names[i]}));
                 }
             }
             
             // Now add the meta variables.
             for (uint_fast64_t i = 0; i < names.size(); ++i) {
-                metaVariableMap.emplace(names[i], DdMetaVariable<CUDD>(names[i], low, high, variables[i], this->shared_from_this()));
+                metaVariableMap.emplace(names[i], DdMetaVariable<DdType::CUDD>(names[i], low, high, variables[i], this->shared_from_this()));
             }
         }
         
-        DdMetaVariable<CUDD> const& DdManager<CUDD>::getMetaVariable(std::string const& metaVariableName) const {
+        DdMetaVariable<DdType::CUDD> const& DdManager<DdType::CUDD>::getMetaVariable(std::string const& metaVariableName) const {
             auto const& nameVariablePair = metaVariableMap.find(metaVariableName);
             
             if (!this->hasMetaVariable(metaVariableName)) {
@@ -160,7 +160,7 @@ namespace storm {
             return nameVariablePair->second;
         }
         
-        std::set<std::string> DdManager<CUDD>::getAllMetaVariableNames() const {
+        std::set<std::string> DdManager<DdType::CUDD>::getAllMetaVariableNames() const {
             std::set<std::string> result;
             for (auto const& nameValuePair : metaVariableMap) {
                 result.insert(nameValuePair.first);
@@ -168,15 +168,15 @@ namespace storm {
             return result;
         }
         
-        std::size_t DdManager<CUDD>::getNumberOfMetaVariables() const {
+        std::size_t DdManager<DdType::CUDD>::getNumberOfMetaVariables() const {
             return this->metaVariableMap.size();
         }
         
-        bool DdManager<CUDD>::hasMetaVariable(std::string const& metaVariableName) const {
+        bool DdManager<DdType::CUDD>::hasMetaVariable(std::string const& metaVariableName) const {
             return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end();
         }
         
-        Cudd& DdManager<CUDD>::getCuddManager() {
+        Cudd& DdManager<DdType::CUDD>::getCuddManager() {
             return this->cuddManager;
         }
     }

src/storage/dd/CuddDdManager.h

@@ -14,10 +14,10 @@
 namespace storm {
     namespace dd {
         template<>
-        class DdManager<CUDD> : public std::enable_shared_from_this<DdManager<CUDD>> {
+        class DdManager<DdType::CUDD> : public std::enable_shared_from_this<DdManager<DdType::CUDD>> {
         public:
             // To break the cylic dependencies, we need to forward-declare the other DD-related classes.
-            friend class Dd<CUDD>;
+            friend class Dd<DdType::CUDD>;
             
             /*!
              * Creates an empty manager without any meta variables.
@@ -25,11 +25,11 @@ namespace storm {
             DdManager();
             
             // Explictly forbid copying a DdManager, but allow moving it.
-            DdManager(DdManager<CUDD> const& other) = delete;
-			DdManager<CUDD>& operator=(DdManager<CUDD> const& other) = delete;
+            DdManager(DdManager<DdType::CUDD> const& other) = delete;
+			DdManager<DdType::CUDD>& operator=(DdManager<DdType::CUDD> const& other) = delete;
 #ifndef WINDOWS
-            DdManager(DdManager<CUDD>&& other) = default;
-            DdManager<CUDD>& operator=(DdManager<CUDD>&& other) = default;
+            DdManager(DdManager<DdType::CUDD>&& other) = default;
+            DdManager<DdType::CUDD>& operator=(DdManager<DdType::CUDD>&& other) = default;
 #endif
             
             /*!
@@ -37,21 +37,21 @@ namespace storm {
              *
              * @return A DD representing the constant one function.
              */
-            Dd<CUDD> getOne();
+            Dd<DdType::CUDD> getOne();
             
             /*!
              * Retrieves a DD representing the constant zero function.
              *
              * @return A DD representing the constant zero function.
              */
-            Dd<CUDD> getZero();
+            Dd<DdType::CUDD> getZero();
             
             /*!
              * Retrieves a DD representing the constant function with the given value.
              *
              * @return A DD representing the constant function with the given value.
              */
-            Dd<CUDD> getConstant(double value);
+            Dd<DdType::CUDD> getConstant(double value);
             
             /*!
              * Retrieves the DD representing the function that maps all inputs which have the given meta variable equal
@@ -62,7 +62,7 @@ namespace storm {
              * @return The DD representing the function that maps all inputs which have the given meta variable equal
              * to the given value one.
              */
-            Dd<CUDD> getEncoding(std::string const& metaVariableName, int_fast64_t value);
+            Dd<DdType::CUDD> getEncoding(std::string const& metaVariableName, int_fast64_t value);
             
             /*!
              * Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values
@@ -71,7 +71,7 @@ namespace storm {
              * @param metaVariableName The name of the meta variable whose range to retrieve.
              * @return The range of the meta variable.
              */
-            Dd<CUDD> getRange(std::string const& metaVariableName);
+            Dd<DdType::CUDD> getRange(std::string const& metaVariableName);
 
             /*!
              * Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal
@@ -80,7 +80,7 @@ namespace storm {
              * @param metaVariableName The name of the meta variable whose identity to retrieve.
              * @return The identity of the meta variable.
              */
-            Dd<CUDD> getIdentity(std::string const& metaVariableName);
+            Dd<DdType::CUDD> getIdentity(std::string const& metaVariableName);
             
             /*!
              * Adds a meta variable with the given name and range.
@@ -106,7 +106,7 @@ namespace storm {
              * @param metaVariableName The name of the meta variable to retrieve.
              * @return The meta variable with the given name.
              */
-            DdMetaVariable<CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
+            DdMetaVariable<DdType::CUDD> const& getMetaVariable(std::string const& metaVariableName) const;
             
             /*!
              * Retrieves the names of all meta variables that have been added to the manager.
@@ -139,7 +139,7 @@ namespace storm {
             Cudd& getCuddManager();
             
             // A mapping from variable names to the meta variable information.
-            std::unordered_map<std::string, DdMetaVariable<CUDD>> metaVariableMap;
+            std::unordered_map<std::string, DdMetaVariable<DdType::CUDD>> metaVariableMap;
             
             // The manager responsible for the DDs created/modified with this DdManager.
             Cudd cuddManager;

src/storage/dd/DdMetaVariable.cpp

@@ -47,6 +47,6 @@ namespace storm {
         }
         
         // Explicitly instantiate DdMetaVariable.
-        template class DdMetaVariable<CUDD>;
+        template class DdMetaVariable<DdType::CUDD>;
     }
 }

src/storage/dd/DdType.h

@@ -3,7 +3,7 @@
 
 namespace storm {
     namespace dd {
-        enum DdType {
+        enum class DdType {
             CUDD
         };
     }

src/storage/expressions/Expression.cpp

@@ -3,6 +3,7 @@
 
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/SubstitutionVisitor.h"
+#include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
 #include "src/exceptions/InvalidTypeException.h"
 #include "src/exceptions/ExceptionMacros.h"
 
@@ -30,6 +31,11 @@ namespace storm {
             return SubstitutionVisitor<MapType>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
         }
         
+        template<template<typename... Arguments> class MapType>
+        Expression Expression::substitute(MapType<std::string, std::string> const& identifierToIdentifierMap) const {
+            return IdentifierSubstitutionVisitor<MapType>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
+        }
+        
         bool Expression::evaluateAsBool(Valuation const& valuation) const {
             return this->getBaseExpression().evaluateAsBool(valuation);
         }
@@ -222,6 +228,8 @@ namespace storm {
         
         template Expression Expression::substitute<std::map>(std::map<std::string, storm::expressions::Expression> const&) const;
         template Expression Expression::substitute<std::unordered_map>(std::unordered_map<std::string, storm::expressions::Expression> const&) const;
+        template Expression Expression::substitute<std::map>(std::map<std::string, std::string> const&) const;
+        template Expression Expression::substitute<std::unordered_map>(std::unordered_map<std::string, std::string> const&) const;
         
         std::ostream& operator<<(std::ostream& stream, Expression const& expression) {
             stream << expression.getBaseExpression();

src/storage/expressions/Expression.h

@@ -71,6 +71,16 @@ namespace storm {
             template<template<typename... Arguments> class MapType>
             Expression substitute(MapType<std::string, Expression> const& identifierToExpressionMap) const;
             
+            /*!
+             * Substitutes all occurrences of identifiers with different names given by a mapping.
+             *
+             * @param identifierToIdentifierMap A mapping from identifiers to identifiers they are substituted with.
+             * @return An expression in which all identifiers in the key set of the mapping are replaced by the
+             * identifiers they are mapped to.
+             */
+            template<template<typename... Arguments> class MapType>
+            Expression substitute(MapType<std::string, std::string> const& identifierToIdentifierMap) const;
+            
             /*!
              * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
              * valuation and returns the resulting boolean value. If the return type of the expression is not a boolean

src/storage/expressions/IdentifierSubstitutionVisitor.cpp

@@ -0,0 +1,177 @@
+#include <map>
+#include <unordered_map>
+
+#include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
+
+#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
+#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/BinaryRelationExpression.h"
+#include "src/storage/expressions/BooleanConstantExpression.h"
+#include "src/storage/expressions/IntegerConstantExpression.h"
+#include "src/storage/expressions/DoubleConstantExpression.h"
+#include "src/storage/expressions/BooleanLiteralExpression.h"
+#include "src/storage/expressions/IntegerLiteralExpression.h"
+#include "src/storage/expressions/DoubleLiteralExpression.h"
+#include "src/storage/expressions/VariableExpression.h"
+#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
+#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
+
+namespace storm {
+    namespace expressions  {
+        template<template<typename... Arguments> class MapType>
+        IdentifierSubstitutionVisitor<MapType>::IdentifierSubstitutionVisitor(MapType<std::string, std::string> const& identifierToIdentifierMap) : identifierToIdentifierMap(identifierToIdentifierMap) {
+            // Intentionally left empty.
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        Expression IdentifierSubstitutionVisitor<MapType>::substitute(BaseExpression const* expression) {
+            expression->accept(this);
+            return Expression(this->expressionStack.top());
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            expression->getSecondOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> secondExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            // If the arguments did not change, we simply push the expression itself.
+            if (firstExpression.get() == expression->getFirstOperand().get() && secondExpression.get() == expression->getSecondOperand().get()) {
+                this->expressionStack.push(expression->getSharedPointer());
+            } else {
+                this->expressionStack.push(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(expression->getReturnType(), firstExpression, secondExpression, expression->getOperatorType())));
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            expression->getSecondOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> secondExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            // If the arguments did not change, we simply push the expression itself.
+            if (firstExpression.get() == expression->getFirstOperand().get() && secondExpression.get() == expression->getSecondOperand().get()) {
+                this->expressionStack.push(expression->getSharedPointer());
+            } else {
+                this->expressionStack.push(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(expression->getReturnType(), firstExpression, secondExpression, expression->getOperatorType())));
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> firstExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            expression->getSecondOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> secondExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            // If the arguments did not change, we simply push the expression itself.
+            if (firstExpression.get() == expression->getFirstOperand().get() && secondExpression.get() == expression->getSecondOperand().get()) {
+                this->expressionStack.push(expression->getSharedPointer());
+            } else {
+                this->expressionStack.push(std::shared_ptr<BaseExpression>(new BinaryRelationExpression(expression->getReturnType(), firstExpression, secondExpression, expression->getRelationType())));
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
+            // If the boolean constant is in the key set of the substitution, we need to replace it.
+            auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
+            if (namePair != this->identifierToIdentifierMap.end()) {
+                this->expressionStack.push(std::shared_ptr<BaseExpression>(new BooleanConstantExpression(namePair->second)));
+            } else {
+                this->expressionStack.push(expression->getSharedPointer());
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
+            // If the double constant is in the key set of the substitution, we need to replace it.
+            auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
+            if (namePair != this->identifierToIdentifierMap.end()) {
+                this->expressionStack.push(std::shared_ptr<BaseExpression>(new DoubleConstantExpression(namePair->second)));
+            } else {
+                this->expressionStack.push(expression->getSharedPointer());
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
+            // If the integer constant is in the key set of the substitution, we need to replace it.
+            auto const& namePair = this->identifierToIdentifierMap.find(expression->getConstantName());
+            if (namePair != this->identifierToIdentifierMap.end()) {
+                this->expressionStack.push(std::shared_ptr<BaseExpression>(new IntegerConstantExpression(namePair->second)));
+            } else {
+                this->expressionStack.push(expression->getSharedPointer());
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(VariableExpression const* expression) {
+            // If the variable is in the key set of the substitution, we need to replace it.
+            auto const& namePair = this->identifierToIdentifierMap.find(expression->getVariableName());
+            if (namePair != this->identifierToIdentifierMap.end()) {
+                this->expressionStack.push(std::shared_ptr<BaseExpression>(new VariableExpression(expression->getReturnType(), namePair->second)));
+            } else {
+                this->expressionStack.push(expression->getSharedPointer());
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
+            expression->getOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            // If the argument did not change, we simply push the expression itself.
+            if (operandExpression.get() == expression->getOperand().get()) {
+                expressionStack.push(expression->getSharedPointer());
+            } else {
+                expressionStack.push(std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(expression->getReturnType(), operandExpression, expression->getOperatorType())));
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
+            expression->getOperand()->accept(this);
+            std::shared_ptr<BaseExpression const> operandExpression = expressionStack.top();
+            expressionStack.pop();
+            
+            // If the argument did not change, we simply push the expression itself.
+            if (operandExpression.get() == expression->getOperand().get()) {
+                expressionStack.push(expression->getSharedPointer());
+            } else {
+                expressionStack.push(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(expression->getReturnType(), operandExpression, expression->getOperatorType())));
+            }
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
+            this->expressionStack.push(expression->getSharedPointer());
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
+            this->expressionStack.push(expression->getSharedPointer());
+        }
+        
+        template<template<typename... Arguments> class MapType>
+        void IdentifierSubstitutionVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
+            this->expressionStack.push(expression->getSharedPointer());
+        }
+        
+        // Explicitly instantiate the class with map and unordered_map.
+        template class IdentifierSubstitutionVisitor<std::map>;
+        template class IdentifierSubstitutionVisitor<std::unordered_map>;
+    }
+}

src/storage/expressions/IdentifierSubstitutionVisitor.h

@@ -0,0 +1,54 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_
+#define STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_
+
+#include <stack>
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/ExpressionVisitor.h"
+
+namespace storm {
+    namespace expressions {
+        template<template<typename... Arguments> class MapType>
+        class IdentifierSubstitutionVisitor : public ExpressionVisitor {
+        public:
+            /*!
+             * Creates a new substitution visitor that uses the given map to replace identifiers.
+             *
+             * @param identifierToExpressionMap A mapping from identifiers to expressions.
+             */
+            IdentifierSubstitutionVisitor(MapType<std::string, std::string> const& identifierToExpressionMap);
+            
+            /*!
+             * Substitutes the identifiers in the given expression according to the previously given map and returns the
+             * resulting expression.
+             *
+             * @param expression The expression in which to substitute the identifiers.
+             * @return The expression in which all identifiers in the key set of the previously given mapping are
+             * substituted with the mapped-to expressions.
+             */
+            Expression substitute(BaseExpression const* expression);
+            
+            virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BinaryRelationExpression const* expression) override;
+            virtual void visit(BooleanConstantExpression const* expression) override;
+            virtual void visit(DoubleConstantExpression const* expression) override;
+            virtual void visit(IntegerConstantExpression const* expression) override;
+            virtual void visit(VariableExpression const* expression) override;
+            virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(UnaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BooleanLiteralExpression const* expression) override;
+            virtual void visit(IntegerLiteralExpression const* expression) override;
+            virtual void visit(DoubleLiteralExpression const* expression) override;
+            
+        private:
+            // A stack of expression used to pass the results to the higher levels.
+            std::stack<std::shared_ptr<BaseExpression const>> expressionStack;
+            
+            // A mapping of identifier names to expressions with which they shall be replaced.
+            MapType<std::string, std::string> const& identifierToIdentifierMap;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_IDENTIFIERSUBSTITUTIONVISITOR_H_ */

src/storage/prism/Assignment.cpp

@@ -0,0 +1,30 @@
+#include "Assignment.h"
+
+namespace storm {
+    namespace prism {
+        Assignment::Assignment(std::string const& variableName, storm::expressions::Expression const& expression) : variableName(variableName), expression(expression) {
+            // Intentionally left empty.
+        }
+        
+        Assignment::Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming) : variableName(oldAssignment.getVariableName()), expression(oldAssignment.getExpression().substitute<std::map>(renaming)) {
+            auto renamingPair = renaming.find(oldAssignment.variableName);
+            if (renamingPair != renaming.end()) {
+                this->variableName = renamingPair->second;
+            }
+        }
+        
+        std::string const& Assignment::getVariableName() const {
+            return variableName;
+        }
+        
+        storm::expressions::Expression const& Assignment::getExpression() const {
+            return this->expression;
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
+            stream << "(" << assignment.getVariableName() << "' = " << assignment.getExpression() << ")";
+            return stream;
+        }
+
+    } // namespace prism
+} // namespace storm

src/storage/prism/Assignment.h

@@ -0,0 +1,61 @@
+#ifndef STORM_STORAGE_PRISM_ASSIGNMENT_H_
+#define STORM_STORAGE_PRISM_ASSIGNMENT_H_
+
+#include <map>
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace prism {
+        class Assignment {
+        public:
+            /*!
+             * Constructs an assignment using the given variable name and expression.
+             *
+             * @param variableName The variable that this assignment targets.
+             * @param expression The expression to assign to the variable.
+             */
+            Assignment(std::string const& variableName, storm::expressions::Expression const& expression);
+            
+            /*!
+             * Creates a copy of the given assignment and performs the provided renaming.
+             *
+             * @param oldAssignment The assignment to copy.
+             * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+             */
+            Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming);
+            
+            // Create default implementations of constructors/assignment.
+            Assignment() = default;
+            Assignment(Assignment const& otherVariable) = default;
+            Assignment& operator=(Assignment const& otherVariable)= default;
+            Assignment(Assignment&& otherVariable) = default;
+            Assignment& operator=(Assignment&& otherVariable) = default;
+            
+            /*!
+             * Retrieves the name of the variable that this assignment targets.
+             *
+             * @return The name of the variable that this assignment targets.
+             */
+            std::string const& getVariableName() const;
+            
+            /*!
+             * Retrieves the expression that is assigned to the variable.
+             *
+             * @return The expression that is assigned to the variable.
+             */
+            storm::expressions::Expression const& getExpression() const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
+            
+        private:
+            // The name of the variable that this assignment targets.
+            std::string variableName;
+            
+            // The expression that is assigned to the variable.
+            storm::expressions::Expression expression;
+        };
+    } // namespace ir
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_ASSIGNMENT_H_ */

src/storage/prism/BooleanVariable.cpp

@@ -0,0 +1,23 @@
+#include "src/storage/prism/BooleanVariable.h"
+
+namespace storm {
+    namespace prism {
+        BooleanVariable::BooleanVariable(std::string const& variableName) : BooleanVariable(variableName, storm::expressions::Expression::createFalse()) {
+            // Nothing to do here.
+        }
+
+        BooleanVariable::BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression) {
+            // Nothing to do here.
+        }
+        
+        BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming) : Variable(oldVariable, newName, renaming) {
+            // Nothing to do here.
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) {
+            stream << variable.getName() << ": bool " << variable.getInitialValueExpression() << ";";
+            return stream;
+        }
+        
+    } // namespace prism
+} // namespace storm

src/storage/prism/BooleanVariable.h

@@ -0,0 +1,50 @@
+#ifndef STORM_STORAGE_PRISM_BOOLEANVARIABLE_H_
+#define STORM_STORAGE_PRISM_BOOLEANVARIABLE_H_
+
+#include <map>
+
+#include "src/storage/prism/Variable.h"
+
+namespace storm {
+    namespace prism {
+        class BooleanVariable : public Variable {
+        public:
+            // Create default implementations of constructors/assignment.
+            BooleanVariable() = default;
+            BooleanVariable(BooleanVariable const& otherVariable) = default;
+            BooleanVariable& operator=(BooleanVariable const& otherVariable)= default;
+            BooleanVariable(BooleanVariable&& otherVariable) = default;
+            BooleanVariable& operator=(BooleanVariable&& otherVariable) = default;
+            
+            /*!
+             * Creates a boolean variable with the given name and default initial value.
+             *
+             * @param variableName The name of the variable.
+             */
+            BooleanVariable(std::string const& variableName);
+
+            /*!
+             * Creates a boolean variable with the given name and the given constant initial value expression.
+             *
+             * @param variableName The name of the variable.
+             * @param initialValueExpression The constant expression that defines the initial value of the variable.
+             */
+            BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression);
+
+            /*!
+             * Creates a copy of the given boolean variable and performs the provided renaming.
+             *
+             * @param oldVariable The variable to copy.
+             * @param newName New name of this variable.
+             * @param renaming A mapping from names that are to be renamed to the names they are to be
+             * replaced with.
+             */
+            BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming);
+            
+            friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable);
+        };
+        
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_BOOLEANVARIABLE_H_ */

src/storage/prism/IntegerVariable.cpp

@@ -0,0 +1,30 @@
+#include "src/storage/prism/IntegerVariable.h"
+
+namespace storm {
+    namespace prism {
+        IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression) : IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, lowerBoundExpression) {
+            // Intentionally left empty.
+        }
+
+        IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
+            // Intentionally left empty.
+        }
+        
+        IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming) : Variable(oldVariable, newName, renaming), lowerBoundExpression(oldVariable.getLowerBoundExpression().substitute<std::map>(renaming)), upperBoundExpression(oldVariable.getUpperBoundExpression().substitute<std::map>(renaming)) {
+            // Intentionally left empty.
+        }
+        
+        storm::expressions::Expression const& IntegerVariable::getLowerBoundExpression() const {
+            return this->lowerBoundExpression;
+        }
+        
+        storm::expressions::Expression const& IntegerVariable::getUpperBoundExpression() const {
+            return this->upperBoundExpression;
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {
+            stream << this->getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << variable.getInitialValueExpression() << ";";
+            return stream;
+        }
+    } // namespace prism
+} // namespace storm

src/storage/prism/IntegerVariable.h

@@ -0,0 +1,74 @@
+#ifndef STORM_STORAGE_PRISM_INTEGERVARIABLE_H_
+#define STORM_STORAGE_PRISM_INTEGERVARIABLE_H_
+
+#include <map>
+
+#include "src/storage/prism/Variable.h"
+
+namespace storm {
+    namespace prism {
+        class IntegerVariable : public Variable {
+        public:
+            // Create default implementations of constructors/assignment.
+            IntegerVariable() = default;
+            IntegerVariable(IntegerVariable const& otherVariable) = default;
+            IntegerVariable& operator=(IntegerVariable const& otherVariable)= default;
+            IntegerVariable(IntegerVariable&& otherVariable) = default;
+            IntegerVariable& operator=(IntegerVariable&& otherVariable) = default;
+
+            /*!
+             * Creates an integer variable with the given name and a default initial value.
+             *
+             * @param variableName The name of the variable.
+             * @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable.
+             * @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable.
+             */
+            IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression);
+
+            /*!
+             * Creates an integer variable with the given name and the given initial value expression.
+             *
+             * @param variableName The name of the variable.
+             * @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable.
+             * @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable.
+             * @param initialValueExpression A constant expression that defines the initial value of the variable.
+             */
+            IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression);
+            
+            /*!
+             * Creates a copy of the given integer variable and performs the provided renaming.
+             *
+             * @param oldVariable The variable to copy.
+             * @param newName New name of this variable.
+             * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+             */
+            IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming);
+            
+            /*!
+             * Retrieves an expression defining the lower bound for this integer variable.
+             *
+             * @return An expression defining the lower bound for this integer variable.
+             */
+            storm::expressions::Expression const& getLowerBoundExpression() const;
+            
+            /*!
+             * Retrieves an expression defining the upper bound for this integer variable.
+             *
+             * @return An expression defining the upper bound for this integer variable.
+             */
+            storm::expressions::Expression const& getUpperBoundExpression() const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable);
+            
+        private:
+            // A constant expression that specifies the lower bound of the domain of the variable.
+            storm::expressions::Expression lowerBoundExpression;
+            
+            // A constant expression that specifies the upper bound of the domain of the variable.
+            storm::expressions::Expression upperBoundExpression;
+        };
+        
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_INTEGERVARIABLE_H_ */

src/storage/prism/Program.h

@@ -0,0 +1,227 @@
+/*
+ * Program.h
+ *
+ *  Created on: 04.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_IR_PROGRAM_H_
+#define STORM_IR_PROGRAM_H_
+
+#include <map>
+#include <vector>
+#include <memory>
+#include <set>
+#include <boost/container/flat_set.hpp>
+
+#include "src/storage/expressions/Expression.h"
+#include "Module.h"
+#include "RewardModel.h"
+
+namespace storm {
+    namespace ir {
+        
+        /*!
+         * A class representing a program.
+         */
+        class Program {
+        public:
+            
+            /*!
+             * An enum for the different model types.
+             */
+            enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP};
+            
+            /*!
+             * Creates a program with the given model type, undefined constants, modules, rewards and labels.
+             *
+             * @param modelType The type of the model that this program gives rise to.
+             * @param booleanUndefinedConstantExpressions A map of undefined boolean constants to their
+             * expression nodes.
+             * @param integerUndefinedConstantExpressions A map of undefined integer constants to their
+             * expression nodes.
+             * @param doubleUndefinedConstantExpressions A map of undefined double constants to their
+             * expression nodes.
+             * @param globalBooleanVariables A list of global boolean variables.
+             * @param globalIntegerVariables A list of global integer variables.
+             * @param globalBooleanVariableToIndexMap A mapping from global boolean variable names to the index in the
+             * list of global boolean variables.
+             * @param globalIntegerVariableToIndexMap A mapping from global integer variable names to the index in the
+             * list of global integer variables.
+             * @param modules The modules of the program.
+             * @param rewards The reward models of the program.
+             * @param labels The labels defined for this model.
+             */
+            Program(ModelType modelType,
+                    std::set<std::string> const& booleanUndefinedConstantExpressions,
+                    std::set<std::string> const& integerUndefinedConstantExpressions,
+                    std::set<std::string> const& doubleUndefinedConstantExpressions,
+                    std::map<std::string, BooleanVariable> const& globalBooleanVariables,
+                    std::map<std::string, IntegerVariable> const& globalIntegerVariables,
+                    std::vector<storm::ir::Module> const& modules,
+                    std::map<std::string, storm::ir::RewardModel> const& rewards,
+                    std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels);
+            
+            // Provide default implementations for constructors and assignments.
+            Program() = default;
+            Program(Program const& otherProgram) = default;
+            Program& operator=(Program const& otherProgram) = default;
+            Program(Program&& otherProgram) = default;
+            Program& operator=(Program&& otherProgram) = default;
+            
+            /*!
+             * Retrieves the model type of the model.
+             *
+             * @return The type of the model.
+             */
+            ModelType getModelType() const;
+
+            bool hasUndefinedConstants() const;
+            
+            bool hasUndefinedBooleanConstants() const;
+            bool hasUndefinedIntegerConstants() const;
+            bool hasUndefinedDoubleConstants() const;
+            
+            std::set<std::string> const& getUndefinedBooleanConstants() const;
+            std::set<std::string> const& getUndefinedIntegerConstants() const;
+            std::set<std::string> const& getUndefinedDoubleConstants() const;
+            
+            std::map<std::string, storm::ir::BooleanVariable> const& getGlobalBooleanVariables() const;
+            
+            /*!
+             * Retrieves a reference to the global boolean variable with the given index.
+             *
+             * @return A reference to the global boolean variable with the given index.
+             */
+            storm::ir::BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const;
+            
+            std::map<std::string, storm::ir::IntegerVariable> const& getGlobalIntegerVariables() const;
+
+            /*!
+             * Retrieves a reference to the global integer variable with the given index.
+             *
+             * @return A reference to the global integer variable with the given index.
+             */
+            storm::ir::IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const;
+
+            /*!
+             * Retrieves the number of global boolean variables of the program.
+             *
+             * @return The number of global boolean variables of the program.
+             */
+            uint_fast64_t getNumberOfGlobalBooleanVariables() const;
+            
+            /*!
+             * Retrieves the number of global integer variables of the program.
+             *
+             * @return The number of global integer variables of the program.
+             */
+            uint_fast64_t getNumberOfGlobalIntegerVariables() const;
+
+            /*!
+             * Retrieves the number of modules in the program.
+             *
+             * @return The number of modules in the program.
+             */
+            uint_fast64_t getNumberOfModules() const;
+            
+            /*!
+             * Retrieves a reference to the module with the given index.
+             *
+             * @param index The index of the module to retrieve.
+             * @return The module with the given index.
+             */
+            storm::ir::Module const& getModule(uint_fast64_t index) const;
+            
+            /*!
+             * Retrieves the set of actions present in the program.
+             *
+             * @return The set of actions present in the program.
+             */
+            std::set<std::string> const& getActions() const;
+            
+            /*!
+             * Retrieves the indices of all modules within this program that contain commands that are labelled with the given
+             * action.
+             *
+             * @param action The name of the action the modules are supposed to possess.
+             * @return A set of indices of all matching modules.
+             */
+            std::set<uint_fast64_t> const& getModuleIndicesByAction(std::string const& action) const;
+            
+            /*!
+             * Retrieves the index of the module in which the given variable name was declared.
+             *
+             * @param variableName The name of the variable to search.
+             * @return The index of the module in which the given variable name was declared.
+             */
+            uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
+            
+            std::map<std::string, storm::ir::RewardModel> const& getRewardModels() const;
+            
+            /*!
+             * Retrieves the reward model with the given name.
+             *
+             * @param name The name of the reward model to return.
+             * @return The reward model with the given name.
+             */
+            storm::ir::RewardModel const& getRewardModel(std::string const& name) const;
+            
+            /*!
+             * Retrieves all labels that are defined by the probabilitic program.
+             *
+             * @return A set of labels that are defined in the program.
+             */
+            std::map<std::string, Expression> const& getLabels() const;
+            
+            /*!
+             * Creates a new program that drops all commands whose indices are not in the given set.
+             *
+             * @param indexSet The set of indices for which to keep the commands.
+             */
+            Program restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet);
+            
+            friend std::ostream& operator<<(std::ostream& stream, Program const& program);
+            
+        private:
+            // The type of the model.
+            ModelType modelType;
+            
+            // A list of undefined boolean constants of the model.
+            std::set<std::string> undefinedBooleanConstants;
+            
+            // A list of undefined integer constants of the model.
+            std::set<std::string> undefinedIntegerConstants;
+
+            // A list of undefined double constants of the model.
+            std::set<std::string> undefinedDoubleConstants;
+            
+            // A list of global boolean variables.
+            std::map<std::string, BooleanVariable> globalBooleanVariables;
+            
+            // A list of global integer variables.
+            std::std::string, IntegerVariable> globalIntegerVariables;
+            
+            // The modules associated with the program.
+            std::vector<storm::ir::Module> modules;
+            
+            // The reward models associated with the program.
+            std::map<std::string, storm::ir::RewardModel> rewardModels;
+            
+            // The labels that are defined for this model.
+            std::map<std::string, Expression> labels;
+            
+            // The set of actions present in this program.
+            std::set<std::string> actions;
+            
+            // A map of actions to the set of modules containing commands labelled with this action.
+            std::map<std::string, std::set<uint_fast64_t>> actionsToModuleIndexMap;
+            
+            // A mapping from variable names to the modules in which they were declared.
+            std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
+        };
+        
+    } // namespace ir
+} // namespace storm
+
+#endif /* STORM_IR_PROGRAM_H_ */

src/storage/prism/StateReward.cpp

@@ -0,0 +1,38 @@
+/*
+ * StateReward.cpp
+ *
+ *  Created on: 12.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#include <sstream>
+
+#include "StateReward.h"
+
+namespace storm {
+    namespace ir {
+        
+        StateReward::StateReward() : statePredicate(), rewardValue() {
+            // Nothing to do here.
+        }
+        
+        StateReward::StateReward(storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) {
+            // Nothing to do here.
+        }
+        
+        std::string StateReward::toString() const {
+            std::stringstream result;
+            result << "\t" << statePredicate << ": " << rewardValue << ";";
+            return result.str();
+        }
+        
+        storm::expressions::Expression const& StateReward::getStatePredicate() const {
+            return this->statePredicate;
+        }
+        
+        storm::expressions::Expression const& StateReward::getRewardValue() const {
+            return this->rewardValue;
+        }
+        
+    } // namespace ir
+} // namespace storm

src/ir/StateReward.h → src/storage/prism/StateReward.h

@@ -10,7 +10,7 @@
 
 #include <memory>
 
-#include "expressions/BaseExpression.h"
+#include "src/storage/expressions/Expression.h"
 
 namespace storm {
     namespace ir {
@@ -34,21 +34,21 @@ namespace storm {
              * @param rewardValue An expression specifying the values of the rewards to attach to the
              * states.
              */
-            StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue);
+            StateReward(storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue);
             
             /*!
              * Performs a deep-copy of the given reward.
              *
              * @param otherReward The reward to copy.
              */
-            StateReward(StateReward const& otherReward);
+            StateReward(StateReward const& otherReward) = default;
 
             /*!
              * Performs a deep-copy of the given reward and assigns it to the current one.
              *
              * @param otherReward The reward to assign.
              */
-            StateReward& operator=(StateReward const& otherReward);
+            StateReward& operator=(StateReward const& otherReward) = default;
             
             /*!
              * Retrieves a string representation of this state reward.
@@ -62,21 +62,21 @@ namespace storm {
              *
              * @return The state predicate that is associated with this state reward.
              */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getStatePredicate() const;
+            storm::expressions::Expression const& getStatePredicate() const;
             
             /*!
              * Retrieves the reward value associated with this state reward.
              *
              * @return The reward value associated with this state reward.
              */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const;
+            storm::expressions::Expression const& getRewardValue() const;
             
         private:
             // The predicate that characterizes the states that obtain this reward.
-            std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate;
+            storm::expressions::Expression statePredicate;
             
             // The expression that specifies the value of the reward obtained.
-            std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue;
+            storm::expressions::Expression rewardValue;
         };
         
     } // namespace ir

src/storage/prism/TransitionReward.cpp

@@ -0,0 +1,42 @@
+/*
+ * TransitionReward.cpp
+ *
+ *  Created on: 12.01.2013
+ *      Author: Christian Dehnert
+ */
+
+#include <sstream>
+
+#include "TransitionReward.h"
+
+namespace storm {
+    namespace ir {
+        
+        TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
+            // Nothing to do here.
+        }
+        
+        TransitionReward::TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
+            // Nothing to do here.
+        }
+        
+        std::string TransitionReward::toString() const {
+            std::stringstream result;
+            result << "\t[" << commandName << "] " << statePredicate << ": " << rewardValue << ";";
+            return result.str();
+        }
+        
+        std::string const& TransitionReward::getActionName() const {
+            return this->commandName;
+        }
+        
+        storm::expressions::Expression const& TransitionReward::getStatePredicate() const {
+            return this->statePredicate;
+        }
+        
+        storm::expressions::Expression const& TransitionReward::getRewardValue() const {
+            return this->rewardValue;
+        }
+        
+    } // namespace ir
+} // namespace storm

src/ir/TransitionReward.h → src/storage/prism/TransitionReward.h

@@ -10,7 +10,7 @@
 
 #include <memory>
 
-#include "expressions/BaseExpression.h"
+#include "src/storage/expressions/Expression.h"
 
 namespace storm {
 
@@ -36,21 +36,21 @@ public:
 	 * @param rewardValue An expression specifying the values of the rewards to attach to the
 	 * transitions.
 	 */
-	TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue);
+	TransitionReward(std::string const& commandName, storm::expressions::Expression const& statePredicate, storm::expressions::Expression const& rewardValue);
 
     /*!
      * Performs a deep-copy of the given transition reward.
      *
      * @param otherReward The transition reward to copy.
      */
-    TransitionReward(TransitionReward const& otherReward);
+    TransitionReward(TransitionReward const& otherReward) = default;
     
     /*!
      * Performs a deep-copy of the given transition reward and assigns it to the current one.
      *
      * @param otherReward The reward to assign.
      */
-    TransitionReward& operator=(TransitionReward const& otherReward);
+    TransitionReward& operator=(TransitionReward const& otherReward) = default;
     
 	/*!
 	 * Retrieves a string representation of this transition reward.
@@ -71,14 +71,14 @@ public:
      *
      * @return The state predicate that is associated with this state reward.
      */
-    std::unique_ptr<storm::ir::expressions::BaseExpression> const& getStatePredicate() const;
+    storm::expressions::Expression const& getStatePredicate() const;
     
     /*!
      * Retrieves the reward value associated with this state reward.
      *
      * @return The reward value associated with this state reward.
      */
-    std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const;
+    storm::expressions::Expression const& getRewardValue() const;
 
 private:
 	// The name of the command this transition-based reward is attached to.
@@ -86,10 +86,10 @@ private:
 
 	// A predicate that needs to be satisfied by states for the reward to be obtained (by taking
 	// a corresponding command transition).
-	std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate;
+	storm::expressions::Expression statePredicate;
 
 	// The expression specifying the value of the reward obtained along the transitions.
-	std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue;
+	storm::expressions::Expression rewardValue;
 };
 
 } // namespace ir

src/storage/prism/Update.cpp

@@ -0,0 +1,94 @@
+#include "Update.h"
+#include "src/exceptions/OutOfRangeException.h"
+
+namespace storm {
+    namespace prism {
+        Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments) : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
+            // Nothing to do here.
+        }
+        
+        Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming) : likelihoodExpression(update.getLikelihoodExpression().substitute<std::map>(renaming)), booleanAssignments(), integerAssignments(), globalIndex(newGlobalIndex) {
+            for (auto const& variableAssignmentPair : update.getBooleanAssignments()) {
+                auto const& namePair = renaming.find(variableAssignmentPair.first);
+                if (namePair != renaming.end()) {
+                    this->booleanAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming));
+                } else {
+                    this->booleanAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming));
+                }
+            }
+            for (auto const& variableAssignmentPair : update.getIntegerAssignments()) {
+                auto const& namePair = renaming.find(variableAssignmentPair.first);
+                if (renaming.count(variableAssignmentPair.first) > 0) {
+                    this->integerAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming));
+                } else {
+                    this->integerAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming));
+                }
+            }
+            this->likelihoodExpression = update.getLikelihoodExpression().substitute<std::map>(renaming);
+        }
+        
+        storm::expressions::Expression const& Update::getLikelihoodExpression() const {
+            return likelihoodExpression;
+        }
+        
+        std::size_t Update::getNumberOfBooleanAssignments() const {
+            return booleanAssignments.size();
+        }
+        
+        std::size_t Update::getNumberOfIntegerAssignments() const {
+            return integerAssignments.size();
+        }
+        
+        std::map<std::string, storm::prism::Assignment> const& Update::getBooleanAssignments() const {
+            return booleanAssignments;
+        }
+        
+        std::map<std::string, storm::prism::Assignment> const& Update::getIntegerAssignments() const {
+            return integerAssignments;
+        }
+        
+        storm::prism::Assignment const& Update::getBooleanAssignment(std::string const& variableName) const {
+            auto variableAssignmentPair = booleanAssignments.find(variableName);
+            if (variableAssignmentPair == booleanAssignments.end()) {
+                throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '" << variableName << "' in update " << *this << ".";
+            }
+            
+            return variableAssignmentPair->second;
+        }
+        
+        storm::prism::Assignment const& Update::getIntegerAssignment(std::string const& variableName) const {
+            auto variableAssignmentPair = integerAssignments.find(variableName);
+            if (variableAssignmentPair == integerAssignments.end()) {
+                throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '" << variableName << "' in update " << *this << ".";
+            }
+            
+            return variableAssignmentPair->second;
+        }
+        
+        uint_fast64_t Update::getGlobalIndex() const {
+            return this->globalIndex;
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, Update const& update) {
+            stream << update.getLikelihoodExpression() << " : ";
+            uint_fast64_t i = 0;
+            for (auto const& assignment : update.getBooleanAssignments()) {
+                stream << assignment.second;
+                if (i < update.getBooleanAssignments().size() - 1 || update.getIntegerAssignments().size() > 0) {
+                    stream << " & ";
+                }
+                ++i;
+            }
+            i = 0;
+            for (auto const& assignment : update.getIntegerAssignments()) {
+                result << assignment.second;
+                if (i < update.getIntegerAssignments().size() - 1) {
+                    stream << " & ";
+                }
+                ++i;
+            }
+            return stream;
+        }
+        
+    } // namespace ir
+} // namespace storm

src/ir/Update.h → src/storage/prism/Update.h

@@ -1,122 +1,88 @@
-/*
- * Update.h
- *
- *  Created on: 06.01.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_IR_UPDATE_H_
-#define STORM_IR_UPDATE_H_
+#ifndef STORM_STORAGE_PRISM_UPDATE_H_
+#define STORM_STORAGE_PRISM_UPDATE_H_
 
 #include <map>
-#include <memory>
 
-#include "expressions/BaseExpression.h"
 #include "Assignment.h"
 
 namespace storm {
-    
-    namespace parser {
-        namespace prism {
-            class VariableState;
-        } // namespace prismparser
-    } // namespace parser
-    
-    namespace ir {
-        
-        /*!
-         * A class representing an update of a command.
-         */
+    namespace prism {
         class Update {
         public:
             /*!
-             * Default constructor. Creates an empty update.
-             */
-            Update();
-            
-            /*!
-             * Creates an update with the given expression specifying the likelihood and the mapping of
-             * variable to their assignments.
+             * Creates an update with the given expression specifying the likelihood and the mapping of variable to
+             * their assignments.
              *
              * @param globalIndex The global index of the update.
              * @param likelihoodExpression An expression specifying the likelihood of this update.
              * @param assignments A map of variable names to their assignments.
              */
-            Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments);
+            Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments);
             
             /*!
              * Creates a copy of the given update and performs the provided renaming.
              *
              * @param update The update that is to be copied.
              * @param newGlobalIndex The global index of the resulting update.
-             * @param renaming A mapping from names that are to be renamed to the names they are to be
-             * replaced with.
-             * @param variableState An object knowing about the variables in the system.
-             */
-            Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
-            
-            /*!
-             * Peforms a deep-copy of the given update.
-             *
-             * @param otherUpdate The update to copy.
+             * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
              */
-            Update(Update const& otherUpdate);
+            Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming);
             
-            /*!
-             * Performs a deep-copy of the given update and assigns it to the current one.
-             *
-             * @param otherUpdate The update to assign.
-             */
-            Update& operator=(Update const& otherUpdate);
+            // Create default implementations of constructors/assignment.
+            Update() = default;
+            Update(Update const& otherVariable) = default;
+            Update& operator=(Update const& otherVariable)= default;
+            Update(Update&& otherVariable) = default;
+            Update& operator=(Update&& otherVariable) = default;
             
             /*!
              * Retrieves the expression for the likelihood of this update.
              *
              * @return The expression for the likelihood of this update.
              */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
+            storm::expressions::Expression const& getLikelihoodExpression() const;
             
             /*!
              * Retrieves the number of boolean assignments associated with this update.
              *
              * @return The number of boolean assignments associated with this update.
              */
-            uint_fast64_t getNumberOfBooleanAssignments() const;
+            std::size_t getNumberOfBooleanAssignments() const;
             
             /*!
              * Retrieves the number of integer assignments associated with this update.
              *
              * @return The number of integer assignments associated with this update.
              */
-            uint_fast64_t getNumberOfIntegerAssignments() const;
+            std::size_t getNumberOfIntegerAssignments() const;
             
             /*!
              * Retrieves a reference to the map of boolean variable names to their respective assignments.
              *
              * @return A reference to the map of boolean variable names to their respective assignments.
              */
-            std::map<std::string, storm::ir::Assignment> const& getBooleanAssignments() const;
+            std::map<std::string, storm::prism::Assignment> const& getBooleanAssignments() const;
             
             /*!
              * Retrieves a reference to the map of integer variable names to their respective assignments.
              *
              * @return A reference to the map of integer variable names to their respective assignments.
              */
-            std::map<std::string, storm::ir::Assignment> const& getIntegerAssignments() const;
+            std::map<std::string, storm::prism::Assignment> const& getIntegerAssignments() const;
             
             /*!
              * Retrieves a reference to the assignment for the boolean variable with the given name.
              *
              * @return A reference to the assignment for the boolean variable with the given name.
              */
-            storm::ir::Assignment const& getBooleanAssignment(std::string const& variableName) const;
+            storm::prism::Assignment const& getBooleanAssignment(std::string const& variableName) const;
             
             /*!
              * Retrieves a reference to the assignment for the integer variable with the given name.
              *
              * @return A reference to the assignment for the integer variable with the given name.
              */
-            storm::ir::Assignment const& getIntegerAssignment(std::string const& variableName) const;
+            storm::prism::Assignment const& getIntegerAssignment(std::string const& variableName) const;
             
             /*!
              * Retrieves the global index of the update, that is, a unique index over all modules.
@@ -125,28 +91,22 @@ namespace storm {
              */
             uint_fast64_t getGlobalIndex() const;
             
-            /*!
-             * Retrieves a string representation of this update.
-             *
-             * @return A string representation of this update.
-             */
-            std::string toString() const;
+            friend std::ostream& operator<<(std::ostream& stream, Update const& assignment);
             
         private:
             // An expression specifying the likelihood of taking this update.
-            std::unique_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
+            storm::expressions::Expression likelihoodExpression;
             
             // A mapping of boolean variable names to their assignments in this update.
-            std::map<std::string, storm::ir::Assignment> booleanAssignments;
+            std::map<std::string, storm::prism::Assignment> booleanAssignments;
             
             // A mapping of integer variable names to their assignments in this update.
-            std::map<std::string, storm::ir::Assignment> integerAssignments;
+            std::map<std::string, storm::prism::Assignment> integerAssignments;
             
             // The global index of the update.
             uint_fast64_t globalIndex;
         };
-        
-    } // namespace ir
+    } // namespace prism
 } // namespace storm
 
-#endif /* STORM_IR_UPDATE_H_ */
+#endif /* STORM_STORAGE_PRISM_UPDATE_H_ */

src/storage/prism/Variable.cpp

@@ -0,0 +1,23 @@
+#include <map>
+
+#include "src/storage/prism/Variable.h"
+
+namespace storm {
+    namespace prism {
+        Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression) : variableName(variableName), initialValueExpression(initialValueExpression) {
+            // Nothing to do here.
+        }
+        
+        Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming) : variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)) {
+            // Intentionally left empty.
+        }
+        
+        std::string const& Variable::getName() const {
+            return variableName;
+        }
+        
+        storm::expressions::Expression const& Variable::getInitialValueExpression() const {
+            return this->initialValueExpression;
+        }
+    } // namespace prism
+} // namespace storm

src/storage/prism/Variable.h

@@ -0,0 +1,64 @@
+#ifndef STORM_STORAGE_PRISM_VARIABLE_H_
+#define STORM_STORAGE_PRISM_VARIABLE_H_
+
+#include <map>
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace prism {
+        class Variable {
+        public:
+            // Create default implementations of constructors/assignment.
+            Variable(Variable const& otherVariable) = default;
+            Variable& operator=(Variable const& otherVariable)= default;
+            Variable(Variable&& otherVariable) = default;
+            Variable& operator=(Variable&& otherVariable) = default;
+            
+            /*!
+             * Retrieves the name of the variable.
+             *
+             * @return The name of the variable.
+             */
+            std::string const& getName() const;
+            
+            /*!
+             * Retrieves the expression defining the initial value of the variable.
+             *
+             * @return The expression defining the initial value of the variable.
+             */
+            storm::expressions::Expression const& getInitialValueExpression() const;
+                        
+            // Make the constructors protected to forbid instantiation of this class.
+        protected:
+            Variable() = default;
+            
+            /*!
+             * Creates a variable with the given name and initial value.
+             *
+             * @param variableName The name of the variable.
+             * @param initialValueExpression The constant expression that defines the initial value of the variable.
+             */
+            Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression);
+            
+            /*!
+             * Creates a copy of the given variable and performs the provided renaming.
+             *
+             * @param oldVariable The variable to copy.
+             * @param newName New name of this variable.
+             * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
+             */
+            Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming);
+            
+        private:
+            // The name of the variable.
+            std::string variableName;
+            
+            // The constant expression defining the initial value of the variable.
+            storm::expressions::Expression initialValueExpression;
+        };
+        
+    } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_VARIABLE_H_ */

test/functional/storage/CuddDdTest.cpp

@@ -6,8 +6,8 @@
 #include "src/storage/dd/DdMetaVariable.h"
 
 TEST(CuddDdManager, Constants) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
-    storm::dd::Dd<storm::dd::CUDD> zero;
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
+    storm::dd::Dd<storm::dd::DdType::CUDD> zero;
     ASSERT_NO_THROW(zero = manager->getZero());
     
     EXPECT_EQ(0, zero.getNonZeroCount());
@@ -16,7 +16,7 @@ TEST(CuddDdManager, Constants) {
     EXPECT_EQ(0, zero.getMin());
     EXPECT_EQ(0, zero.getMax());
     
-    storm::dd::Dd<storm::dd::CUDD> one;
+    storm::dd::Dd<storm::dd::DdType::CUDD> one;
     ASSERT_NO_THROW(one = manager->getOne());
     
     EXPECT_EQ(1, one.getNonZeroCount());
@@ -25,7 +25,7 @@ TEST(CuddDdManager, Constants) {
     EXPECT_EQ(1, one.getMin());
     EXPECT_EQ(1, one.getMax());
 
-    storm::dd::Dd<storm::dd::CUDD> two;
+    storm::dd::Dd<storm::dd::DdType::CUDD> two;
     ASSERT_NO_THROW(two = manager->getConstant(2));
     
     EXPECT_EQ(1, two.getNonZeroCount());
@@ -36,7 +36,7 @@ TEST(CuddDdManager, Constants) {
 }
 
 TEST(CuddDdManager, AddGetMetaVariableTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
     EXPECT_EQ(1, manager->getNumberOfMetaVariables());
     
@@ -56,15 +56,15 @@ TEST(CuddDdManager, AddGetMetaVariableTest) {
     std::set<std::string> metaVariableSet = {"x", "y", "y'"};
     EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
     
-    ASSERT_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException);
-    ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
+    ASSERT_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
 }
 
 TEST(CuddDdManager, EncodingTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariable("x", 1, 9);
     
-    storm::dd::Dd<storm::dd::CUDD> encoding;
+    storm::dd::Dd<storm::dd::DdType::CUDD> encoding;
     ASSERT_THROW(encoding = manager->getEncoding("x", 0), storm::exceptions::InvalidArgumentException);
     ASSERT_THROW(encoding = manager->getEncoding("x", 10), storm::exceptions::InvalidArgumentException);
     ASSERT_NO_THROW(encoding = manager->getEncoding("x", 4));
@@ -74,10 +74,10 @@ TEST(CuddDdManager, EncodingTest) {
 }
 
 TEST(CuddDdManager, RangeTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
     
-    storm::dd::Dd<storm::dd::CUDD> range;
+    storm::dd::Dd<storm::dd::DdType::CUDD> range;
     ASSERT_THROW(range = manager->getRange("y"), storm::exceptions::InvalidArgumentException);
     ASSERT_NO_THROW(range = manager->getRange("x"));
     
@@ -87,10 +87,10 @@ TEST(CuddDdManager, RangeTest) {
 }
 
 TEST(CuddDdManager, IdentityTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariable("x", 1, 9);
     
-    storm::dd::Dd<storm::dd::CUDD> range;
+    storm::dd::Dd<storm::dd::DdType::CUDD> range;
     ASSERT_THROW(range = manager->getIdentity("y"), storm::exceptions::InvalidArgumentException);
     ASSERT_NO_THROW(range = manager->getIdentity("x"));
     
@@ -100,11 +100,11 @@ TEST(CuddDdManager, IdentityTest) {
 }
 
 TEST(CuddDdMetaVariable, AccessorTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariable("x", 1, 9);
     EXPECT_EQ(1, manager->getNumberOfMetaVariables());
-    ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
-    storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x");
+    ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
+    storm::dd::DdMetaVariable<storm::dd::DdType::CUDD> const& metaVariableX = manager->getMetaVariable("x");
     
     EXPECT_EQ(1, metaVariableX.getLow());
     EXPECT_EQ(9, metaVariableX.getHigh());
@@ -114,14 +114,14 @@ TEST(CuddDdMetaVariable, AccessorTest) {
 }
 
 TEST(CuddDd, OperatorTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariable("x", 1, 9);
     EXPECT_TRUE(manager->getZero() == manager->getZero());
     EXPECT_FALSE(manager->getZero() == manager->getOne());
     
-    storm::dd::Dd<storm::dd::CUDD> dd1 = manager->getOne();
-    storm::dd::Dd<storm::dd::CUDD> dd2 = manager->getOne();
-    storm::dd::Dd<storm::dd::CUDD> dd3 = dd1 + dd2;
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne();
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getOne();
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd3 = dd1 + dd2;
     EXPECT_TRUE(dd3 == manager->getConstant(2));
     
     dd3 += manager->getZero();
@@ -154,7 +154,7 @@ TEST(CuddDd, OperatorTest) {
     dd3 = dd1.equals(dd2);
     EXPECT_EQ(1, dd3.getNonZeroCount());
     
-    storm::dd::Dd<storm::dd::CUDD> dd4 = dd1.notEquals(dd2);
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd4 = dd1.notEquals(dd2);
     EXPECT_TRUE(dd4 == ~dd3);
     
     dd3 = dd1.less(dd2);
@@ -171,11 +171,11 @@ TEST(CuddDd, OperatorTest) {
 }
 
 TEST(CuddDd, AbstractionTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
-    storm::dd::Dd<storm::dd::CUDD> dd1;
-    storm::dd::Dd<storm::dd::CUDD> dd2;
-    storm::dd::Dd<storm::dd::CUDD> dd3;
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd3;
     
     dd1 = manager->getIdentity("x");
     dd2 = manager->getConstant(5);
@@ -216,12 +216,12 @@ TEST(CuddDd, AbstractionTest) {
 }
 
 TEST(CuddDd, SwapTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     
     manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
     manager->addMetaVariable("z", 2, 8);
-    storm::dd::Dd<storm::dd::CUDD> dd1;
-    storm::dd::Dd<storm::dd::CUDD> dd2;
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd1;
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
     
     dd1 = manager->getIdentity("x");
     ASSERT_THROW(dd1.swapVariables({std::make_pair("x", "z")}), storm::exceptions::InvalidArgumentException);
@@ -230,12 +230,12 @@ TEST(CuddDd, SwapTest) {
 }
 
 TEST(CuddDd, MultiplyMatrixTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariablesInterleaved({"x", "x'"}, 1, 9);
     
-    storm::dd::Dd<storm::dd::CUDD> dd1 = manager->getIdentity("x").equals(manager->getIdentity("x'"));
-    storm::dd::Dd<storm::dd::CUDD> dd2 = manager->getRange("x'");
-    storm::dd::Dd<storm::dd::CUDD> dd3;
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getIdentity("x").equals(manager->getIdentity("x'"));
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getRange("x'");
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd3;
     dd1 *= manager->getConstant(2);
     
     ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {"x'"}));
@@ -244,10 +244,10 @@ TEST(CuddDd, MultiplyMatrixTest) {
 }
 
 TEST(CuddDd, GetSetValueTest) {
-    std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     manager->addMetaVariable("x", 1, 9);
     
-    storm::dd::Dd<storm::dd::CUDD> dd1 = manager->getOne();
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne();
     ASSERT_NO_THROW(dd1.setValue("x", 4, 2));
     EXPECT_EQ(2, dd1.getLeafCount());
     dd1.exportToDot("dd1.dot");