diff --git a/src/adapters/DdExpressionAdapter.cpp b/src/adapters/DdExpressionAdapter.cpp
new file mode 100644
index 000000000..955a94970
--- /dev/null
+++ b/src/adapters/DdExpressionAdapter.cpp
@@ -0,0 +1,172 @@
+#include "src/adapters/DdExpressionAdapter.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/ExpressionEvaluationException.h"
+
+#include "src/storage/dd/CuddDdManager.h"
+
+namespace storm {
+ namespace adapters {
+
+ template<storm::dd::DdType Type>
+ SymbolicExpressionAdapter<Type>::SymbolicExpressionAdapter(storm::dd::DdManager<Type> const& ddManager, std::map<storm::expressions::Variable, storm::expressions::Variable> const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType Type>
+ storm::dd::Dd<Type> SymbolicExpressionAdapter<Type>::translateExpression(storm::expressions::Expression const& expression) {
+ return boost::any_cast<storm::dd::Dd<Type>>(expression.accept(*this));
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::IfThenElseExpression const& expression) {
+ storm::dd::Dd<Type> elseDd = boost::any_cast<storm::dd::Dd<Type>>(expression.getElseExpression()->accept(*this));
+ storm::dd::Dd<Type> thenDd = boost::any_cast<storm::dd::Dd<Type>>(expression.getThenExpression()->accept(*this));
+ storm::dd::Dd<Type> conditionDd = boost::any_cast<storm::dd::Dd<Type>>(expression.getCondition()->accept(*this));
+ return conditionDd.ite(thenDd, elseDd);
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) {
+ storm::dd::Dd<Type> leftResult = boost::any_cast<storm::dd::Dd<Type>>(expression.getFirstOperand()->accept(*this));
+ storm::dd::Dd<Type> rightResult = boost::any_cast<storm::dd::Dd<Type>>(expression.getSecondOperand()->accept(*this));
+
+ storm::dd::Dd<Type> result;
+ switch (expression.getOperatorType()) {
+ case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And:
+ result = leftResult && rightResult;
+ break;
+ case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or:
+ result = leftResult || rightResult;
+ break;
+ case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff:
+ result = leftResult.equals(rightResult);
+ break;
+ case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies:
+ result = !leftResult || rightResult;
+ break;
+ case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor:
+ result = (leftResult && !rightResult) || (!leftResult && rightResult);
+ break;
+ }
+
+ return result;
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) {
+ storm::dd::Dd<Type> leftResult = boost::any_cast<storm::dd::Dd<Type>>(expression.getFirstOperand()->accept(*this));
+ storm::dd::Dd<Type> rightResult = boost::any_cast<storm::dd::Dd<Type>>(expression.getSecondOperand()->accept(*this));
+
+ storm::dd::Dd<Type> result;
+ switch (expression.getOperatorType()) {
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus:
+ result = leftResult + rightResult;
+ break;
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus:
+ result = leftResult - rightResult;
+ break;
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times:
+ result = leftResult * rightResult;
+ break;
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide:
+ result = leftResult / rightResult;
+ break;
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max:
+ result = leftResult.maximum(rightResult);
+ break;
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min:
+ result = leftResult.minimum(rightResult);
+ break;
+ default:
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate expression containing power operator.");
+ }
+
+ return result;
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::BinaryRelationExpression const& expression) {
+ storm::dd::Dd<Type> leftResult = boost::any_cast<storm::dd::Dd<Type>>(expression.getFirstOperand()->accept(*this));
+ storm::dd::Dd<Type> rightResult = boost::any_cast<storm::dd::Dd<Type>>(expression.getSecondOperand()->accept(*this));
+
+ storm::dd::Dd<Type> result;
+ switch (expression.getRelationType()) {
+ case storm::expressions::BinaryRelationExpression::RelationType::Equal:
+ result = leftResult.equals(rightResult);
+ break;
+ case storm::expressions::BinaryRelationExpression::RelationType::NotEqual:
+ result = leftResult.notEquals(rightResult);
+ break;
+ case storm::expressions::BinaryRelationExpression::RelationType::Less:
+ result = leftResult.less(rightResult);
+ break;
+ case storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual:
+ result = leftResult.lessOrEqual(rightResult);
+ break;
+ case storm::expressions::BinaryRelationExpression::RelationType::Greater:
+ result = leftResult.greater(rightResult);
+ break;
+ case storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual:
+ result = leftResult.greaterOrEqual(rightResult);
+ break;
+ }
+
+ return result;
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::VariableExpression const& expression) {
+ auto const& variablePair = variableMapping.find(expression.getVariable());
+ STORM_LOG_THROW(variablePair != variableMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains th variable '" << expression.getVariableName() << "' for which no DD counterpart is known.");
+ return ddManager.getIdentity(variablePair->second);
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) {
+ storm::dd::Dd<Type> result = boost::any_cast<storm::dd::Dd<Type>>(expression.getOperand()->accept(*this));
+
+ switch (expression.getOperatorType()) {
+ case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not:
+ result = !result;
+ break;
+ }
+
+ return result;
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) {
+ storm::dd::Dd<Type> result = boost::any_cast<storm::dd::Dd<Type>>(expression.getOperand()->accept(*this));
+
+ switch (expression.getOperatorType()) {
+ case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus:
+ result = -result;
+ break;
+ default:
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate expression containing floor/ceil operator.");
+ }
+
+ return result;
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::BooleanLiteralExpression const& expression) {
+ return ddManager.getConstant(expression.getValue());
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::IntegerLiteralExpression const& expression) {
+ return ddManager.getConstant(expression.getValue());
+ }
+
+ template<storm::dd::DdType Type>
+ boost::any SymbolicExpressionAdapter<Type>::visit(storm::expressions::DoubleLiteralExpression const& expression) {
+ return ddManager.getConstant(expression.getValue());
+ }
+
+ // Explicitly instantiate the symbolic expression adapter
+ template class SymbolicExpressionAdapter<storm::dd::DdType::CUDD>;
+
+ } // namespace adapters
+} // namespace storm
diff --git a/src/adapters/DdExpressionAdapter.h b/src/adapters/DdExpressionAdapter.h
new file mode 100644
index 000000000..a41d0993c
--- /dev/null
+++ b/src/adapters/DdExpressionAdapter.h
@@ -0,0 +1,43 @@
+#ifndef STORM_ADAPTERS_DDEXPRESSIONADAPTER_H_
+#define STORM_ADAPTERS_DDEXPRESSIONADAPTER_H_
+
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/Expressions.h"
+#include "storage/expressions/ExpressionVisitor.h"
+
+#include "src/storage/dd/Dd.h"
+#include "src/storage/dd/DdManager.h"
+
+namespace storm {
+ namespace adapters {
+
+ template<storm::dd::DdType Type>
+ class SymbolicExpressionAdapter : public storm::expressions::ExpressionVisitor {
+ public:
+ SymbolicExpressionAdapter(storm::dd::DdManager<Type> const& ddManager, std::map<storm::expressions::Variable, storm::expressions::Variable> const& variableMapping);
+
+ storm::dd::Dd<Type> translateExpression(storm::expressions::Expression const& expression);
+
+ virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::VariableExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override;
+ virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override;
+
+ private:
+ // The manager responsible for the DDs built by this adapter.
+ storm::dd::DdManager<Type> const& ddManager;
+
+ // This member maps the variables used in the expressions to the variables used by the DD manager.
+ std::map<storm::expressions::Variable, storm::expressions::Variable> const& variableMapping;
+ };
+
+ } // namespace adapters
+} // namespace storm
+
+#endif /* STORM_ADAPTERS_DDEXPRESSIONADAPTER_H_ */
diff --git a/src/adapters/StormAdapter.h b/src/adapters/StormAdapter.h
deleted file mode 100644
index 9fe348c00..000000000
--- a/src/adapters/StormAdapter.h
+++ /dev/null
@@ -1,199 +0,0 @@
-/*
- * StormAdapter.h
- *
- * Created on: 02.03.2013
- * Author: Philipp Berger
- */
-
-#ifndef STORM_ADAPTERS_STORMADAPTER_H_
-#define STORM_ADAPTERS_STORMADAPTER_H_
-
-#include "gmm/gmm_matrix.h"
-#include "Eigen/Sparse"
-#include "src/storage/SparseMatrix.h"
-
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-
-extern log4cplus::Logger logger;
-
-namespace storm {
-
-namespace adapters {
-
-class StormAdapter {
-public:
- /*!
- * Converts a sparse matrix into a sparse matrix in the storm format.
- * @return A pointer to a row-major sparse matrix in storm format.
- */
- template<class T>
- static storm::storage::SparseMatrix<T>* toStormSparseMatrix(gmm::csr_matrix<T> const& matrix) {
- uint_fast64_t realNonZeros = gmm::nnz(matrix);
- LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from gmm++ format into Storm.");
-
- // Prepare the resulting matrix.
- storm::storage::SparseMatrix<T>* result = new storm::storage::SparseMatrix<T>(matrix.ncols(), matrix.jc, matrix.ir, matrix.pr);
-
- LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format.");
-
- return result;
- }
-
- /*!
- * Helper function to determine whether the given Eigen matrix is in RowMajor
- * format. Always returns true, but is overloaded, so the compiler will
- * only call it in case the Eigen matrix is in RowMajor format.
- * @return True.
- */
- template<typename _Scalar, typename _Index>
- static bool isEigenRowMajor(Eigen::SparseMatrix<_Scalar, Eigen::RowMajor, _Index>) {
- return true;
- }
-
- /*!
- * Helper function to determine whether the given Eigen matrix is in RowMajor
- * format. Always returns false, but is overloaded, so the compiler will
- * only call it in case the Eigen matrix is in ColMajor format.
- * @return False.
- */
- template<typename _Scalar, typename _Index>
- static bool isEigenRowMajor(
- Eigen::SparseMatrix<_Scalar, Eigen::ColMajor, _Index>) {
- return false;
- }
-
- /*!
- * Converts a sparse matrix in the eigen format to Storm Sparse Matrix format.
- * @return A pointer to a row-major sparse matrix in our format.
- */
- template<class T, int _Options, typename _Index>
- static storm::storage::SparseMatrix<T>* toStormSparseMatrix(Eigen::SparseMatrix<T, _Options, _Index> const& matrix) {
- uint_fast64_t realNonZeros = matrix.nonZeros();
- LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from Eigen3 format into Storm.");
-
- // Throw an error in case the matrix is not in compressed format.
- if (!matrix.isCompressed()) {
- LOG4CPLUS_ERROR(logger, "Trying to convert from an Eigen matrix that is not in compressed form.");
- return nullptr;
- }
-
- /*
- * Try to prepare the internal storage and throw an error in case of
- * failure.
- */
-
- // Get necessary pointers to the contents of the Eigen matrix.
- const T* valuePtr = matrix.valuePtr();
- const _Index* indexPtr = matrix.innerIndexPtr();
- const _Index* outerPtr = matrix.outerIndexPtr();
-
- const uint_fast64_t outerSize = matrix.outerSize();
-
- storm::storage::SparseMatrix<T>* result = nullptr;
-
- // If the given matrix is in RowMajor format, copying can simply
- // be done by adding all values in order.
- // Direct copying is, however, prevented because we have to
- // separate the diagonal entries from others.
- if (isEigenRowMajor(matrix)) {
- /* Because of the RowMajor format outerSize evaluates to the
- * number of rows.
- * Prepare the resulting matrix.
- */
- result = new storm::storage::SparseMatrix<T>(matrix.outerSize(), matrix.innerSize());
-
- // Set internal NonZero Counter
- result->nonZeroEntryCount = realNonZeros;
- result->setState(result->Initialized);
-
- if (!result->prepareInternalStorage(false)) {
- LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting Eigen3 RM Matrix to Storm.");
- delete result;
- return nullptr;
- } else {
-
- // Copy Row Indications
- std::copy(outerPtr, outerPtr + outerSize, std::back_inserter(result->rowIndications));
- // Copy Columns Indications
- std::copy(indexPtr, indexPtr + realNonZeros, std::back_inserter(result->columnIndications));
- // And do the same thing with the actual values.
- std::copy(valuePtr, valuePtr + realNonZeros, std::back_inserter(result->valueStorage));
-
- // This is our Sentinel Element.
- result->rowIndications.push_back(realNonZeros);
-
- result->currentSize = realNonZeros;
- result->lastRow = outerSize - 1;
- }
- } else {
- /* Because of the RowMajor format outerSize evaluates to the
- * number of columns.
- * Prepare the resulting matrix.
- */
- const uint_fast64_t colCount = matrix.outerSize();
- result = new storm::storage::SparseMatrix<T>(matrix.innerSize(), colCount);
-
- // Set internal NonZero Counter
- result->nonZeroEntryCount = realNonZeros;
- result->setState(result->Initialized);
- if (!result->prepareInternalStorage()) {
- LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting Eigen3 CM Matrix to Storm.");
- delete result;
- return nullptr;
- } else {
- // Set internal NonZero Counter
- result->nonZeroEntryCount = realNonZeros;
- result->setState(result->Initialized);
-
- // Create an array to remember which elements have to still
- // be searched in each column and initialize it with the starting
- // index for every column.
- _Index* positions = new _Index[colCount]();
- for (_Index i = 0; i < colCount; ++i) {
- positions[i] = outerPtr[i];
- }
-
- // Now copy the elements. As the matrix is in ColMajor format,
- // we need to iterate over the columns to find the next non-zero
- // entry.
- uint_fast64_t i = 0;
- int currentRow = 0;
- int currentColumn = 0;
- while (i < realNonZeros) {
- // If the current element belongs the the current column,
- // add it in case it is also in the current row.
- if ((positions[currentColumn] < outerPtr[currentColumn + 1])
- && (indexPtr[positions[currentColumn]] == currentRow)) {
- result->addNextValue(currentRow, currentColumn, valuePtr[positions[currentColumn]]);
- // Remember that we found one more non-zero element.
- ++i;
- // Mark this position as "used".
- ++positions[currentColumn];
- }
-
- // Now we can advance to the next column and also row,
- // in case we just iterated through the last column.
- ++currentColumn;
- if (currentColumn == colCount) {
- currentColumn = 0;
- ++currentRow;
- }
- }
- delete[] positions;
- }
- }
- result->setState(result->Initialized);
- result->finalize();
-
- LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format.");
-
- return result;
- }
-};
-
-} //namespace adapters
-
-} //namespace storm
-
-#endif /* STORM_ADAPTERS_STORMADAPTER_H_ */
diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h
deleted file mode 100644
index 29ab6c613..000000000
--- a/src/adapters/SymbolicModelAdapter.h
+++ /dev/null
@@ -1,299 +0,0 @@
-/*
- * SymbolicModelAdapter.h
- *
- * Created on: 25.01.2013
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_
-#define STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_
-
-#include "src/exceptions/WrongFormatException.h"
-
-#include "src/utility/CuddUtility.h"
-#include "SymbolicExpressionAdapter.h"
-
-#include "cuddObj.hh"
-#include <iostream>
-#include <unordered_map>
-#include <cmath>
-
-namespace storm {
-
-namespace adapters {
-
-class SymbolicModelAdapter {
-public:
-
- SymbolicModelAdapter(storm::ir::Program const& program) : program(program), cuddUtility(storm::utility::cuddUtilityInstance()), allDecisionDiagramVariables(),
- allRowDecisionDiagramVariables(), allColumnDecisionDiagramVariables(), booleanRowDecisionDiagramVariables(),
- integerRowDecisionDiagramVariables(), booleanColumnDecisionDiagramVariables(), integerColumnDecisionDiagramVariables(),
- variableToRowDecisionDiagramVariableMap(), variableToColumnDecisionDiagramVariableMap(),
- variableToIdentityDecisionDiagramMap(),
- rowExpressionAdapter(program, variableToRowDecisionDiagramVariableMap), columnExpressionAdapter(program, variableToColumnDecisionDiagramVariableMap) {
-
- }
-
- void toMTBDD() {
- LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program.");
- createDecisionDiagramVariables(program);
- createIdentityDecisionDiagrams(program);
-
- ADD* systemAdd = cuddUtility->getZero();
- for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
- storm::ir::Module const& module = program.getModule(i);
-
- ADD* moduleAdd = cuddUtility->getZero();
- for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
- storm::ir::Command const& command = module.getCommand(j);
-
- ADD* commandAdd = cuddUtility->getZero();
-
- ADD* guard = rowExpressionAdapter.translateExpression(command.getGuard());
- if (*guard != *cuddUtility->getZero()) {
- for (uint_fast64_t i = 0; i < command.getNumberOfUpdates(); ++i) {
- ADD* updateAdd = cuddUtility->getOne();
-
- storm::ir::Update const& update = command.getUpdate(i);
-
- std::map<std::string, storm::ir::Assignment> booleanAssignments = update.getBooleanAssignments();
- for (auto assignmentPair : booleanAssignments) {
- ADD* updateExpr = rowExpressionAdapter.translateExpression(assignmentPair.second.getExpression());
-
- ADD* temporary = cuddUtility->getZero();
- cuddUtility->setValueAtIndex(temporary, 0, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], 0);
- cuddUtility->setValueAtIndex(temporary, 1, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], 1);
-
- ADD* result = new ADD(*updateExpr * *guard);
- result = new ADD(result->Equals(*temporary));
-
- *updateAdd = *updateAdd * *result;
- }
-
- std::map<std::string, storm::ir::Assignment> integerAssignments = update.getIntegerAssignments();
- for (auto assignmentPair : integerAssignments) {
- ADD* updateExpr = rowExpressionAdapter.translateExpression(assignmentPair.second.getExpression());
-
- ADD* temporary = cuddUtility->getZero();
-
- uint_fast64_t variableIndex = module.getIntegerVariableIndex(assignmentPair.first);
- storm::ir::IntegerVariable integerVariable = module.getIntegerVariable(variableIndex);
- int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr);
- int_fast64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr);
-
- for (int_fast64_t i = low; i <= high; ++i) {
- cuddUtility->setValueAtIndex(temporary, i - low, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], static_cast<double>(i));
- }
-
- ADD* result = new ADD(*updateExpr * *guard);
- result = new ADD(result->Equals(*temporary));
- *result *= *guard;
-
- *updateAdd = *updateAdd * *result;
- }
- for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); ++i) {
- storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(i);
-
- if (update.getBooleanAssignments().find(booleanVariable.getName()) == update.getBooleanAssignments().end()) {
- *updateAdd = *updateAdd * *variableToIdentityDecisionDiagramMap[booleanVariable.getName()];
- }
- }
- for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); ++i) {
- storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(i);
-
- if (update.getIntegerAssignments().find(integerVariable.getName()) == update.getIntegerAssignments().end()) {
- *updateAdd = *updateAdd * *variableToIdentityDecisionDiagramMap[integerVariable.getName()];
- }
- }
-
- *commandAdd += *updateAdd * *cuddUtility->getConstant(update.getLikelihoodExpression()->getValueAsDouble(nullptr));
- }
- *moduleAdd += *commandAdd;
- } else {
- LOG4CPLUS_WARN(logger, "Guard " << command.getGuard()->toString() << " is unsatisfiable.");
- }
- }
- *systemAdd += *moduleAdd;
- }
-
- performReachability(program, systemAdd);
-
- LOG4CPLUS_INFO(logger, "Done creating MTBDD representation for probabilistic program.");
- }
-
-private:
- storm::ir::Program const& program;
- storm::utility::CuddUtility* cuddUtility;
-
- std::vector<ADD*> allDecisionDiagramVariables;
- std::vector<ADD*> allRowDecisionDiagramVariables;
- std::vector<ADD*> allColumnDecisionDiagramVariables;
- std::vector<ADD*> booleanRowDecisionDiagramVariables;
- std::vector<ADD*> integerRowDecisionDiagramVariables;
- std::vector<ADD*> booleanColumnDecisionDiagramVariables;
- std::vector<ADD*> integerColumnDecisionDiagramVariables;
- std::unordered_map<std::string, std::vector<ADD*>> variableToRowDecisionDiagramVariableMap;
- std::unordered_map<std::string, std::vector<ADD*>> variableToColumnDecisionDiagramVariableMap;
-
- std::unordered_map<std::string, ADD*> variableToIdentityDecisionDiagramMap;
-
- SymbolicExpressionAdapter rowExpressionAdapter;
- SymbolicExpressionAdapter columnExpressionAdapter;
-
- // As log2 is not part of C90, only of C99 which no Compiler fully supports, this feature is unavailable on MSVC
- inline double log2(uint_fast64_t number) {
-# include "src/utility/OsDetection.h"
-# ifndef WINDOWS
- return std::log2(number);
-# else
- return std::log(number) / std::log(2);
-# endif
- }
-
- ADD* getInitialStateDecisionDiagram(storm::ir::Program const& program) {
- ADD* initialStates = cuddUtility->getOne();
- for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
- storm::ir::Module const& module = program.getModule(i);
-
- for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
- storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j);
- *initialStates *= *cuddUtility->getConstantEncoding(1, variableToRowDecisionDiagramVariableMap[booleanVariable.getName()]);
- }
- for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
- storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j);
- int_fast64_t initialValue = integerVariable.getInitialValue()->getValueAsInt(nullptr);
- int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr);
- *initialStates *= *cuddUtility->getConstantEncoding(initialValue - low, variableToRowDecisionDiagramVariableMap[integerVariable.getName()]);
- }
- }
-
- cuddUtility->dumpDotToFile(initialStates, "initstates.add");
- return initialStates;
- }
-
- void performReachability(storm::ir::Program const& program, ADD* systemAdd) {
- ADD* systemAdd01 = new ADD(systemAdd->GreaterThan(*cuddUtility->getZero()));
- cuddUtility->dumpDotToFile(systemAdd01, "system01.add");
-
- cuddUtility->dumpDotToFile(systemAdd, "reachtransold.add");
- ADD* reachableStates = getInitialStateDecisionDiagram(program);
- cuddUtility->dumpDotToFile(reachableStates, "init.add");
- ADD* newReachableStates = new ADD(*reachableStates);
-
- ADD* rowCube = cuddUtility->getOne();
- for (auto variablePtr : allRowDecisionDiagramVariables) {
- *rowCube *= *variablePtr;
- }
-
- bool changed;
- do {
- changed = false;
- *newReachableStates = *reachableStates * *systemAdd01;
- newReachableStates = new ADD(newReachableStates->ExistAbstract(*rowCube));
-
- cuddUtility->dumpDotToFile(newReachableStates, "reach1.add");
-
- newReachableStates = cuddUtility->permuteVariables(newReachableStates, allColumnDecisionDiagramVariables, allRowDecisionDiagramVariables, static_cast<int>(allDecisionDiagramVariables.size()));
-
- *newReachableStates += *reachableStates;
- newReachableStates = new ADD(newReachableStates->GreaterThan(*cuddUtility->getZero()));
-
- if (*newReachableStates != *reachableStates) changed = true;
- *reachableStates = *newReachableStates;
- } while (changed);
-
- *systemAdd *= *reachableStates;
- std::cout << "got " << systemAdd->nodeCount() << " nodes" << std::endl;
- std::cout << "and " << systemAdd->CountMinterm(static_cast<int>(allRowDecisionDiagramVariables.size() + allColumnDecisionDiagramVariables.size())) << std::endl;
- }
-
- void createIdentityDecisionDiagrams(storm::ir::Program const& program) {
- for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
- storm::ir::Module const& module = program.getModule(i);
-
- for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
- storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j);
- ADD* identity = cuddUtility->getZero();
- cuddUtility->setValueAtIndices(identity, 0, 0,
- variableToRowDecisionDiagramVariableMap[booleanVariable.getName()],
- variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()], 1);
- cuddUtility->setValueAtIndices(identity, 1, 1,
- variableToRowDecisionDiagramVariableMap[booleanVariable.getName()],
- variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()], 1);
- variableToIdentityDecisionDiagramMap[booleanVariable.getName()] = identity;
- }
-
- for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
- storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j);
-
- ADD* identity = cuddUtility->getZero();
-
- int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr);
- int_fast64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr);
-
- for (int_fast64_t i = low; i <= high; ++i) {
- cuddUtility->setValueAtIndices(identity, i - low, i - low,
- variableToRowDecisionDiagramVariableMap[integerVariable.getName()],
- variableToColumnDecisionDiagramVariableMap[integerVariable.getName()], 1);
- }
- variableToIdentityDecisionDiagramMap[integerVariable.getName()] = identity;
- }
- }
- }
-
- void createDecisionDiagramVariables(storm::ir::Program const& program) {
- for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
- storm::ir::Module const& module = program.getModule(i);
-
- for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
- storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j);
-
- ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable();
- variableToRowDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newRowDecisionDiagramVariable);
- booleanRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
- allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
- allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
-
- ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable();
- variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newColumnDecisionDiagramVariable);
- booleanColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
- allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
- allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
- }
-
- for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
- storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j);
- uint_fast64_t integerRange = integerVariable.getUpperBound()->getValueAsInt(nullptr) - integerVariable.getLowerBound()->getValueAsInt(nullptr);
- if (integerRange <= 0) {
- throw storm::exceptions::WrongFormatException() << "Range of variable "
- << integerVariable.getName() << " is empty or negativ.";
- }
- uint_fast64_t numberOfDecisionDiagramVariables = static_cast<uint_fast64_t>(std::ceil(log2(integerRange)));
-
- std::vector<ADD*> allRowDecisionDiagramVariablesForVariable;
- std::vector<ADD*> allColumnDecisionDiagramVariablesForVariable;
- for (uint_fast64_t k = 0; k < numberOfDecisionDiagramVariables; ++k) {
- ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable();
- allRowDecisionDiagramVariablesForVariable.push_back(newRowDecisionDiagramVariable);
- integerRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
- allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
- allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable);
-
- ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable();
- allColumnDecisionDiagramVariablesForVariable.push_back(newColumnDecisionDiagramVariable);
- integerColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
- allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
- allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable);
- }
- variableToRowDecisionDiagramVariableMap[integerVariable.getName()] = allRowDecisionDiagramVariablesForVariable;
- variableToColumnDecisionDiagramVariableMap[integerVariable.getName()] = allColumnDecisionDiagramVariablesForVariable;
- }
- }
- }
-};
-
-} // namespace adapters
-
-} // namespace storm
-
-#endif /* STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ */
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
new file mode 100644
index 000000000..3214a1e42
--- /dev/null
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -0,0 +1,1442 @@
+#include "src/builder/DdPrismModelBuilder.h"
+#include "src/adapters/DdExpressionAdapter.h"
+
+#include "src/storage/dd/CuddDd.h"
+#include "src/storage/dd/CuddDdManager.h"
+#include "src/settings/SettingsManager.h"
+
+#include "src/utility/prism.h"
+#include "src/utility/math.h"
+#include "src/utility/macros.h"
+
+namespace storm {
+ namespace adapters {
+
+ template <storm::dd::DdType Type>
+ DdPrismModelBuilder<Type>::Options::Options() : buildRewards(false), rewardModelName(), constantDefinitions() {
+ // Intentionally left empty.
+ }
+
+ template <storm::dd::DdType Type>
+ DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildRewards(formula.containsRewardOperator()), rewardModelName(), constantDefinitions(), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
+ // Extract all the labels used in the formula.
+ std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
+ for (auto const& formula : atomicLabelFormulas) {
+ labelsToBuild.get().insert(formula.get()->getLabel());
+ }
+
+ // Extract all the expressions used in the formula.
+ std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas();
+ for (auto const& formula : atomicExpressionFormulas) {
+ expressionLabels.get().push_back(formula.get()->getExpression());
+ }
+ }
+
+ template <storm::dd::DdType Type>
+ void DdPrismModelBuilder<Type>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
+ std::map<storm::expressions::Variable, storm::expressions::Expression> newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString);
+
+ // If there is at least one constant that is defined, and the constant definition map does not yet exist,
+ // we need to create it.
+ if (!constantDefinitions && !newConstantDefinitions.empty()) {
+ constantDefinitions = std::map<storm::expressions::Variable, storm::expressions::Expression>();
+ }
+
+ // Now insert all the entries that need to be defined.
+ for (auto const& entry : newConstantDefinitions) {
+ constantDefinitions.get().insert(entry);
+ }
+ }
+
+ template <storm::dd::DdType Type>
+ void DdPrismModelBuilder<Type>::translateProgram(storm::prism::Program const& program, Options const& options) {
+ // There might be nondeterministic variables. In that case the program must be prepared before translating.
+ storm::prism::Program preparedProgram;
+ if (options.constantDefinitions) {
+ preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get());
+ } else {
+ preparedProgram = program;
+ }
+
+ preparedProgram = preparedProgram.substituteConstants();
+
+ // Start by initializing the structure used for storing all information needed during the model generation.
+ // In particular, this creates the meta variables used to encode the model.
+// GenerationInformation generationInfo(preparedProgram);
+
+
+// LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program.");
+//
+// // There might be nondeterministic variables. In that case the program must be prepared before translating.
+// storm::prism::Program preparedProgram = program.defineUndefinedConstants(std::map<std::string, storm::expressions::Expression>());
+// preparedProgram = preparedProgram.substituteConstants();
+//
+// // Initialize the structure used for storing all information needed during the model generation.
+// GenerationInformation generationInfo(preparedProgram);
+//
+// // Initial state DD
+// storm::dd::Dd<Type> initialStateDd = generationInfo.manager->getZero();
+// initialStateDd = getInitialStateDecisionDiagram(generationInfo);
+//
+// // System DD
+// storm::dd::Dd<Type> systemDd = generationInfo.manager->getZero();
+//
+// // Reachable states DD
+// storm::dd::Dd<Type> reachableStatesDd = generationInfo.manager->getOne();
+//
+// // Initialize the clock.
+// auto clock = std::chrono::high_resolution_clock::now();
+//
+// // Create system DD
+// systemDd = createSystemDecisionDiagramm(generationInfo);
+// std::cout << "Built transition matrix in " << std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl;
+//
+// //manager->triggerReordering();
+//
+// // Get all reachable states
+// if (!storm::settings::adapterSettings().isNoReachSet()){
+// reachableStatesDd = performReachability(generationInfo, systemDd, initialStateDd);
+// // Reduce transition matrix
+// systemDd = systemDd * reachableStatesDd;
+// }
+//
+// // Fix deadlocks
+// if (!storm::settings::adapterSettings().isNoDeadlockSet()){
+// systemDd = findDeadlocks(generationInfo, systemDd, reachableStatesDd);
+// }
+//
+// // System DD with only 0/1 leaves
+// storm::dd::Dd<Type> systemBdd = systemDd.notZero();
+//
+// // Get all abstract variables (MDP)
+// std::set<std::string> abstractVariables = std::set<std::string>();
+//
+// if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) {
+// // Synchronizing variables
+// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) {
+// abstractVariables.insert("sync" + std::to_string(i));
+// }
+// }
+// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) {
+// // Nondet. variables
+// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) {
+// abstractVariables.insert("nondet" + std::to_string(i));
+// }
+// }
+// }
+//
+// // Create state labeling
+// std::unordered_map<std::string, storm::dd::Dd<Type>> labelToStateDdMap;
+// storm::dd::Dd<Type> temporary;
+// for (auto const& label : program.getLabels()) {
+// // Translate Labeling into Expression and further into DD
+// temporary = storm::adapters::SymbolicExpressionAdapter<Type>::translateExpression(label.getStatePredicateExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager, false);
+// temporary = temporary * reachableStatesDd;
+// labelToStateDdMap.insert(std::make_pair(label.getName(), temporary));
+// }
+//
+// // Create model
+// std::shared_ptr<storm::models::AbstractSymbolicModel<Type>> model;
+// switch (program.getModelType()){
+// case storm::prism::Program::ModelType::DTMC:
+// model = std::shared_ptr<storm::models::AbstractSymbolicModel<Type>>(std::make_shared<storm::models::SymbolicDtmc<Type>>(std::move(systemDd),
+// std::move(systemBdd), std::move(initialStateDd), std::move(reachableStatesDd),
+// std::move(generationInfo.rewardDds.first), std::move(generationInfo.rewardDds.second), std::move(generationInfo.manager->getZero()),
+// std::move(generationInfo.rowMetaVariableNames), std::move(generationInfo.columnMetaVariableNames), std::move(generationInfo.metaVariablePairs),
+// std::move(generationInfo.allSynchronizingActions), std::move(abstractVariables), std::move(generationInfo.manager), std::move(labelToStateDdMap)));
+// break;
+// case storm::prism::Program::ModelType::MDP:
+// model = std::shared_ptr<storm::models::AbstractSymbolicModel<Type>>(std::make_shared<storm::models::SymbolicMdp<Type>>(std::move(systemDd),
+// std::move(systemBdd), std::move(initialStateDd), std::move(reachableStatesDd),
+// std::move(generationInfo.rewardDds.first), std::move(generationInfo.rewardDds.second), std::move(generationInfo.transitionActionDd),
+// std::move(generationInfo.rowMetaVariableNames), std::move(generationInfo.columnMetaVariableNames), std::move(generationInfo.metaVariablePairs),
+// std::move(generationInfo.allSynchronizingActions), std::move(abstractVariables), std::move(generationInfo.manager), std::move(labelToStateDdMap)));
+// break;
+// default:
+// STORM_LOG_ASSERT(false, "Illegal model type.");
+// }
+//
+// LOG4CPLUS_INFO(logger, "Done creating MTBDD representation for probabilistic preparedProgram.");
+// LOG4CPLUS_INFO(logger, "MTBDD: " << systemDd.getNodeCount() << " nodes, " << systemDd.getLeafCount() << " leaves, " << generationInfo.manager->getNumberOfMetaVariables() << " variables.");
+// return model;
+ }
+
+// template <storm::dd::DdType Type>
+// void SymbolicModelAdapter<Type>::GenerationInformation::addDecisionDiagramVariables() {
+//
+// uint_fast64_t numberOfSynchronizingActions = allSynchronizingActions.size();
+//
+// // Add synchronizing variables
+// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i) {
+// manager->addMetaVariable("sync" + std::to_string(i), 0, 1);
+// }
+//
+// // Add nondet. variables ( number of modules + number of commands)
+// numberOfNondetVariables = program.getModules().size();
+// for (uint_fast64_t i = 0; i < program.getModules().size(); ++i) {
+// numberOfNondetVariables += program.getModule(i).getCommands().size();
+// }
+//
+// for (uint_fast64_t i = numberOfNondetVariables; i > 0; --i) {
+// manager->addMetaVariable("nondet" + std::to_string(i), 0, 1);
+// }
+//
+// std::vector<std::string> newVariables;
+//
+// // Global Boolean Variables
+// for (uint_fast64_t j = 0; j < program.getGlobalBooleanVariables().size(); ++j) {
+// storm::prism::BooleanVariable const& booleanVariable = program.getGlobalBooleanVariables().at(j);
+//
+// // Add row and column meta variable
+// manager->addMetaVariable(booleanVariable.getName(), 0, 1);
+//
+// rowMetaVariableNames.insert(booleanVariable.getName());
+// columnMetaVariableNames.insert(booleanVariable.getName() + "'");
+//
+// // Create pair (column,row)
+// std::pair<std::string, std::string> variablePair(booleanVariable.getName() + "'", booleanVariable.getName());
+// metaVariablePairs.push_back(variablePair);
+// }
+//
+// // Global Integer Variables
+// for (uint_fast64_t j = 0; j < program.getGlobalIntegerVariables().size(); ++j) {
+// storm::prism::IntegerVariable const& integerVariable = program.getGlobalIntegerVariables().at(j);
+//
+// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
+// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
+//
+// // Add row and column meta variable
+// manager->addMetaVariable(integerVariable.getName(), low, high);
+//
+// rowMetaVariableNames.insert(integerVariable.getName());
+// columnMetaVariableNames.insert(integerVariable.getName() + "'");
+//
+// // Create pair (column,row)
+// std::pair<std::string, std::string> variablePair(integerVariable.getName() + "'", integerVariable.getName());
+// metaVariablePairs.push_back(variablePair);
+// }
+//
+// // Add boolean and integer variables
+// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+// storm::prism::Module const& module = program.getModule(i);
+//
+// // Boolean Variables
+// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
+// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(j);
+//
+// // Add row and column meta variable
+// manager->addMetaVariable(booleanVariable.getName(), 0, 1);
+//
+// rowMetaVariableNames.insert(booleanVariable.getName());
+// columnMetaVariableNames.insert(booleanVariable.getName() + "'");
+//
+// // Create pair (column,row)
+// std::pair<std::string, std::string> variablePair(booleanVariable.getName() + "'", booleanVariable.getName());
+// metaVariablePairs.push_back(variablePair);
+// }
+//
+// // Integer Variables
+// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
+// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(j);
+//
+// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
+// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
+//
+// // Add row and column meta variable
+// manager->addMetaVariable(integerVariable.getName(), low, high);
+//
+// rowMetaVariableNames.insert(integerVariable.getName());
+// columnMetaVariableNames.insert(integerVariable.getName() + "'");
+//
+// // Create pair (column,row)
+// std::pair<std::string, std::string> variablePair(integerVariable.getName() + "'", integerVariable.getName());
+// metaVariablePairs.push_back(variablePair);
+// }
+// }
+//
+// std::cout << "Variable Ordering: ";
+// for(auto x: manager->getDdVariableNames()){
+// std::cout << x << ",";
+// }
+// std::cout << std::endl;
+// std::cout << std::endl;
+// }
+//
+// template <storm::dd::DdType Type>
+// void SymbolicModelAdapter<Type>::GenerationInformation::createIdentityDecisionDiagrams() {
+//
+// // Global Boolean variables
+// for (uint_fast64_t j = 0; j < program.getGlobalBooleanVariables().size(); ++j) {
+// storm::prism::BooleanVariable const & booleanVariable = program.getGlobalBooleanVariables().at(j);
+//
+// storm::dd::Dd<Type> identity = manager->getZero();
+//
+// // f(0)=0 leads to 1
+// identity.setValue(booleanVariable.getName(), 0, booleanVariable.getName() + "'", 0, 1);
+// // f(1)=1 leads to 1
+// identity.setValue(booleanVariable.getName(), 1, booleanVariable.getName() + "'", 1, 1);
+//
+// variableToIdentityDecisionDiagramMap.insert(std::make_pair(booleanVariable.getName(), identity));
+// }
+//
+// // Global Integer variables
+// for (uint_fast64_t j = 0; j < program.getGlobalIntegerVariables().size(); ++j) {
+// storm::prism::IntegerVariable const& integerVariable = program.getGlobalIntegerVariables().at(j);
+// storm::dd::Dd<Type> identity = manager->getZero();
+//
+// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
+// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
+//
+// for (int_fast64_t i = low; i <= high; ++i) {
+// // f(i)=i leads to 1
+// identity.setValue(integerVariable.getName(), i, integerVariable.getName() + "'", i, 1);
+// }
+//
+// variableToIdentityDecisionDiagramMap.insert(std::make_pair(integerVariable.getName(), identity));
+// }
+//
+//
+// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+// storm::prism::Module const& module = program.getModule(i);
+//
+// // Module identity matrix
+// storm::dd::Dd<Type> moduleIdentity = manager->getOne();
+//
+// // Boolean variables
+// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
+// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(j);
+//
+// storm::dd::Dd<Type> identity = manager->getZero();
+//
+// // f(0)=0 leads to 1
+// identity.setValue(booleanVariable.getName(), 0, booleanVariable.getName() + "'", 0, 1);
+// // f(1)=1 leads to 1
+// identity.setValue(booleanVariable.getName(), 1, booleanVariable.getName() + "'", 1, 1);
+//
+// variableToIdentityDecisionDiagramMap.insert(std::make_pair(booleanVariable.getName(), identity));
+// moduleIdentity = moduleIdentity * identity;
+// }
+//
+// // Integer variables
+// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
+// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(j);
+// storm::dd::Dd<Type> identity = manager->getZero();
+//
+// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
+// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
+//
+// for (int_fast64_t i = low; i <= high; ++i) {
+// // f(i)=i leads to 1
+// identity.setValue(integerVariable.getName(), i, integerVariable.getName() + "'", i, 1);
+// }
+//
+// variableToIdentityDecisionDiagramMap.insert(std::make_pair(integerVariable.getName(), identity));
+// moduleIdentity = moduleIdentity * identity;
+// }
+//
+// // Create module identity matrix
+// moduleToIdentityDecisionDiagramMap.insert(std::make_pair(module.getName(), moduleIdentity));
+// }
+//
+// }
+//
+// template <storm::dd::DdType Type>
+// storm::dd::Dd<Type> SymbolicModelAdapter<Type>::createSystemDecisionDiagramm(GenerationInformation & generationInfo){
+//
+// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size();
+//
+// // System DDs
+// SystemComponentDecisionDiagram<Type> systemDds(0);
+// SystemComponentDecisionDiagram<Type> systemDds1(0);
+// SystemComponentDecisionDiagram<Type> systemDds2(0);
+//
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+//
+// // Initialize usedNondetVariablesVector
+// // TODO: Formulate simpler.
+// std::vector<uint_fast64_t> usedNondetVariablesVector(numberOfSynchronizingActions);
+// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j) {
+// usedNondetVariablesVector[j] = 0;
+// }
+//
+// // Create DD for first module
+// systemDds = createSystemComponentDecisionDiagramm(generationInfo, generationInfo.program.getModule(0), usedNondetVariablesVector);
+//
+// for (uint_fast64_t i = 1; i < generationInfo.program.getNumberOfModules(); ++i) {
+//
+// // Create new usedNondetVariablesVector
+// std::vector<uint_fast64_t> newUsedNondetVariablesVector(numberOfSynchronizingActions);
+// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j) {
+// // Check if systemDds contains action
+// if (std::find(systemDds.allSynchronizingActions.begin(), systemDds.allSynchronizingActions.end(), generationInfo.allSynchronizingActions[j]) != systemDds.allSynchronizingActions.end()) {
+// newUsedNondetVariablesVector[j] = systemDds.synchronizingActionDds[j].usedNondetVariables;
+// }
+// else{
+// newUsedNondetVariablesVector[j] = usedNondetVariablesVector[j];
+// }
+// }
+//
+// // Create DD for next module
+// systemDds2 = createSystemComponentDecisionDiagramm(generationInfo, generationInfo.program.getModule(i), newUsedNondetVariablesVector);
+//
+// // SystemDds1 stores the previous modules (already combined)
+// systemDds1 = SystemComponentDecisionDiagram<Type>(systemDds);
+//
+// // SystemDds is used to store combination of SystemDds1 and SystemDds2
+// systemDds = SystemComponentDecisionDiagram<Type>(numberOfSynchronizingActions);
+//
+// // Combine non-synchronizing/independent actions
+// systemDds.independentActionDd = combineModules(generationInfo, false, systemDds1.independentActionDd, systemDds2.independentActionDd, systemDds1.identityMatrix, systemDds2.identityMatrix);
+//
+// // Combine synchronizing actions
+// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j){
+// // Check if both modules contain the current action
+// if (std::find(systemDds1.allSynchronizingActions.begin(), systemDds1.allSynchronizingActions.end(), generationInfo.allSynchronizingActions[j]) != systemDds1.allSynchronizingActions.end() &&
+// std::find(systemDds2.allSynchronizingActions.begin(), systemDds2.allSynchronizingActions.end(), generationInfo.allSynchronizingActions[j]) != systemDds2.allSynchronizingActions.end()) {
+// // Both modules contain action
+// systemDds.synchronizingActionDds[j] = combineModules(generationInfo, true, systemDds1.synchronizingActionDds[j], systemDds2.synchronizingActionDds[j], systemDds1.identityMatrix, systemDds2.identityMatrix);
+// }
+// else {
+// // Only one or no module contains current action
+// systemDds.synchronizingActionDds[j] = combineModules(generationInfo, false, systemDds1.synchronizingActionDds[j], systemDds2.synchronizingActionDds[j], systemDds1.identityMatrix, systemDds2.identityMatrix);
+// }
+// }
+//
+// // Combine identity matrix
+// systemDds.identityMatrix = systemDds1.identityMatrix * systemDds2.identityMatrix;
+//
+// // Combine list of synchronizing actions
+// systemDds.allSynchronizingActions.insert(systemDds1.allSynchronizingActions.begin(), systemDds1.allSynchronizingActions.end());
+// systemDds.allSynchronizingActions.insert(systemDds2.allSynchronizingActions.begin(), systemDds2.allSynchronizingActions.end());
+// }
+//
+// // Combine all DDs
+// systemDds = combineSystem(generationInfo, systemDds);
+// generationInfo.globalSystemDds = SystemComponentDecisionDiagram<Type>(systemDds);
+//
+//
+// // Build state and transition rewards
+// generationInfo.rewardDds = computeRewards(generationInfo, systemDds);
+//
+// // Create transition to action mapping for MDPs
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// generationInfo.transitionActionDd = computeTransitionAction(generationInfo, systemDds);
+// }
+//
+// // Normalize each row for DTMCs
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
+// temporary = storm::dd::Dd<Type>(systemDds.independentActionDd.commandsDd);
+// temporary = temporary.sumAbstract(generationInfo.columnMetaVariableNames);
+// systemDds.independentActionDd.commandsDd = systemDds.independentActionDd.commandsDd / temporary;
+// }
+//
+// // Get system transition matrix
+// storm::dd::Dd<Type> systemTransitionMatrix = systemDds.independentActionDd.commandsDd;
+//
+// return systemTransitionMatrix;
+// }
+//
+// template <storm::dd::DdType Type>
+// SystemComponentDecisionDiagram<Type> SymbolicModelAdapter<Type>::combineSystem(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram<Type> systemDds){
+//
+// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size();
+// uint_fast64_t max = 0;
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+// storm::dd::Dd<Type> variableDd = generationInfo.manager->getZero();
+//
+// // Add non-determinism variables for MDPs
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// // Check DD variables
+//
+// // Look for maximal variable index
+// max = systemDds.independentActionDd.usedNondetVariables;
+// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){
+// if (systemDds.synchronizingActionDds[i].usedNondetVariables > max) {
+// max = systemDds.synchronizingActionDds[i].usedNondetVariables;
+// }
+// }
+//
+// // Add variables to independent action DD (if required)
+// if (max > systemDds.independentActionDd.usedNondetVariables) {
+// temporary = generationInfo.manager->getOne();
+// for (uint_fast64_t i = systemDds.independentActionDd.usedNondetVariables+1; i <= max; ++i){
+//
+// // Get variable and set to 0
+// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0);
+// temporary = temporary * variableDd;
+//
+// }
+// systemDds.independentActionDd.commandsDd = systemDds.independentActionDd.commandsDd * temporary;
+// systemDds.independentActionDd.usedNondetVariables = max;
+// }
+//
+// // Add variables to synchronized action DDs
+// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j){
+// if (max > systemDds.synchronizingActionDds[j].usedNondetVariables) {
+// temporary = generationInfo.manager->getOne();
+// for (uint_fast64_t i = systemDds.synchronizingActionDds[j].usedNondetVariables+1; i <= max; ++i){
+//
+// // Get variable and set to 0
+// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0);
+// temporary = temporary * variableDd;
+//
+// }
+// systemDds.synchronizingActionDds[j].commandsDd = systemDds.synchronizingActionDds[j].commandsDd * temporary;
+// systemDds.synchronizingActionDds[j].usedNondetVariables = max;
+// }
+// }
+//
+// // Set variables for synchronization
+// temporary = generationInfo.manager->getOne();
+// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){
+// // Get sync variable
+// variableDd = generationInfo.manager->getEncoding("sync" + std::to_string(i), 0);
+// temporary = temporary * variableDd;
+// }
+//
+// systemDds.independentActionDd.commandsDd = temporary * systemDds.independentActionDd.commandsDd;
+//
+// // Set variables for synchronized action DDs
+// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){
+// temporary = generationInfo.manager->getOne();
+// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j){
+// // Enable synchronizing variable j iff current action i==j
+// if (i == j) {
+// variableDd = generationInfo.manager->getEncoding("sync" + std::to_string(j), 1);
+// temporary = temporary * variableDd;
+// }
+// else {
+// variableDd = generationInfo.manager->getEncoding("sync" + std::to_string(j), 0);
+// temporary = temporary * variableDd;
+// }
+// }
+//
+// systemDds.synchronizingActionDds[i].commandsDd = temporary * systemDds.synchronizingActionDds[i].commandsDd;
+// }
+//
+// }
+//
+// // Create transition matrix
+// temporary = systemDds.independentActionDd.commandsDd;
+// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){
+// temporary = temporary + systemDds.synchronizingActionDds[i].commandsDd;
+// }
+//
+// // Store transition matrix in systemDDs structure
+// systemDds.independentActionDd.commandsDd = temporary;
+//
+// return systemDds;
+// }
+//
+// template <storm::dd::DdType Type>
+// ModuleDecisionDiagram<Type> SymbolicModelAdapter<Type>::combineModules(GenerationInformation const & generationInfo, bool synchronizing, ModuleDecisionDiagram<Type> moduleDd1, ModuleDecisionDiagram<Type> moduleDd2, storm::dd::Dd<Type> const& identityDd1, storm::dd::Dd<Type> const& identityDd2){
+//
+// // Module DD
+// ModuleDecisionDiagram<Type> moduleDd = ModuleDecisionDiagram<Type>();
+//
+// if (synchronizing) {
+// // Synchronizing actions
+//
+// // Combine guards (intersection)
+// moduleDd.guardDd = moduleDd1.guardDd * moduleDd2.guardDd;
+//
+// // Combine transitions
+// moduleDd.commandsDd = moduleDd1.commandsDd * moduleDd2.commandsDd;
+//
+// // Update min/max index
+// moduleDd.usedNondetVariables = (moduleDd1.usedNondetVariables > moduleDd2.usedNondetVariables) ? moduleDd1.usedNondetVariables : moduleDd2.usedNondetVariables;
+//
+// } else {
+// // Non-synchronizing actions
+//
+// // Multiply commands with identity matrix (because of non-synchronization)
+// moduleDd1.commandsDd = moduleDd1.commandsDd * identityDd2;
+// moduleDd2.commandsDd = moduleDd2.commandsDd * identityDd1;
+//
+// // Combine modules
+// switch (generationInfo.program.getModelType()) {
+// case storm::prism::Program::ModelType::DTMC:
+//
+// // No non-determinism, just sum up
+// moduleDd.guardDd = moduleDd1.guardDd + moduleDd2.guardDd;
+// moduleDd.commandsDd = moduleDd1.commandsDd + moduleDd2.commandsDd;
+// moduleDd.usedNondetVariables = 0;
+// break;
+// case storm::prism::Program::ModelType::MDP:
+//
+// // Combine modules and solve non-determinism
+// moduleDd = combineModulesMDP(generationInfo, moduleDd1, moduleDd2);
+// break;
+// default:
+// STORM_LOG_ASSERT(false, "Illegal model type.");
+// }
+// }
+//
+// return moduleDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// ModuleDecisionDiagram<Type> SymbolicModelAdapter<Type>::combineModulesMDP(GenerationInformation const & generationInfo, ModuleDecisionDiagram<Type> moduleDd1, ModuleDecisionDiagram<Type> moduleDd2){
+//
+// // Module DD
+// ModuleDecisionDiagram<Type> moduleDd = ModuleDecisionDiagram<Type>();
+//
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+// storm::dd::Dd<Type> variableDd = generationInfo.manager->getZero();
+//
+// // Check if one command DD equals 0
+// if (moduleDd1.commandsDd.isZero()) {
+// moduleDd.guardDd = moduleDd2.guardDd;
+// moduleDd.commandsDd = moduleDd2.commandsDd;
+// moduleDd.usedNondetVariables = moduleDd2.usedNondetVariables;
+// return moduleDd;
+// }
+// if (moduleDd2.commandsDd.isZero()) {
+// moduleDd.guardDd = moduleDd1.guardDd;
+// moduleDd.commandsDd = moduleDd1.commandsDd;
+// moduleDd.usedNondetVariables = moduleDd1.usedNondetVariables;
+// return moduleDd;
+// }
+//
+// // Solve non-determinism
+//
+// // Check index of DD variables
+// if (moduleDd1.usedNondetVariables > moduleDd2.usedNondetVariables) {
+// temporary = generationInfo.manager->getOne();
+//
+// for (uint_fast64_t i = moduleDd2.usedNondetVariables+1; i <= moduleDd1.usedNondetVariables; ++i){
+// // Get variable and set to 0
+// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0);
+// temporary = temporary * variableDd;
+// }
+// moduleDd2.commandsDd = moduleDd2.commandsDd * temporary;
+// moduleDd2.usedNondetVariables = moduleDd1.usedNondetVariables;
+// }
+// if (moduleDd2.usedNondetVariables > moduleDd1.usedNondetVariables) {
+// temporary = generationInfo.manager->getOne();
+//
+// for (uint_fast64_t i = moduleDd1.usedNondetVariables+1; i <= moduleDd2.usedNondetVariables; ++i){
+// // Get variable and set to 0
+// variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0);
+// temporary = temporary * variableDd;
+// }
+// moduleDd1.commandsDd = moduleDd1.commandsDd * temporary;
+// moduleDd1.usedNondetVariables = moduleDd2.usedNondetVariables;
+// }
+//
+// // Get new nondet. variable
+// variableDd = variableDd = generationInfo.manager->getEncoding("nondet" + std::to_string(moduleDd1.usedNondetVariables + 1), 1);
+//
+// // Set nondet. variable
+// moduleDd2.commandsDd = moduleDd2.commandsDd * variableDd;
+// moduleDd1.commandsDd = moduleDd1.commandsDd * (!variableDd);
+//
+// // Combine command DDs
+// moduleDd.commandsDd = moduleDd1.commandsDd + moduleDd2.commandsDd;
+//
+// // Combine guard DDs
+// moduleDd.guardDd = moduleDd1.guardDd || moduleDd2.guardDd;
+//
+// moduleDd.usedNondetVariables = moduleDd1.usedNondetVariables + 1;
+//
+// return moduleDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// SystemComponentDecisionDiagram<Type> SymbolicModelAdapter<Type>::createSystemComponentDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, std::vector<uint_fast64_t> usedNondetVariablesVector){
+//
+// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size();
+//
+// // System Component DD
+// SystemComponentDecisionDiagram<Type> systemComponentDd(numberOfSynchronizingActions);
+//
+// // Create module DD for independent actions
+// systemComponentDd.independentActionDd = createModuleDecisionDiagramm(generationInfo, module, "", 0);
+//
+// // Create module DD for synchronizing actions
+// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i){
+//
+// if (module.hasAction(generationInfo.allSynchronizingActions[i])){
+// systemComponentDd.synchronizingActionDds[i] = createModuleDecisionDiagramm(generationInfo, module, generationInfo.allSynchronizingActions[i], usedNondetVariablesVector[i]);
+// }else{
+// switch (generationInfo.program.getModelType()){
+// case storm::prism::Program::ModelType::DTMC:
+// systemComponentDd.synchronizingActionDds[i] = ModuleDecisionDiagram<Type>(generationInfo.manager->getZero(), generationInfo.manager->getZero(), 0);
+// break;
+// case storm::prism::Program::ModelType::MDP:
+// systemComponentDd.synchronizingActionDds[i] = ModuleDecisionDiagram<Type>(generationInfo.manager->getZero(), generationInfo.manager->getZero(), usedNondetVariablesVector[i]);
+// break;
+// default:
+// STORM_LOG_ASSERT(false, "Illegal model type.");
+// }
+// }
+//
+// }
+//
+// // Get module identity matrix
+// systemComponentDd.identityMatrix = generationInfo.moduleToIdentityDecisionDiagramMap.at(module.getName());
+//
+// // Store all synchronizing actions
+// systemComponentDd.allSynchronizingActions.insert(module.getActions().begin(), module.getActions().end());
+//
+// return systemComponentDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// ModuleDecisionDiagram<Type> SymbolicModelAdapter<Type>::combineCommandsDTMC(std::shared_ptr<storm::dd::DdManager<Type>> const & manager, uint_fast64_t numberOfCommands, std::vector<storm::dd::Dd<Type>> const& commandDds, std::vector<storm::dd::Dd<Type>> const & guardDds){
+//
+// // Module DD
+// ModuleDecisionDiagram<Type> moduleDd;
+//
+// // Initialize DDs
+// storm::dd::Dd<Type> guardRangeDd = manager->getZero();
+// storm::dd::Dd<Type> commandsDd = manager->getZero();
+// storm::dd::Dd<Type> temporary = manager->getZero();
+//
+// for (uint_fast64_t i = 0; i < numberOfCommands; ++i) {
+//
+// // Check guard
+// if (guardDds[i].isZero()) continue;
+//
+// // Check for overlapping guards
+// temporary = guardDds[i] * guardRangeDd;
+// if (!(temporary.isZero())) {
+// LOG4CPLUS_WARN(logger, "Overlapping guard in command " << (i + 1) << ".");
+// }
+//
+// // Sum up all guards
+// guardRangeDd = guardRangeDd + guardDds[i];
+//
+// // Create command DD (multiply guard and updates)
+// temporary = guardDds[i] * commandDds[i];
+//
+// // Sum up all command DDs
+// commandsDd = commandsDd + temporary;
+// }
+//
+// moduleDd.guardDd = guardRangeDd;
+// moduleDd.commandsDd = commandsDd;
+// moduleDd.usedNondetVariables = 0;
+//
+// return moduleDd;
+// }
+//
+// // TODO
+// std::map<std::string, int_fast64_t> getMetaVariableMapping(std::vector<std::string> metaVariables, uint_fast64_t value){
+//
+// std::map<std::string, int_fast64_t> metaVariableNameToValueMap = std::map<std::string, int_fast64_t>();
+//
+// for (uint_fast64_t i = 0; i < metaVariables.size(); ++i) {
+// if (value & (1ull << (metaVariables.size() - i - 1))) {
+// metaVariableNameToValueMap.insert(std::make_pair(metaVariables[i], 1));
+// }
+// else {
+// metaVariableNameToValueMap.insert(std::make_pair(metaVariables[i], 0));
+// }
+// }
+//
+// return metaVariableNameToValueMap;
+// }
+//
+// template <storm::dd::DdType Type>
+// ModuleDecisionDiagram<Type> SymbolicModelAdapter<Type>::combineCommandsMDP(std::shared_ptr<storm::dd::DdManager<Type>> const & manager, uint_fast64_t numberOfCommands, std::vector<storm::dd::Dd<Type>> const& commandDds, std::vector<storm::dd::Dd<Type>> const & guardDds, uint_fast64_t usedNondetVariables){
+//
+// // Module DD
+// ModuleDecisionDiagram<Type> moduleDd = ModuleDecisionDiagram<Type>();
+//
+// // Initialize DDs
+// storm::dd::Dd<Type> guardRangeDd = manager->getZero();
+// storm::dd::Dd<Type> commandsDd = manager->getZero();
+// storm::dd::Dd<Type> temporaryDd = manager->getZero();
+//
+// // Check for overlapping guards
+// storm::dd::Dd<Type> overlappingGuardDd = manager->getZero();
+//
+// for (uint_fast64_t i = 0; i < numberOfCommands; ++i) {
+// overlappingGuardDd = overlappingGuardDd + guardDds[i];
+// guardRangeDd = guardRangeDd || guardDds[i];
+// }
+//
+// uint_fast64_t maxChoices = overlappingGuardDd.getMax();
+//
+// // Check for no choice or no non-determinism
+// if (maxChoices == 0 || maxChoices == 1) {
+//
+// if (maxChoices == 1) {
+// // Sum up all command updates
+// for (uint_fast64_t i = 0; i < numberOfCommands; ++i) {
+// temporaryDd = guardDds[i] * commandDds[i];
+// commandsDd = commandsDd + temporaryDd;
+// }
+// }
+//
+// moduleDd.guardDd = guardRangeDd;
+// moduleDd.commandsDd = commandsDd;
+// moduleDd.usedNondetVariables = usedNondetVariables;
+//
+// return moduleDd;
+// }
+//
+// // Calculate number of required variables (log2(maxChoices))
+// uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(log2(maxChoices)));
+//
+// // Allocate local nondet. choice variables
+// std::vector<std::string> nondetVariables(numberOfBinaryVariables);
+// for (uint_fast64_t i = 1; i <= numberOfBinaryVariables; ++i) {
+// nondetVariables[i-1] = "nondet" + std::to_string(usedNondetVariables + i);
+// }
+//
+// // Initialize more DDs
+// storm::dd::Dd<Type> equalsNumberOfChoicesDd = manager->getZero();
+// std::vector<storm::dd::Dd<Type>> choiceDds(maxChoices);
+// std::vector<storm::dd::Dd<Type>> remainingDds(maxChoices);
+//
+// storm::dd::Dd<Type> temporaryDd1 = manager->getZero();
+// storm::dd::Dd<Type> temporaryDd2 = manager->getZero();
+//
+// for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
+//
+// // Check for paths with exactly i nondet. choices
+// equalsNumberOfChoicesDd = overlappingGuardDd.equals(manager->getConstant(static_cast<double> (currentChoices)));
+//
+// if (equalsNumberOfChoicesDd.isZero()) continue;
+//
+// // Reset DDs
+// for (uint_fast64_t j = 0; j < currentChoices; ++j) {
+// choiceDds[j] = manager->getZero();
+// remainingDds[j] = equalsNumberOfChoicesDd;
+// }
+//
+// // Check all commands
+// for (uint_fast64_t j = 0; j < numberOfCommands; ++j) {
+//
+// // Check if command guard overlaps with equalsNumberOfChoicesDd
+// temporaryDd1 = guardDds[j] && equalsNumberOfChoicesDd;
+// if (temporaryDd1.isZero()) continue;
+//
+// // Split nondet. choices
+// for (uint_fast64_t k = 0; k < currentChoices; ++k) {
+//
+// // Calculate maximal overlapping parts of command guard and remaining DD (for current index)
+// temporaryDd2 = temporaryDd1 && remainingDds[k];
+//
+// // Check if we can add some overlapping parts to the current index
+// if (temporaryDd2 != manager->getZero()) {
+//
+// // Remove overlapping parts from the remaining DD
+// remainingDds[k] = remainingDds[k] && (!temporaryDd2);
+//
+// // Combine guard (overlapping parts) with command updates
+// temporaryDd = temporaryDd2 * commandDds[j];
+// // Add command DD to the commands with current index
+// choiceDds[k] = choiceDds[k] + temporaryDd;
+// }
+//
+// // Remove overlapping parts from the command guard DD
+// temporaryDd1 = temporaryDd1 && (!temporaryDd2);
+//
+// // Check if the command guard DD is already 0
+// if (temporaryDd1.isZero()) break;
+// }
+// }
+//
+// // Set nondet. choices for corresponding DDs
+// for (uint_fast64_t j = 0; j < currentChoices; ++j) {
+//
+// temporaryDd1 = manager->getZero();
+//
+// // Set chosen variables to value j
+// temporaryDd1.setValue(getMetaVariableMapping(nondetVariables, j), 1);
+//
+// // Multiply setting of nondet. variables with corresponding commands
+// temporaryDd = temporaryDd1 * choiceDds[j];
+// // Sum up all DDs (no non-determinism any more)
+// commandsDd = commandsDd + temporaryDd;
+// }
+//
+// // Delete currentChoices out of overlapping DD
+// overlappingGuardDd = overlappingGuardDd * (!equalsNumberOfChoicesDd);
+// }
+//
+// moduleDd.guardDd = guardRangeDd;
+// moduleDd.commandsDd = commandsDd;
+// moduleDd.usedNondetVariables = usedNondetVariables + numberOfBinaryVariables;
+//
+// return moduleDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// ModuleDecisionDiagram<Type> SymbolicModelAdapter<Type>::createModuleDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, std::string const& synchronizingAction, uint_fast64_t usedNondetVariables){
+//
+// // Module DD
+// ModuleDecisionDiagram<Type> moduleDd;
+//
+// // Set up vectors
+// uint_fast64_t numberOfCommands = module.getNumberOfCommands();
+// std::vector<storm::dd::Dd<Type>> guardDds(numberOfCommands);
+// std::vector<storm::dd::Dd<Type>> commandDds(numberOfCommands);
+//
+// for (uint_fast64_t j = 0; j < numberOfCommands; ++j) {
+//
+// storm::prism::Command const& command = module.getCommand(j);
+//
+// // Check if command action matches requested synchronizing action
+// if (synchronizingAction == command.getActionName()) {
+//
+// // Translate guard
+// guardDds[j] = storm::adapters::SymbolicExpressionAdapter<Type>::translateExpression(command.getGuardExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager);
+//
+// if (guardDds[j].isZero()){
+// LOG4CPLUS_WARN(logger, "A guard is unsatisfiable.");
+// }
+//
+// // Create command DD
+// commandDds[j] = createCommandDecisionDiagramm(generationInfo, module, guardDds[j], command);
+//
+// commandDds[j] = commandDds[j] * guardDds[j];
+//
+// // check negative probabilities/rates
+// if (commandDds[j].getMin() < 0){
+// LOG4CPLUS_WARN(logger, "Negative probabilites/rates in command " << (j + 1) << ".");
+// }
+// }
+// else {
+// // Otherwise use zero DDs
+// guardDds[j] = generationInfo.manager->getZero();
+// commandDds[j] = generationInfo.manager->getZero();
+// }
+// }
+//
+// // combine command DDs with guard DDs
+// switch (generationInfo.program.getModelType()){
+// case storm::prism::Program::ModelType::DTMC:
+// moduleDd = combineCommandsDTMC(generationInfo.manager, numberOfCommands, commandDds, guardDds);
+// break;
+// case storm::prism::Program::ModelType::MDP:
+// moduleDd = combineCommandsMDP(generationInfo.manager, numberOfCommands, commandDds, guardDds, usedNondetVariables);
+// break;
+// default:
+// STORM_LOG_ASSERT(false, "Illegal model type.");
+// }
+//
+// return moduleDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// storm::dd::Dd<Type> SymbolicModelAdapter<Type>::createCommandDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd<Type> const& guard, storm::prism::Command const& command){
+//
+// // Command DD
+// storm::dd::Dd<Type> commandDd = generationInfo.manager->getZero();
+//
+// for (uint_fast64_t i = 0; i < command.getNumberOfUpdates(); ++i) {
+//
+// // Create update DD
+// storm::dd::Dd<Type> updateDd = createUpdateDecisionDiagramm(generationInfo, module, guard, command.getUpdate(i));
+//
+// if (updateDd.isZero()){
+// LOG4CPLUS_WARN(logger, "Update " << (i + 1) << " does not do anything.");
+// }
+//
+// // Multiply likelihood expression (MDP: transition probability)
+// double p = command.getUpdate(i).getLikelihoodExpression().evaluateAsDouble();
+//
+// updateDd = updateDd * generationInfo.manager->getConstant(p);
+//
+// commandDd = commandDd + updateDd;
+// }
+//
+// return commandDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// storm::dd::Dd<Type> SymbolicModelAdapter<Type>::createUpdateDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd<Type> const& guard, storm::prism::Update const& update){
+//
+// // Update DD
+// storm::dd::Dd<Type> updateDd = generationInfo.manager->getOne();
+//
+// // Assignments (integer and boolean)
+// std::vector<storm::prism::Assignment> assignments = update.getAssignments();
+// for (auto singleAssignment : assignments) {
+//
+// // Translate first part of assignment
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+//
+// temporary = generationInfo.manager->getIdentity(singleAssignment.getVariableName() + "'");
+//
+// // Translate second part of assignment
+// storm::dd::Dd<Type> updateExpr = storm::adapters::SymbolicExpressionAdapter<Type>::translateExpression(singleAssignment.getExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager);
+//
+// storm::dd::Dd<Type> result = updateExpr * guard;
+// // Combine first and second part of the assignment
+// result = result.equals(temporary);
+// result = result * guard;
+//
+// // Filter range
+// result = result * generationInfo.manager->getRange(singleAssignment.getVariableName() + "'");
+//
+// updateDd = updateDd * result;
+// }
+//
+// // All unused global boolean variables do not change
+// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalBooleanVariables().size(); ++i) {
+// storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(i);
+// if (update.getAssignmentMapping().find(booleanVariable.getName()) == update.getAssignmentMapping().end()) {
+// // Multiply identity matrix
+// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(booleanVariable.getName());
+// }
+// }
+//
+// // All unused global integer variables do not change
+// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalIntegerVariables().size(); ++i) {
+// storm::prism::IntegerVariable const& integerVariable = generationInfo.program.getGlobalIntegerVariables().at(i);
+// if (update.getAssignmentMapping().find(integerVariable.getName()) == update.getAssignmentMapping().end()) {
+// // Multiply identity matrix
+// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName());
+// }
+// }
+//
+// // All unused boolean variables do not change
+// for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); ++i) {
+// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(i);
+// if (update.getAssignmentMapping().find(booleanVariable.getName()) == update.getAssignmentMapping().end()) {
+// // Multiply identity matrix
+// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(booleanVariable.getName());
+// }
+// }
+//
+// // All unused integer variables do not change
+// for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); ++i) {
+// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(i);
+// if (update.getAssignmentMapping().find(integerVariable.getName()) == update.getAssignmentMapping().end()) {
+// // Multiply identity matrix
+// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName());
+// }
+// }
+//
+// return updateDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// storm::dd::Dd<Type> SymbolicModelAdapter<Type>::getInitialStateDecisionDiagram(GenerationInformation const & generationInfo) {
+// storm::dd::Dd<Type> initialStates = generationInfo.manager->getOne();
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+//
+// // Global Boolean variables
+// for (uint_fast64_t j = 0; j < generationInfo.program.getGlobalBooleanVariables().size(); ++j) {
+// storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(j);
+// temporary = generationInfo.manager->getEncoding(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool());
+// initialStates = initialStates * temporary;
+// }
+//
+// // Global Integer variables
+// for (uint_fast64_t j = 0; j < generationInfo.program.getGlobalIntegerVariables().size(); ++j) {
+// storm::prism::IntegerVariable const& integerVariable = generationInfo.program.getGlobalIntegerVariables().at(j);
+// temporary = generationInfo.manager->getEncoding(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt());
+// initialStates = initialStates * temporary;
+// }
+//
+// for (uint_fast64_t i = 0; i < generationInfo.program.getNumberOfModules(); ++i) {
+// storm::prism::Module const& module = generationInfo.program.getModule(i);
+//
+// // Boolean variables
+// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
+// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(j);
+// temporary = generationInfo.manager->getEncoding(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool());
+// initialStates = initialStates * temporary;
+// }
+//
+// // Integer variables
+// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
+// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(j);
+// temporary = generationInfo.manager->getEncoding(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt());
+// initialStates = initialStates * temporary;
+// }
+// }
+//
+// return initialStates;
+// }
+//
+// template <storm::dd::DdType Type>
+// storm::dd::Dd<Type> SymbolicModelAdapter<Type>::performReachability(GenerationInformation & generationInfo, storm::dd::Dd<Type> const& systemDd, storm::dd::Dd<Type> const& initialStateDd) {
+//
+// // Initialize the clock.
+// auto clock = std::chrono::high_resolution_clock::now();
+//
+//
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+// storm::dd::Dd<Type> S;
+// storm::dd::Dd<Type> U;
+//
+// // Get initial state
+// storm::dd::Dd<Type> reachableStates = initialStateDd;
+//
+// // Copy current state
+// storm::dd::Dd<Type> newReachableStates = reachableStates;
+//
+// std::set<std::string> abstractVariables = std::set<std::string>();
+//
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) {
+// // Synchronizing variables
+// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) {
+// abstractVariables.insert("sync" + std::to_string(i));
+// }
+// }
+// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) {
+// // Nondet. variables
+// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) {
+// abstractVariables.insert("nondet" + std::to_string(i));
+// }
+// }
+// }
+//
+// // Create system BDD
+// storm::dd::Dd<Type> systemBdd = systemDd.notZero();
+//
+// // For MDPs, we need to abstract from the nondeterminism variables, but we can do so prior to the
+// // reachability analysis.
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// // Abstract from synchronizing and nondet. variables (MDPs)
+// systemBdd = systemBdd.existsAbstract(abstractVariables);
+// }
+//
+// // Initialize variables and choose option
+// bool changed;
+// int iter = 0;
+// int option = storm::settings::adapterSettings().getReachabilityMethod();
+//
+// //TODO: Name reachability options.
+// std::cout << "Reachability option: " << option << std::endl;
+//
+// if (option == 3 || option == 4){
+//
+// S = storm::dd::Dd<Type>(initialStateDd);
+// U = storm::dd::Dd<Type>(initialStateDd);
+//
+// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.notZero();
+// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.existsAbstract(abstractVariables);
+//
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) {
+// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.notZero();
+// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.existsAbstract(abstractVariables);
+// }
+// }
+//
+// // Perform updates until nothing changes
+// do {
+// if (option == 1){
+// iter++;
+// changed = true;
+//
+// newReachableStates = newReachableStates * systemBdd;
+//
+// // Abstract from row meta variables
+// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames);
+//
+// // Swap column variables to row variables
+// newReachableStates.swapVariables(generationInfo.metaVariablePairs);
+//
+// newReachableStates = newReachableStates * (!reachableStates);
+//
+// // Check if something has changed
+// if (newReachableStates.isZero()) {
+// changed = false;
+// }
+//
+// // Update reachableStates DD
+// reachableStates = reachableStates + newReachableStates;
+//
+// } else if (option == 2) {
+// iter++;
+// changed = false;
+//
+// newReachableStates = newReachableStates * systemBdd;
+//
+// // Abstract from row meta variables
+// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames);
+//
+// // Swap column variables to row variables
+// newReachableStates.swapVariables(generationInfo.metaVariablePairs);
+//
+// newReachableStates = newReachableStates || reachableStates;
+//
+// // Check if something has changed
+// if (newReachableStates != reachableStates) {
+// changed = true;
+// }
+//
+// // Update reachableStates DD
+// reachableStates = newReachableStates;
+//
+// } else if (option == 3) {
+// iter++;
+// changed = true;
+//
+// newReachableStates = generationInfo.manager->getZero();
+//
+// temporary = U * generationInfo.globalSystemDds.independentActionDd.commandsDd;
+// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames);
+// newReachableStates.swapVariables(generationInfo.metaVariablePairs);
+// newReachableStates = temporary;
+//
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) {
+// temporary = U * generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd;
+// temporary = temporary.existsAbstract(generationInfo.rowMetaVariableNames);
+// temporary.swapVariables(generationInfo.metaVariablePairs);
+// newReachableStates = newReachableStates || temporary;
+// }
+//
+// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames);
+// newReachableStates.swapVariables(generationInfo.metaVariablePairs);
+// U = U || newReachableStates;
+//
+// if (U == S){
+// changed = false;
+// reachableStates = S;
+// break;
+// }
+//
+// S = S || U;
+//
+// }
+// else if (option == 4) {
+// iter++;
+// changed = true;
+//
+// temporary = U * generationInfo.globalSystemDds.independentActionDd.commandsDd;
+// temporary = temporary.existsAbstract(generationInfo.rowMetaVariableNames);
+// temporary.swapVariables(generationInfo.metaVariablePairs);
+// U = U || temporary;
+//
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) {
+// temporary = U * generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd;
+// temporary = temporary.existsAbstract(generationInfo.rowMetaVariableNames);
+// temporary.swapVariables(generationInfo.metaVariablePairs);
+// U = U || temporary;
+// }
+//
+// U = U * (!S);
+//
+// S = S + U;
+//
+// if (U.isZero()){
+// changed = false;
+// reachableStates = S;
+// }
+//
+// }
+// } while (changed);
+//
+// std::cout << "Performed reachability (" << iter << " iterations) in " << std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl;
+//
+// return reachableStates;
+// }
+//
+// template <storm::dd::DdType Type>
+// storm::dd::Dd<Type> SymbolicModelAdapter<Type>::findDeadlocks(GenerationInformation const & generationInfo, storm::dd::Dd<Type> systemDd, storm::dd::Dd<Type> const& reachableStatesDd) {
+//
+// // Initialize the clock.
+// auto clock = std::chrono::high_resolution_clock::now();
+//
+// storm::dd::Dd<Type> systemBdd = systemDd.notZero();
+//
+// std::set<std::string> abstractVariables = std::set<std::string>();
+//
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) {
+// // Synchronizing variables
+// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) {
+// abstractVariables.insert("sync" + std::to_string(i));
+// }
+// }
+// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) {
+// // Nondet. variables
+// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) {
+// abstractVariables.insert("nondet" + std::to_string(i));
+// }
+// }
+// }
+//
+// // Find states with at least one transition
+// systemBdd = systemBdd.existsAbstract(generationInfo.columnMetaVariableNames);
+//
+// // For MDPs, we need to abstract from the nondeterminism variables
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// // Abstract from synchronizing and nondet. variables (MDPs)
+// systemBdd = systemBdd.existsAbstract(abstractVariables);
+// }
+//
+// systemBdd = reachableStatesDd * (!systemBdd);
+//
+// std::cout << "Deadlocks: " << systemBdd.getNonZeroCount() << " fixed." << std::endl;
+//
+// // Check if there are deadlocks
+// if (!systemBdd.isZero()){
+//
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getOne();
+//
+// // Get all variable identities
+// for (auto variable : generationInfo.rowMetaVariableNames) {
+// temporary = temporary * generationInfo.variableToIdentityDecisionDiagramMap.at(variable);
+// }
+//
+// // Add synchronizing and nondet. variables to identity for MDPs (all set to 0)
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) {
+// // Synchronizing variables
+// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) {
+// temporary = temporary * generationInfo.manager->getEncoding("sync" + std::to_string(i),0);
+// }
+// }
+// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) {
+// // Nondet. variables
+// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) {
+// temporary = temporary * generationInfo.manager->getEncoding("nondet" + std::to_string(i), 0);
+// }
+// }
+// }
+//
+// temporary = temporary * systemBdd;
+//
+// // Add self-loops to transition matrix
+// systemDd = systemDd + temporary;
+// }
+//
+// std::cout << "Fixed deadlocks in " << std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl;
+//
+// return systemDd;
+// }
+//
+// template <storm::dd::DdType Type>
+// std::pair<std::vector<storm::dd::Dd<Type>>, std::vector<storm::dd::Dd<Type>>> SymbolicModelAdapter<Type>::computeRewards(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram<Type> const& systemDds) {
+//
+// // Get number of reward modules and synchronizing actions
+// uint_fast64_t numberOfRewardModules = generationInfo.program.getRewardModels().size();
+// uint_fast64_t numberOfSynchronizingActions = generationInfo.allSynchronizingActions.size();
+//
+// // State reward DD
+// std::vector<storm::dd::Dd<Type>> stateRewardsDds = std::vector<storm::dd::Dd<Type>>(numberOfRewardModules);
+// // Transition reward DD
+// std::vector<storm::dd::Dd<Type>> transitionRewardsDds = std::vector<storm::dd::Dd<Type>>(numberOfRewardModules);
+//
+// // Initialize DDs
+// for (uint_fast64_t i = 0; i < numberOfRewardModules; ++i) {
+// stateRewardsDds[i] = generationInfo.manager->getConstant(0);
+// transitionRewardsDds[i] = generationInfo.manager->getConstant(0);
+// }
+//
+// storm::dd::Dd<Type> statesDd = generationInfo.manager->getZero();
+// storm::dd::Dd<Type> rewardsDd = generationInfo.manager->getZero();
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+//
+// // Loop through all reward models
+// for (uint_fast64_t i = 0; i < numberOfRewardModules; ++i) {
+// storm::prism::RewardModel const& currentRewardModule = generationInfo.program.getRewardModels().at(i);
+//
+// // State rewards
+// for (auto stateReward : currentRewardModule.getStateRewards()) {
+//
+// // Translate state and reward expression
+// statesDd = storm::adapters::SymbolicExpressionAdapter<Type>::translateExpression(stateReward.getStatePredicateExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager);
+// rewardsDd = storm::adapters::SymbolicExpressionAdapter<Type>::translateExpression(stateReward.getRewardValueExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager);
+//
+// // Restrict rewards to states
+// temporary = statesDd * rewardsDd;
+//
+// // Check for negative rewards
+// if (temporary.getMin() < 0){
+// LOG4CPLUS_WARN(logger, "Negative state reward in reward model " << (i + 1) << ".");
+// }
+//
+// if(temporary.isZero()) {
+// LOG4CPLUS_WARN(logger, "Only zero rewards in reward model " << (i + 1) << ".");
+// }
+//
+// // Combine all rewards
+// stateRewardsDds[i] = stateRewardsDds[i] + temporary;
+// }
+//
+// // Transition rewards
+// for (auto transitionReward : currentRewardModule.getTransitionRewards()) {
+//
+// // Translate state and reward expression
+// statesDd = storm::adapters::SymbolicExpressionAdapter<Type>::translateExpression(transitionReward.getStatePredicateExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager);
+// rewardsDd = storm::adapters::SymbolicExpressionAdapter<Type>::translateExpression(transitionReward.getRewardValueExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager);
+//
+// // Get action name of the transition
+// std::string const& rewardAction = transitionReward.getActionName();
+//
+// if (rewardAction == "") {
+// // Take independent action module
+// temporary = systemDds.independentActionDd.commandsDd;
+// }else {
+// // Get module corresponding to the reward action
+// for (uint_fast64_t j = 0; j < numberOfSynchronizingActions; ++j) {
+// if (generationInfo.allSynchronizingActions[j] == rewardAction) {
+// temporary = systemDds.synchronizingActionDds[j].commandsDd;
+// break;
+// }
+// }
+// }
+//
+// // Convert to BDD for MDPs (DTMC need exact values for scaling)
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+// temporary = temporary.notZero();
+// }
+//
+// // Restrict to states and multiply reward values
+// temporary = temporary * statesDd;
+// temporary = temporary * rewardsDd;
+//
+// // Check for negative rewards
+// if (temporary.getMin() < 0){
+// LOG4CPLUS_WARN(logger, "Negative transition reward in reward model " << (i + 1) << ".");
+// }
+//
+// // Combine all rewards
+// transitionRewardsDds[i] = transitionRewardsDds[i] + temporary;
+// }
+// }
+//
+// // Scale transition rewards for DTMCs
+// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
+// for (uint_fast64_t i = 0; i < generationInfo.program.getRewardModels().size(); ++i){
+// // Divide transition rewards through transition matrix
+// transitionRewardsDds[i] = transitionRewardsDds[i] / systemDds.independentActionDd.commandsDd;
+// }
+// }
+//
+// // Pair to store state and transition rewards
+// return std::make_pair(stateRewardsDds, transitionRewardsDds);
+// }
+//
+// template <storm::dd::DdType Type>
+// storm::dd::Dd<Type> SymbolicModelAdapter<Type>::computeTransitionAction(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram<Type> const& systemDds){
+//
+// // Transition actions DD
+// storm::dd::Dd<Type> transitionActionDd = generationInfo.manager->getZero();
+// storm::dd::Dd<Type> temporary = generationInfo.manager->getZero();
+//
+// // Store action labels for each transition (0 iff no action/tau/epsilon)
+// storm::dd::Dd<Type> commandsBdd = generationInfo.manager->getZero();
+// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i){
+// // Get action transition matrix as BDD
+// commandsBdd = systemDds.synchronizingActionDds[i].commandsDd.notZero();
+// commandsBdd = commandsBdd.existsAbstract(generationInfo.columnMetaVariableNames);
+//
+// // Add action index
+// temporary = commandsBdd * generationInfo.manager->getConstant(i + 1);
+// transitionActionDd = transitionActionDd + temporary;
+// }
+//
+// return transitionActionDd;
+// }
+
+ // Explicitly instantiate the symbolic expression adapter
+ template class DdPrismModelBuilder<storm::dd::DdType::CUDD>;
+
+ } // namespace adapters
+} // namespace storm
+
+
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
new file mode 100644
index 000000000..03283d55d
--- /dev/null
+++ b/src/builder/DdPrismModelBuilder.h
@@ -0,0 +1,282 @@
+#ifndef STORM_BUILDER_DDPRISMMODELBUILDER_H_
+#define STORM_BUILDER_DDPRISMMODELBUILDER_H_
+
+#include <map>
+#include <boost/optional.hpp>
+
+#include "src/logic/Formulas.h"
+#include "src/storage/prism/Program.h"
+#include "src/adapters/DdExpressionAdapter.h"
+
+namespace storm {
+ namespace adapters {
+
+ template <storm::dd::DdType Type>
+ class DdPrismModelBuilder {
+ public:
+ struct Options {
+ /*!
+ * Creates an object representing the default building options.
+ */
+ Options();
+
+ /*! Creates an object representing the suggested building options assuming that the given formula is the
+ * only one to check.
+ *
+ * @param formula The formula based on which to choose the building options.
+ */
+ Options(storm::logic::Formula const& formula);
+
+ /*!
+ * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c',
+ * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants.
+ *
+ * @param program The program managing the constants that shall be defined. Note that the program itself
+ * is not modified whatsoever.
+ * @param constantDefinitionString The string from which to parse the constants' values.
+ */
+ void addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString);
+
+ // A flag that indicates whether or not a reward model is to be built.
+ bool buildRewards;
+
+ // An optional string, that, if given, indicates which of the reward models is to be built.
+ boost::optional<std::string> rewardModelName;
+
+ // An optional mapping that, if given, contains defining expressions for undefined constants.
+ boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
+
+ // An optional set of labels that, if given, restricts the labels that are built.
+ boost::optional<std::set<std::string>> labelsToBuild;
+
+ // An optional set of expressions for which labels need to be built.
+ boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
+ };
+
+ /*!
+ * Translates the given program into a model that stores the transition relation as a decision diagram.
+ *
+ * @param program The program to translate.
+ */
+ static void translateProgram(storm::prism::Program const& program, Options const& options = Options());
+
+ private:
+ // This structure can store the decision diagrams representing a particular action.
+ struct ActionDecisionDiagram {
+ ActionDecisionDiagram(storm::dd::DdManager<Type> const& manager) : guardDd(manager.getZero()), transitionsDd(manager.getZero()), numberOfUsedNondeterminismVariables(0) {
+ // Intentionally left empty.
+ }
+
+ // The guard of the action.
+ storm::dd::Dd<Type> guardDd;
+
+ // The actual transitions (source and target states).
+ storm::dd::Dd<Type> transitionsDd;
+
+ // The number of variables that are used to encode the nondeterminism.
+ uint_fast64_t numberOfUsedNondeterminismVariables;
+ };
+
+ // This structure holds all decision diagrams related to a module.
+ struct ModuleDecisionDiagram {
+ ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independantAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()) {
+ // Intentionally left empty.
+ }
+
+ // The decision diagram for the independant action.
+ ActionDecisionDiagram independantAction;
+
+ // A mapping from synchronizing action indices to the decision diagram.
+ std::map<uint_fast64_t, ActionDecisionDiagram> synchronizingActionToDecisionDiagramMap;
+
+ // A decision diagram that represents the identity of this module.
+ storm::dd::Dd<Type> identity;
+ };
+
+ /*!
+ * Structure to store all information required to generate the model from the program.
+ */
+ class GenerationInformation {
+ GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), columnMetaVariables(), metaVariablePairs(), numberOfNondetVariables(0), variableToIdentityMap(), moduleToIdentityMap(), allSynchronizingActionIndices(), labelToStateDdMap() {
+ // Initializes variables and identity DDs.
+ createMetaVariables();
+ createIdentities();
+ }
+
+ private:
+ /*!
+ * Creates the required meta variables.
+ */
+ void createMetaVariables();
+
+ /*!
+ * Creates identity DDs for all variables and all modules.
+ */
+ void createIdentities();
+
+ // The program that is currently translated.
+ storm::prism::Program const& program;
+
+ // The manager used to build the decision diagrams.
+ std::shared_ptr<storm::dd::DdManager<Type>> manager;
+
+ // The meta variables for the row encoding.
+ std::vector<storm::expressions::Variable> rowMetaVariables;
+
+ // The meta variables for the column encoding.
+ std::vector<storm::expressions::Variable> columnMetaVariables;
+
+ // Pairs of meta variables (row, column).
+ std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> metaVariablePairs;
+
+ // Number of variables used to encode the nondeterminism.
+ uint_fast64_t numberOfNondetVariables;
+
+ // DDs representing the identity for each variable.
+ std::map<storm::expressions::Variable, storm::dd::Dd<Type>> variableToIdentityMap;
+
+ // DDs representing the identity for each module (index).
+ std::map<uint_fast64_t, storm::dd::Dd<Type>> moduleToIdentityMap;
+
+ // All synchronizing actions
+ std::set<uint_fast64_t> allSynchronizingActionIndices;
+
+ // DDs representing the identity matrix for each module
+ std::unordered_map<std::string, storm::dd::Dd<Type>> labelToStateDdMap;
+ };
+
+ private:
+
+// /*!
+// * Creates system DD (full parallel)
+// *
+// * @return A DD representing the whole system
+// */
+// static storm::dd::Dd<Type> createSystemDecisionDiagramm(GenerationInformation & generationInfo);
+//
+// /*!
+// * Combines all DDs to one DD (including independent/synchronized actions)
+// *
+// * @param systemDds DDs representing the whole system
+// * @return System DDs with combined independent/synchronized actions
+// */
+// static SystemComponentDecisionDiagram<Type> combineSystem(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram<Type> systemDds);
+//
+// /*!
+// * Combines 2 modules with/without synchronizing actions
+// *
+// * @param synchronizing Synchronizing actions or not
+// * @param module1 First module
+// * @param module1 Second module
+// * @param identity1 Identity matrix of first module
+// * @param identity2 Identity matrix of second module
+// * @return A module DD representing the combination of both modules
+// */
+// static ModuleDecisionDiagram<Type> combineModules(GenerationInformation const & generationInfo, bool synchronizing, ModuleDecisionDiagram<Type> moduleDd1, ModuleDecisionDiagram<Type> moduleDd2, storm::dd::Dd<Type> const& identityDd1, storm::dd::Dd<Type> const& identityDd2);
+//
+// /*!
+// * Combines 2 modules and solves non-determinism (MDP)
+// *
+// * @param module1 First module
+// * @param module1 Second module
+// * @return A module DD representing the combination of both modules
+// */
+// static ModuleDecisionDiagram<Type> combineModulesMDP(GenerationInformation const & generationInfo, ModuleDecisionDiagram<Type> moduleDd1, ModuleDecisionDiagram<Type> moduleDd2);
+//
+// /*!
+// * Creates a system component DD (module)
+// *
+// * @param module Module
+// * @param usedNondetVariablesVector Number of used nondet. variables
+// * @return A system component DD storing all required module information
+// */
+// static SystemComponentDecisionDiagram<Type> createSystemComponentDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const & module, std::vector<uint_fast64_t> usedNondetVariablesVector);
+//
+// /*!
+// * Combines commands (with guards) to a module DD (DTMC)
+// *
+// * @param numberOfCommands Number of commands in the current module
+// * @param commandDds DDs containing all updates for each command
+// * @param guardDds Guard DDs for each command
+// * @return A DD representing the module.
+// */
+// static ModuleDecisionDiagram<Type> combineCommandsDTMC(std::shared_ptr<storm::dd::DdManager<Type>> const & manager, uint_fast64_t numberOfCommands, std::vector<storm::dd::Dd<Type>> const& commandDds, std::vector<storm::dd::Dd<Type>> const& guardDds);
+//
+// /*!
+// * Combines commands (with guards) to a module DD (MDP)
+// *
+// * @param numberOfCommands Number of commands in the current module
+// * @param commandDds DDs containing all updates for each command
+// * @param guardDds Guard DDs for each command
+// * @param usedNondetVariables Number of used nondet. variables
+// * @return A DD representing the module.
+// */
+// static ModuleDecisionDiagram<Type> combineCommandsMDP(std::shared_ptr<storm::dd::DdManager<Type>> const & manager, uint_fast64_t numberOfCommands, std::vector<storm::dd::Dd<Type>> const& commandDds, std::vector<storm::dd::Dd<Type>> const& guardDds, uint_fast64_t usedNondetVariables);
+//
+// /*!
+// * Creates a module DD
+// *
+// * @param module Module
+// * @param synchronizingAction Name of the synchronizing action ("" = no synchronization)
+// * @param usedNondetVariables Number of used nondet. variables
+// * @return A DD representing the module (with/without synchronized actions).
+// */
+// static ModuleDecisionDiagram<Type> createModuleDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, std::string const& synchronizingAction, uint_fast64_t usedNondetVariables);
+//
+// /*!
+// * Creates a command DD
+// *
+// * @param module Current module
+// * @param guard Command guard
+// * @param update Command expression
+// * @return A DD representing the command.
+// */
+// static storm::dd::Dd<Type> createCommandDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd<Type> const& guard, storm::prism::Command const& command);
+//
+// /*!
+// * Creates an update DD
+// *
+// * @param module Current module
+// * @param guard Command guard
+// * @param update Update expression
+// * @return A DD representing the update.
+// */
+// static storm::dd::Dd<Type> createUpdateDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd<Type> const& guard, storm::prism::Update const& update);
+//
+// /*!
+// * Creates initial state DD
+// *
+// * @return A DD representing the initial state.
+// */
+// static storm::dd::Dd<Type> getInitialStateDecisionDiagram(GenerationInformation const & generationInfo);
+//
+// /*!
+// * Calculates the reachable states of the given transition matrix
+// *
+// * @param systemDd The transition matrix DD
+// * @param initialStateDd All initial states
+// * @return A DD representing all reachable states
+// */
+// static storm::dd::Dd<Type> performReachability(GenerationInformation & generationInfo, storm::dd::Dd<Type> const& systemDd, storm::dd::Dd<Type> const& initialStateDd);
+//
+// /*!
+// * Adds a self-loop to deadlock states
+// *
+// * @param systemDd The given DD
+// * @param reachableStatesDd DD representing all reachable states
+// * @return A DD with fixed deadlocks.
+// */
+// static storm::dd::Dd<Type> findDeadlocks(GenerationInformation const & generationInfo, storm::dd::Dd<Type> systemDd, storm::dd::Dd<Type> const& reachableStatesDd);
+//
+// /*!
+// * Computes state and transition rewards
+// *
+// * @param systemDds System DDs
+// */
+// static std::pair<std::vector<storm::dd::Dd<Type>>, std::vector<storm::dd::Dd<Type>>> computeRewards(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram<Type> const& systemDds);
+ };
+
+ } // namespace adapters
+} // namespace storm
+
+#endif /* STORM_BUILDER_DDPRISMMODELBUILDER_H_ */
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 5ac83af33..974d9d306 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -7,6 +7,7 @@
#include "src/models/Mdp.h"
#include "src/models/Ctmdp.h"
+#include "src/utility/prism.h"
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
@@ -54,13 +55,11 @@ namespace storm {
// Intentionally left empty.
}
-
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildRewards(false), rewardModelName(), constantDefinitions() {
// Intentionally left empty.
}
-
-
+
template <typename ValueType, typename IndexType>
ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildRewards(formula.containsRewardOperator()), rewardModelName(), constantDefinitions(), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
// Extract all the labels used in the formula.
diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index 6e474bebf..25c99ced1 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -12,7 +12,7 @@
namespace storm {
namespace dd {
- Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariables(containedMetaVariables) {
+ Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariables(containedMetaVariables) {
// Intentionally left empty.
}
@@ -808,7 +808,7 @@ namespace storm {
this->getContainedMetaVariables().erase(metaVariable);
}
- std::shared_ptr<DdManager<DdType::CUDD>> Dd<DdType::CUDD>::getDdManager() const {
+ std::shared_ptr<DdManager<DdType::CUDD> const> Dd<DdType::CUDD>::getDdManager() const {
return this->ddManager;
}
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 2a56b96a5..0fa04f574 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -563,7 +563,7 @@ namespace storm {
*
* A pointer to the manager that is responsible for this DD.
*/
- std::shared_ptr<DdManager<DdType::CUDD>> getDdManager() const;
+ std::shared_ptr<DdManager<DdType::CUDD> const> getDdManager() const;
/*!
* Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
@@ -604,6 +604,7 @@ namespace storm {
storm::expressions::Expression getMintermExpression() const;
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.
@@ -659,7 +660,7 @@ namespace storm {
* @param cuddAdd The CUDD ADD to store.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
- Dd(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+ Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
/*!
* Helper function to convert the DD into a (sparse) matrix.
@@ -723,7 +724,7 @@ namespace storm {
std::vector<uint_fast64_t> getSortedVariableIndices() const;
// A pointer to the manager responsible for this DD.
- std::shared_ptr<DdManager<DdType::CUDD>> ddManager;
+ std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
// The ADD created by CUDD.
ADD cuddAdd;
diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp
index b37ba1a11..74f29d174 100644
--- a/src/storage/dd/CuddDdForwardIterator.cpp
+++ b/src/storage/dd/CuddDdForwardIterator.cpp
@@ -9,7 +9,7 @@ namespace storm {
// Intentionally left empty.
}
- DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) {
+ DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) {
// If the given generator is not yet at its end, we need to create the current valuation from the cube from
// scratch.
if (!this->isAtEnd) {
diff --git a/src/storage/dd/CuddDdForwardIterator.h b/src/storage/dd/CuddDdForwardIterator.h
index aad7db67c..4c7e97364 100644
--- a/src/storage/dd/CuddDdForwardIterator.h
+++ b/src/storage/dd/CuddDdForwardIterator.h
@@ -85,7 +85,7 @@ namespace storm {
* @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
* if a meta variable does not at all influence the the function value.
*/
- DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true);
+ DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true);
/*!
* Recreates the internal information when a new cube needs to be treated.
@@ -98,7 +98,7 @@ namespace storm {
void treatNextInCube();
// The manager responsible for the meta variables (and therefore the underlying DD).
- std::shared_ptr<DdManager<DdType::CUDD>> ddManager;
+ std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
// The CUDD generator used to enumerate the cubes of the DD.
DdGen* generator;
diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp
index 32a25ae3e..933b95af6 100644
--- a/src/storage/dd/CuddDdManager.cpp
+++ b/src/storage/dd/CuddDdManager.cpp
@@ -37,19 +37,19 @@ namespace storm {
}
}
- Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne() {
+ Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne() const {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addOne());
}
- Dd<DdType::CUDD> DdManager<DdType::CUDD>::getZero() {
+ Dd<DdType::CUDD> DdManager<DdType::CUDD>::getZero() const {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addZero());
}
- Dd<DdType::CUDD> DdManager<DdType::CUDD>::getConstant(double value) {
+ Dd<DdType::CUDD> DdManager<DdType::CUDD>::getConstant(double value) const {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.constant(value));
}
- Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) {
+ Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const {
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'.");
@@ -77,7 +77,7 @@ namespace storm {
return result;
}
- Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(storm::expressions::Variable const& variable) {
+ Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(storm::expressions::Variable const& variable) const {
storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
Dd<DdType::CUDD> result = this->getZero();
@@ -88,7 +88,7 @@ namespace storm {
return result;
}
- Dd<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(storm::expressions::Variable const& variable) {
+ Dd<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(storm::expressions::Variable const& variable) const {
storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
Dd<DdType::CUDD> result = this->getZero();
diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h
index 8ff263ed2..5aff80682 100644
--- a/src/storage/dd/CuddDdManager.h
+++ b/src/storage/dd/CuddDdManager.h
@@ -40,21 +40,21 @@ namespace storm {
*
* @return A DD representing the constant one function.
*/
- Dd<DdType::CUDD> getOne();
+ Dd<DdType::CUDD> getOne() const;
/*!
* Retrieves a DD representing the constant zero function.
*
* @return A DD representing the constant zero function.
*/
- Dd<DdType::CUDD> getZero();
+ Dd<DdType::CUDD> getZero() const;
/*!
* Retrieves a DD representing the constant function with the given value.
*
* @return A DD representing the constant function with the given value.
*/
- Dd<DdType::CUDD> getConstant(double value);
+ Dd<DdType::CUDD> getConstant(double value) const;
/*!
* Retrieves the DD representing the function that maps all inputs which have the given meta variable equal
@@ -65,7 +65,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<DdType::CUDD> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value);
+ Dd<DdType::CUDD> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const;
/*!
* Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values
@@ -74,7 +74,7 @@ namespace storm {
* @param variable The expression variable associated with the meta variable.
* @return The range of the meta variable.
*/
- Dd<DdType::CUDD> getRange(storm::expressions::Variable const& variable);
+ Dd<DdType::CUDD> getRange(storm::expressions::Variable const& variable) const;
/*!
* Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal
@@ -83,7 +83,7 @@ namespace storm {
* @param variable The expression variable associated with the meta variable.
* @return The identity of the meta variable.
*/
- Dd<DdType::CUDD> getIdentity(storm::expressions::Variable const& variable);
+ Dd<DdType::CUDD> getIdentity(storm::expressions::Variable const& variable) const;
/*!
* Adds an integer meta variable with the given range.
diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp
index dc84d9fd7..bd06a8648 100644
--- a/src/storage/dd/CuddOdd.cpp
+++ b/src/storage/dd/CuddOdd.cpp
@@ -8,7 +8,7 @@
namespace storm {
namespace dd {
Odd<DdType::CUDD>::Odd(Dd<DdType::CUDD> const& dd) {
- std::shared_ptr<DdManager<DdType::CUDD>> manager = dd.getDdManager();
+ std::shared_ptr<DdManager<DdType::CUDD> const> manager = dd.getDdManager();
// First, we need to determine the involved DD variables indices.
std::vector<uint_fast64_t> ddVariableIndices = dd.getSortedVariableIndices();
diff --git a/src/utility/math.h b/src/utility/math.h
new file mode 100644
index 000000000..9ee653c4e
--- /dev/null
+++ b/src/utility/math.h
@@ -0,0 +1,22 @@
+#ifndef STORM_UTILITY_MATH_H_
+#define STORM_UTILITY_MATH_H_
+
+#include <cmath>
+
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+ namespace math {
+ // We provide this method explicitly, because MSVC does not offer it (non-C99 compliant).
+ template<typename ValueType>
+ static inline double log2(ValueType number) {
+# ifndef WINDOWS
+ return std::log2(number);
+# else
+ return std::log(number) / std::log(2);
+# endif
+ }
+ }
+}
+
+#endif /* STORM_UTILITY_MATH_H_ */
\ No newline at end of file
diff --git a/src/utility/PrismUtility.h b/src/utility/prism.h
similarity index 99%
rename from src/utility/PrismUtility.h
rename to src/utility/prism.h
index 7d76dd5f4..f88188fb5 100644
--- a/src/utility/PrismUtility.h
+++ b/src/utility/prism.h
@@ -1,5 +1,5 @@
-#ifndef STORM_UTILITY_PRISMUTILITY
-#define STORM_UTILITY_PRISMUTILITY
+#ifndef STORM_UTILITY_PRISM_H_
+#define STORM_UTILITY_PRISM_H_
#include <memory>
#include <boost/algorithm/string.hpp>
@@ -236,4 +236,4 @@ namespace storm {
} // namespace utility
} // namespace storm
-#endif /* STORM_UTILITY_PRISMUTILITY_H_ */
+#endif /* STORM_UTILITY_PRISM_H_ */