diff --git a/CMakeLists.txt b/CMakeLists.txt
index 7913af7d7..77b5c64a0 100644
--- a/CMakeLists.txt
+++ b/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})
diff --git a/src/ir/Assignment.cpp b/src/ir/Assignment.cpp
deleted file mode 100644
index a50847afb..000000000
--- a/src/ir/Assignment.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h
deleted file mode 100644
index 12d96a413..000000000
--- a/src/ir/Assignment.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp
deleted file mode 100644
index 843655be9..000000000
--- a/src/ir/BooleanVariable.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h
deleted file mode 100644
index b968d7890..000000000
--- a/src/ir/BooleanVariable.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/IR.h b/src/ir/IR.h
deleted file mode 100644
index 80a794002..000000000
--- a/src/ir/IR.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp
deleted file mode 100644
index b98b30d07..000000000
--- a/src/ir/IntegerVariable.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h
deleted file mode 100644
index 930e1d0b8..000000000
--- a/src/ir/IntegerVariable.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/Program.h b/src/ir/Program.h
deleted file mode 100644
index 8ce96bc87..000000000
--- a/src/ir/Program.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/StateReward.cpp b/src/ir/StateReward.cpp
deleted file mode 100644
index ff3c815ce..000000000
--- a/src/ir/StateReward.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/TransitionReward.cpp b/src/ir/TransitionReward.cpp
deleted file mode 100644
index bd9664529..000000000
--- a/src/ir/TransitionReward.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp
deleted file mode 100644
index aac7b3ca0..000000000
--- a/src/ir/Update.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp
deleted file mode 100644
index 83cb2a33a..000000000
--- a/src/ir/Variable.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/Variable.h b/src/ir/Variable.h
deleted file mode 100644
index 53b2f3b98..000000000
--- a/src/ir/Variable.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/BaseExpression.cpp b/src/ir/expressions/BaseExpression.cpp
deleted file mode 100644
index 66771d6b0..000000000
--- a/src/ir/expressions/BaseExpression.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h
deleted file mode 100644
index 948ed9d88..000000000
--- a/src/ir/expressions/BaseExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp b/src/ir/expressions/BinaryBooleanFunctionExpression.cpp
deleted file mode 100644
index 83cb1d82f..000000000
--- a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h
deleted file mode 100644
index b0cec5906..000000000
--- a/src/ir/expressions/BinaryBooleanFunctionExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/BinaryExpression.cpp b/src/ir/expressions/BinaryExpression.cpp
deleted file mode 100644
index 417cc9301..000000000
--- a/src/ir/expressions/BinaryExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/BinaryExpression.h b/src/ir/expressions/BinaryExpression.h
deleted file mode 100644
index 1d6560863..000000000
--- a/src/ir/expressions/BinaryExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp
deleted file mode 100644
index a80e04ae4..000000000
--- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h
deleted file mode 100644
index 846ceb99a..000000000
--- a/src/ir/expressions/BinaryNumericalFunctionExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/BinaryRelationExpression.cpp b/src/ir/expressions/BinaryRelationExpression.cpp
deleted file mode 100644
index 5c08e7f33..000000000
--- a/src/ir/expressions/BinaryRelationExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h
deleted file mode 100644
index 873cbe5bf..000000000
--- a/src/ir/expressions/BinaryRelationExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/BooleanConstantExpression.cpp b/src/ir/expressions/BooleanConstantExpression.cpp
deleted file mode 100644
index 2022e8796..000000000
--- a/src/ir/expressions/BooleanConstantExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h
deleted file mode 100644
index 4838ba595..000000000
--- a/src/ir/expressions/BooleanConstantExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/BooleanLiteralExpression.cpp b/src/ir/expressions/BooleanLiteralExpression.cpp
deleted file mode 100644
index 89e6b7876..000000000
--- a/src/ir/expressions/BooleanLiteralExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/BooleanLiteralExpression.h b/src/ir/expressions/BooleanLiteralExpression.h
deleted file mode 100644
index 1fb747a78..000000000
--- a/src/ir/expressions/BooleanLiteralExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h
deleted file mode 100644
index dc1763c33..000000000
--- a/src/ir/expressions/ConstantExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/DoubleConstantExpression.cpp b/src/ir/expressions/DoubleConstantExpression.cpp
deleted file mode 100644
index bc29cbf26..000000000
--- a/src/ir/expressions/DoubleConstantExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h
deleted file mode 100644
index 9eaa6eb18..000000000
--- a/src/ir/expressions/DoubleConstantExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/DoubleLiteralExpression.cpp b/src/ir/expressions/DoubleLiteralExpression.cpp
deleted file mode 100644
index 08663f8f7..000000000
--- a/src/ir/expressions/DoubleLiteralExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/DoubleLiteralExpression.h b/src/ir/expressions/DoubleLiteralExpression.h
deleted file mode 100644
index 7105858c2..000000000
--- a/src/ir/expressions/DoubleLiteralExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/ExpressionVisitor.h b/src/ir/expressions/ExpressionVisitor.h
deleted file mode 100644
index d301e9792..000000000
--- a/src/ir/expressions/ExpressionVisitor.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/Expressions.h b/src/ir/expressions/Expressions.h
deleted file mode 100644
index 634a0585d..000000000
--- a/src/ir/expressions/Expressions.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/IntegerConstantExpression.cpp b/src/ir/expressions/IntegerConstantExpression.cpp
deleted file mode 100644
index bcc5cb0eb..000000000
--- a/src/ir/expressions/IntegerConstantExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h
deleted file mode 100644
index 04370574d..000000000
--- a/src/ir/expressions/IntegerConstantExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/IntegerLiteralExpression.cpp b/src/ir/expressions/IntegerLiteralExpression.cpp
deleted file mode 100644
index ed3277f18..000000000
--- a/src/ir/expressions/IntegerLiteralExpression.cpp
+++ /dev/null
@@ -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
\ No newline at end of file
diff --git a/src/ir/expressions/IntegerLiteralExpression.h b/src/ir/expressions/IntegerLiteralExpression.h
deleted file mode 100644
index cb1041684..000000000
--- a/src/ir/expressions/IntegerLiteralExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.cpp b/src/ir/expressions/UnaryBooleanFunctionExpression.cpp
deleted file mode 100644
index 3b0e6ca03..000000000
--- a/src/ir/expressions/UnaryBooleanFunctionExpression.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h
deleted file mode 100644
index a3087f5e5..000000000
--- a/src/ir/expressions/UnaryBooleanFunctionExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/UnaryExpression.cpp b/src/ir/expressions/UnaryExpression.cpp
deleted file mode 100644
index 31463aff3..000000000
--- a/src/ir/expressions/UnaryExpression.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/expressions/UnaryExpression.h b/src/ir/expressions/UnaryExpression.h
deleted file mode 100644
index cfc685455..000000000
--- a/src/ir/expressions/UnaryExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp
deleted file mode 100644
index 6b4b1fbb2..000000000
--- a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp
+++ /dev/null
@@ -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
-
diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h
deleted file mode 100644
index bcb942378..000000000
--- a/src/ir/expressions/UnaryNumericalFunctionExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/ir/expressions/VariableExpression.cpp b/src/ir/expressions/VariableExpression.cpp
deleted file mode 100644
index 9bf09a734..000000000
--- a/src/ir/expressions/VariableExpression.cpp
+++ /dev/null
@@ -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
diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h
deleted file mode 100644
index 99358d377..000000000
--- a/src/ir/expressions/VariableExpression.h
+++ /dev/null
@@ -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_ */
diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index 97ca50507..69fadf5c9 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/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;
}
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 80cf88f3a..6da2dc9c3 100644
--- a/src/storage/dd/CuddDd.h
+++ b/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;
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index 3c87157b2..9843b5c92 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/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;
}
}
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index 569ccf1c9..ca3f9c2c3 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/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;
diff --git a/src/storage/dd/DdMetaVariable.cpp b/src/storage/dd/DdMetaVariable.cpp
index 7671289fc..9132eab03 100644
--- a/src/storage/dd/DdMetaVariable.cpp
+++ b/src/storage/dd/DdMetaVariable.cpp
@@ -47,6 +47,6 @@ namespace storm {
}
// Explicitly instantiate DdMetaVariable.
- template class DdMetaVariable<CUDD>;
+ template class DdMetaVariable<DdType::CUDD>;
}
}
\ No newline at end of file
diff --git a/src/storage/dd/DdType.h b/src/storage/dd/DdType.h
index 327832ec5..feb2fe70a 100644
--- a/src/storage/dd/DdType.h
+++ b/src/storage/dd/DdType.h
@@ -3,7 +3,7 @@
namespace storm {
namespace dd {
- enum DdType {
+ enum class DdType {
CUDD
};
}
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index bd2e3cbc9..0c641d3ec 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/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();
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index 52e656a15..3002e4d35 100644
--- a/src/storage/expressions/Expression.h
+++ b/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
diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp
new file mode 100644
index 000000000..e753583f9
--- /dev/null
+++ b/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>;
+ }
+}
diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.h b/src/storage/expressions/IdentifierSubstitutionVisitor.h
new file mode 100644
index 000000000..87976122c
--- /dev/null
+++ b/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_ */
\ No newline at end of file
diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp
new file mode 100644
index 000000000..4455ec65d
--- /dev/null
+++ b/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
diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h
new file mode 100644
index 000000000..48a235c8a
--- /dev/null
+++ b/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_ */
diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp
new file mode 100644
index 000000000..adf12b165
--- /dev/null
+++ b/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
diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h
new file mode 100644
index 000000000..74c046e00
--- /dev/null
+++ b/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_ */
diff --git a/src/ir/Command.cpp b/src/storage/prism/Command.cpp
similarity index 100%
rename from src/ir/Command.cpp
rename to src/storage/prism/Command.cpp
diff --git a/src/ir/Command.h b/src/storage/prism/Command.h
similarity index 100%
rename from src/ir/Command.h
rename to src/storage/prism/Command.h
diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp
new file mode 100644
index 000000000..7f11a8bc2
--- /dev/null
+++ b/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
diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h
new file mode 100644
index 000000000..b2dbb4cb5
--- /dev/null
+++ b/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_ */
diff --git a/src/ir/Module.cpp b/src/storage/prism/Module.cpp
similarity index 100%
rename from src/ir/Module.cpp
rename to src/storage/prism/Module.cpp
diff --git a/src/ir/Module.h b/src/storage/prism/Module.h
similarity index 100%
rename from src/ir/Module.h
rename to src/storage/prism/Module.h
diff --git a/src/ir/Program.cpp b/src/storage/prism/Program.cpp
similarity index 100%
rename from src/ir/Program.cpp
rename to src/storage/prism/Program.cpp
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
new file mode 100644
index 000000000..169a3fe32
--- /dev/null
+++ b/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_ */
diff --git a/src/ir/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
similarity index 100%
rename from src/ir/RewardModel.cpp
rename to src/storage/prism/RewardModel.cpp
diff --git a/src/ir/RewardModel.h b/src/storage/prism/RewardModel.h
similarity index 100%
rename from src/ir/RewardModel.h
rename to src/storage/prism/RewardModel.h
diff --git a/src/storage/prism/StateReward.cpp b/src/storage/prism/StateReward.cpp
new file mode 100644
index 000000000..50457cabc
--- /dev/null
+++ b/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
diff --git a/src/ir/StateReward.h b/src/storage/prism/StateReward.h
similarity index 78%
rename from src/ir/StateReward.h
rename to src/storage/prism/StateReward.h
index 117544d6d..d8c09f4e2 100644
--- a/src/ir/StateReward.h
+++ b/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
diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp
new file mode 100644
index 000000000..93d951731
--- /dev/null
+++ b/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
diff --git a/src/ir/TransitionReward.h b/src/storage/prism/TransitionReward.h
similarity index 79%
rename from src/ir/TransitionReward.h
rename to src/storage/prism/TransitionReward.h
index 298d17024..b21eeb12f 100644
--- a/src/ir/TransitionReward.h
+++ b/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
diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp
new file mode 100644
index 000000000..7a4bb64ad
--- /dev/null
+++ b/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
diff --git a/src/ir/Update.h b/src/storage/prism/Update.h
similarity index 54%
rename from src/ir/Update.h
rename to src/storage/prism/Update.h
index 07b9a7d24..878e394c3 100644
--- a/src/ir/Update.h
+++ b/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_ */
diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp
new file mode 100644
index 000000000..9527e7f76
--- /dev/null
+++ b/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
diff --git a/src/storage/prism/Variable.h b/src/storage/prism/Variable.h
new file mode 100644
index 000000000..248a0e533
--- /dev/null
+++ b/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_ */
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index 959bc5db0..9230f00e3 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/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");