diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index ab9fe02d9..ee79488ac 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -4,61 +4,60 @@ #include "src/exceptions/ExpressionEvaluationException.h" #include "src/exceptions/InvalidArgumentException.h" -#include "src/storage/dd/cudd/CuddDdManager.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" - +#include "src/storage/dd/DdManager.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" namespace storm { namespace adapters { - template - AddExpressionAdapter::AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { + template + AddExpressionAdapter::AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { // Intentionally left empty. } - template - storm::dd::Add AddExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { + template + storm::dd::Add AddExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { return boost::any_cast>(expression.accept(*this)); } - template - boost::any AddExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { storm::dd::Add elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); storm::dd::Add thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); storm::dd::Add conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); return conditionDd.ite(thenDd, elseDd); } - template - boost::any AddExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { storm::dd::Bdd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)).toBdd(); storm::dd::Bdd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)).toBdd(); - storm::dd::Add result; + storm::dd::Add result; switch (expression.getOperatorType()) { case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: - result = (leftResult && rightResult).toAdd(); + result = (leftResult && rightResult).template toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: - result = (leftResult || rightResult).toAdd(); + result = (leftResult || rightResult).template toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: - result = (leftResult.iff(rightResult)).toAdd(); + result = (leftResult.iff(rightResult)).template toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: - result = (!leftResult || rightResult).toAdd(); + result = (!leftResult || rightResult).template toAdd(); break; case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: - result = (leftResult.exclusiveOr(rightResult)).toAdd(); + result = (leftResult.exclusiveOr(rightResult)).template toAdd(); break; } return result; } - template - boost::any AddExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); @@ -92,8 +91,8 @@ namespace storm { return result; } - template - boost::any AddExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); @@ -122,15 +121,15 @@ namespace storm { return result; } - template - boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { + template + boost::any AddExpressionAdapter::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 the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); - return ddManager->getIdentity(variablePair->second); + return ddManager->template getIdentity(variablePair->second); } - template - boost::any AddExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { storm::dd::Bdd result = boost::any_cast>(expression.getOperand()->accept(*this)).toBdd(); switch (expression.getOperatorType()) { @@ -139,11 +138,11 @@ namespace storm { break; } - return result.toAdd(); + return result.template toAdd(); } - template - boost::any AddExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { storm::dd::Add result = boost::any_cast>(expression.getOperand()->accept(*this)); switch (expression.getOperatorType()) { @@ -163,23 +162,23 @@ namespace storm { return result; } - template - boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { return ddManager->getConstant(expression.getValue()); } - template - boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { return ddManager->getConstant(expression.getValue()); } - template - boost::any AddExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { + template + boost::any AddExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { return ddManager->getConstant(expression.getValue()); } // Explicitly instantiate the symbolic expression adapter - template class AddExpressionAdapter; + template class AddExpressionAdapter; } // namespace adapters } // namespace storm diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h index 8225556f1..a8a8d43c6 100644 --- a/src/adapters/AddExpressionAdapter.h +++ b/src/adapters/AddExpressionAdapter.h @@ -11,7 +11,7 @@ namespace storm { namespace adapters { - template + template class AddExpressionAdapter : public storm::expressions::ExpressionVisitor { public: AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping); diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 3b421408b..c5ed1c1af 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -7,18 +7,18 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" namespace storm { namespace modelchecker { template - HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory()) { + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory()) { // Intentionally left empty. } template - HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + HybridCtmcCslModelChecker::HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } @@ -46,8 +46,8 @@ namespace storm { } template - storm::models::symbolic::Ctmc const& HybridCtmcCslModelChecker::getModel() const { - return this->template getModelAs>(); + storm::models::symbolic::Ctmc const& HybridCtmcCslModelChecker::getModel() const { + return this->template getModelAs>(); } template diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index c447909b2..cfdd5326b 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -11,10 +11,10 @@ namespace storm { namespace modelchecker { template - class HybridCtmcCslModelChecker : public SymbolicPropositionalModelChecker { + class HybridCtmcCslModelChecker : public SymbolicPropositionalModelChecker { public: - explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model); - explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model); + explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; @@ -27,7 +27,7 @@ namespace storm { virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: - storm::models::symbolic::Ctmc const& getModel() const override; + storm::models::symbolic::Ctmc const& getModel() const override; private: // An object that is used for solving linear equations and performing matrix-vector multiplication. diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index 133a120a1..5202cbec2 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -3,9 +3,9 @@ #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h" #include "src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h" -#include "src/storage/dd/cudd/CuddDdManager.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" +#include "src/storage/dd/DdManager.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" #include "src/storage/dd/cudd/CuddOdd.h" #include "src/utility/macros.h" @@ -27,23 +27,23 @@ namespace storm { namespace helper { template - std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return HybridDtmcPrctlHelper::computeReachabilityRewards(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative, linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates) { + std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates) { return HybridDtmcPrctlHelper::computeNextProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), nextStates); } template - std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return HybridDtmcPrctlHelper::computeUntilProbabilities(model, computeProbabilityMatrix(model, rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If the time bounds are [0, inf], we rather call untimed reachability. if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { @@ -74,10 +74,10 @@ namespace storm { STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); // Compute the vector that is to be added as a compensation for removing the absorbing states. - storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); // Create an ODD for the translation to an explicit representation. storm::dd::Odd odd(statesWithProbabilityGreater0NonPsi); @@ -122,7 +122,7 @@ namespace storm { ValueType uniformizationRate = 1.02 * (relevantStates.toAdd() * exitRateVector).getMax(); // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, relevantStates, uniformizationRate); storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); // Compute the transient probabilities. @@ -140,10 +140,10 @@ namespace storm { STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); // Compute the (first) uniformized matrix. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0NonPsi, uniformizationRate); // Create the one-step vector. - storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); + storm::dd::Add b = (statesWithProbabilityGreater0NonPsi.toAdd() * rateMatrix * psiStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(model.getColumnVariables()) / model.getManager().getConstant(uniformizationRate); // Build an ODD for the relevant states and translate the symbolic parts to their explicit representation. storm::dd::Odd odd = storm::dd::Odd(statesWithProbabilityGreater0NonPsi); @@ -204,7 +204,7 @@ namespace storm { STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); // Finally, we compute the second set of transient probabilities. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate); + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, statesWithProbabilityGreater0, uniformizationRate); storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); newSubresult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, linearEquationSolverFactory); @@ -219,7 +219,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -235,7 +235,7 @@ namespace storm { ValueType uniformizationRate = 1.02 * exitRateVector.getMax(); STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, result, linearEquationSolverFactory); @@ -245,7 +245,7 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -264,11 +264,11 @@ namespace storm { storm::dd::Odd odd(model.getReachableStates()); // Compute the uniformized matrix. - storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); + storm::dd::Add uniformizedMatrix = computeUniformizedMatrix(model, rateMatrix, exitRateVector, model.getReachableStates(), uniformizationRate); storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); // Then compute the state reward vector to use in the computation. - storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector); + storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector); std::vector explicitTotalRewardVector = totalRewardVector.template toVector(odd); // Finally, compute the transient probabilities. @@ -277,8 +277,8 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslHelper::computeLongRunAverage(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - storm::dd::Add probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector); + std::unique_ptr HybridCtmcCslHelper::computeLongRunAverage(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add probabilityMatrix = computeProbabilityMatrix(model, rateMatrix, exitRateVector); // Create ODD for the translation. storm::dd::Odd odd(model.getReachableStates()); @@ -291,17 +291,17 @@ namespace storm { } template - storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { + storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); STORM_LOG_DEBUG("Keeping " << maybeStates.getNonZeroCount() << " rows."); // Cut all non-maybe rows/columns from the transition matrix. - storm::dd::Add uniformizedMatrix = transitionMatrix * maybeStates.toAdd() * maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); + storm::dd::Add uniformizedMatrix = transitionMatrix * maybeStates.toAdd() * maybeStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); // Now perform the uniformization. uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate); - storm::dd::Add diagonal = model.getRowColumnIdentity() * maybeStates.toAdd(); - storm::dd::Add diagonalOffset = diagonal; + storm::dd::Add diagonal = model.getRowColumnIdentity() * maybeStates.toAdd(); + storm::dd::Add diagonalOffset = diagonal; diagonalOffset -= diagonal * (exitRateVector / model.getManager().getConstant(uniformizationRate)); uniformizedMatrix += diagonalOffset; @@ -309,7 +309,7 @@ namespace storm { } template - storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { + storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { return rateMatrix / exitRateVector; } diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h index 2581c644b..ea2d74638 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -16,21 +16,21 @@ namespace storm { template class HybridCtmcCslHelper { public: - typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; + typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeLongRunAverage(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeLongRunAverage(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); + static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); /*! * Converts the given rate-matrix into a time-abstract probability matrix. @@ -40,7 +40,7 @@ namespace storm { * @param exitRateVector The exit rate vector of the model. * @return The probability matrix. */ - static storm::dd::Add computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + static storm::dd::Add computeProbabilityMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); /*! * Computes the matrix representing the transitions of the uniformized CTMC. @@ -52,7 +52,7 @@ namespace storm { * @param uniformizationRate The rate to be used for uniformization. * @return The uniformized matrix. */ - static storm::dd::Add computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate); + static storm::dd::Add computeUniformizedMatrix(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate); }; } diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 18db55a52..f16be8cd1 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -4,7 +4,7 @@ #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "src/storage/dd/cudd/CuddOdd.h" -#include "src/storage/dd/cudd/CuddDdManager.h" +#include "src/storage/dd/DdManager.h" #include "src/utility/macros.h" #include "src/utility/graph.h" diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 5ccb82bcd..af7329978 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -11,7 +11,7 @@ namespace storm { namespace modelchecker { template - class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { + class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker { public: explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model); explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); @@ -27,7 +27,7 @@ namespace storm { virtual std::unique_ptr computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; protected: - storm::models::symbolic::Dtmc const& getModel() const override; + storm::models::symbolic::Dtmc const& getModel() const override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h index 03b863d6c..539fbff8d 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h @@ -8,17 +8,17 @@ namespace storm { namespace models { namespace symbolic { - template class Model; + template + class Model; } } namespace modelchecker { - - template + template class SymbolicPropositionalModelChecker : public AbstractModelChecker { public: - explicit SymbolicPropositionalModelChecker(storm::models::symbolic::Model const& model); + explicit SymbolicPropositionalModelChecker(storm::models::symbolic::Model const& model); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(storm::logic::Formula const& formula) const override; @@ -32,7 +32,7 @@ namespace storm { * * @return The model associated with this model checker instance. */ - virtual storm::models::symbolic::Model const& getModel() const; + virtual storm::models::symbolic::Model const& getModel() const; /*! * Retrieves the model associated with this model checker instance as the given template parameter type. @@ -44,8 +44,9 @@ namespace storm { private: // The model that is to be analyzed by the model checker. - storm::models::symbolic::Model const& model; + storm::models::symbolic::Model const& model; }; + } } diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h index 1de7a33c5..152fc9e3b 100644 --- a/src/modelchecker/results/CheckResult.h +++ b/src/modelchecker/results/CheckResult.h @@ -13,10 +13,18 @@ namespace storm { class QualitativeCheckResult; class QuantitativeCheckResult; class ExplicitQualitativeCheckResult; - template class ExplicitQuantitativeCheckResult; - template class SymbolicQualitativeCheckResult; - template class SymbolicQuantitativeCheckResult; - template class HybridQuantitativeCheckResult; + + template + class ExplicitQuantitativeCheckResult; + + template + class SymbolicQualitativeCheckResult; + + template + class SymbolicQuantitativeCheckResult; + + template + class HybridQuantitativeCheckResult; // The base class of all check results. class CheckResult { @@ -65,17 +73,17 @@ namespace storm { template SymbolicQualitativeCheckResult const& asSymbolicQualitativeCheckResult() const; - template - SymbolicQuantitativeCheckResult& asSymbolicQuantitativeCheckResult(); + template + SymbolicQuantitativeCheckResult& asSymbolicQuantitativeCheckResult(); - template - SymbolicQuantitativeCheckResult const& asSymbolicQuantitativeCheckResult() const; + template + SymbolicQuantitativeCheckResult const& asSymbolicQuantitativeCheckResult() const; - template - HybridQuantitativeCheckResult& asHybridQuantitativeCheckResult(); + template + HybridQuantitativeCheckResult& asHybridQuantitativeCheckResult(); - template - HybridQuantitativeCheckResult const& asHybridQuantitativeCheckResult() const; + template + HybridQuantitativeCheckResult const& asHybridQuantitativeCheckResult() const; virtual std::ostream& writeToStream(std::ostream& out) const = 0; }; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 8543d4008..53527d499 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -2,15 +2,15 @@ #define STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ #include "src/storage/dd/DdType.h" -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" #include "src/storage/dd/cudd/CuddOdd.h" #include "src/modelchecker/results/QuantitativeCheckResult.h" #include "src/utility/OsDetection.h" namespace storm { namespace modelchecker { - template + template class HybridQuantitativeCheckResult : public QuantitativeCheckResult { public: HybridQuantitativeCheckResult() = default; @@ -34,21 +34,21 @@ namespace storm { storm::dd::Bdd const& getSymbolicStates() const; - storm::dd::Add const& getSymbolicValueVector() const; + storm::dd::Add const& getSymbolicValueVector() const; storm::dd::Bdd const& getExplicitStates() const; storm::dd::Odd const& getOdd() const; - std::vector const& getExplicitValueVector() const; + std::vector const& getExplicitValueVector() const; virtual std::ostream& writeToStream(std::ostream& out) const override; virtual void filter(QualitativeCheckResult const& filter) override; - virtual double getMin() const; + virtual ValueType getMin() const; - virtual double getMax() const; + virtual ValueType getMax() const; private: // The set of all reachable states. @@ -58,7 +58,7 @@ namespace storm { storm::dd::Bdd symbolicStates; // The symbolic value vector. - storm::dd::Add symbolicValues; + storm::dd::Add symbolicValues; // The set of all states whose result is stored explicitly. storm::dd::Bdd explicitStates; @@ -67,7 +67,7 @@ namespace storm { storm::dd::Odd odd; // The explicit value vector. - std::vector explicitValues; + std::vector explicitValues; }; } } diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 3201f8f5e..3e94f5ee8 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -2,7 +2,7 @@ #define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ #include "src/storage/dd/DdType.h" -#include "src/storage/dd/cudd/CuddBdd.h" +#include "src/storage/dd/Bdd.h" #include "src/modelchecker/results/QualitativeCheckResult.h" #include "src/utility/OsDetection.h" diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index fb970dc7c..d513e6782 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -2,13 +2,13 @@ #define STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_ #include "src/storage/dd/DdType.h" -#include "src/storage/dd/cudd/CuddAdd.h" +#include "src/storage/dd/Add.h" #include "src/modelchecker/results/QuantitativeCheckResult.h" #include "src/utility/OsDetection.h" namespace storm { namespace modelchecker { - template + template class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult { public: SymbolicQuantitativeCheckResult() = default; @@ -28,15 +28,15 @@ namespace storm { virtual bool isSymbolicQuantitativeCheckResult() const override; - storm::dd::Add const& getValueVector() const; + storm::dd::Add const& getValueVector() const; virtual std::ostream& writeToStream(std::ostream& out) const override; virtual void filter(QualitativeCheckResult const& filter) override; - virtual double getMin() const; + virtual ValueType getMin() const; - virtual double getMax() const; + virtual ValueType getMax() const; private: // The set of all reachable states. @@ -46,7 +46,7 @@ namespace storm { storm::dd::Bdd states; // The values of the quantitative check result. - storm::dd::Add values; + storm::dd::Add values; }; } } diff --git a/src/models/symbolic/Ctmc.h b/src/models/symbolic/Ctmc.h index 26736fed2..79e116ca8 100644 --- a/src/models/symbolic/Ctmc.h +++ b/src/models/symbolic/Ctmc.h @@ -11,17 +11,17 @@ namespace storm { /*! * This class represents a continuous-time Markov chain. */ - template - class Ctmc : public DeterministicModel { + template + class Ctmc : public DeterministicModel { public: - typedef typename DeterministicModel::RewardModelType RewardModelType; + typedef typename DeterministicModel::RewardModelType RewardModelType; - Ctmc(Ctmc const& other) = default; - Ctmc& operator=(Ctmc const& other) = default; + Ctmc(Ctmc const& other) = default; + Ctmc& operator=(Ctmc const& other) = default; #ifndef WINDOWS - Ctmc(Ctmc&& other) = default; - Ctmc& operator=(Ctmc&& other) = default; + Ctmc(Ctmc&& other) = default; + Ctmc& operator=(Ctmc&& other) = default; #endif /*! @@ -44,11 +44,11 @@ namespace storm { Ctmc(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, - storm::dd::Add transitionMatrix, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); @@ -58,10 +58,10 @@ namespace storm { * * @return The exit rate vector. */ - storm::dd::Add const& getExitRateVector() const; + storm::dd::Add const& getExitRateVector() const; private: - storm::dd::Add exitRates; + storm::dd::Add exitRates; }; } // namespace symbolic diff --git a/src/models/symbolic/DeterministicModel.h b/src/models/symbolic/DeterministicModel.h index 2e025c549..6fab1b8db 100644 --- a/src/models/symbolic/DeterministicModel.h +++ b/src/models/symbolic/DeterministicModel.h @@ -11,17 +11,17 @@ namespace storm { /*! * Base class for all deterministic symbolic models. */ - template - class DeterministicModel : public Model { + template + class DeterministicModel : public Model { public: - typedef typename Model::RewardModelType RewardModelType; + typedef typename Model::RewardModelType RewardModelType; - DeterministicModel(DeterministicModel const& other) = default; - DeterministicModel& operator=(DeterministicModel const& other) = default; + DeterministicModel(DeterministicModel const& other) = default; + DeterministicModel& operator=(DeterministicModel const& other) = default; #ifndef WINDOWS - DeterministicModel(DeterministicModel&& other) = default; - DeterministicModel& operator=(DeterministicModel&& other) = default; + DeterministicModel(DeterministicModel&& other) = default; + DeterministicModel& operator=(DeterministicModel&& other) = default; #endif /*! @@ -46,11 +46,11 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, - storm::dd::Add transitionMatrix, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); diff --git a/src/models/symbolic/Dtmc.h b/src/models/symbolic/Dtmc.h index b5cc4a50d..91ba3be07 100644 --- a/src/models/symbolic/Dtmc.h +++ b/src/models/symbolic/Dtmc.h @@ -11,17 +11,17 @@ namespace storm { /*! * This class represents a discrete-time Markov chain. */ - template - class Dtmc : public DeterministicModel { + template + class Dtmc : public DeterministicModel { public: - typedef typename DeterministicModel::RewardModelType RewardModelType; + typedef typename DeterministicModel::RewardModelType RewardModelType; - Dtmc(Dtmc const& other) = default; - Dtmc& operator=(Dtmc const& other) = default; + Dtmc(Dtmc const& other) = default; + Dtmc& operator=(Dtmc const& other) = default; #ifndef WINDOWS - Dtmc(Dtmc&& other) = default; - Dtmc& operator=(Dtmc&& other) = default; + Dtmc(Dtmc&& other) = default; + Dtmc& operator=(Dtmc&& other) = default; #endif /*! @@ -44,11 +44,11 @@ namespace storm { Dtmc(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, - storm::dd::Add transitionMatrix, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); diff --git a/src/models/symbolic/Mdp.h b/src/models/symbolic/Mdp.h index 357016400..56be6ad67 100644 --- a/src/models/symbolic/Mdp.h +++ b/src/models/symbolic/Mdp.h @@ -11,17 +11,17 @@ namespace storm { /*! * This class represents a discrete-time Markov decision process. */ - template - class Mdp : public NondeterministicModel { + template + class Mdp : public NondeterministicModel { public: - typedef typename NondeterministicModel::RewardModelType RewardModelType; + typedef typename NondeterministicModel::RewardModelType RewardModelType; - Mdp(Mdp const& other) = default; - Mdp& operator=(Mdp const& other) = default; + Mdp(Mdp const& other) = default; + Mdp& operator=(Mdp const& other) = default; #ifndef WINDOWS - Mdp(Mdp&& other) = default; - Mdp& operator=(Mdp&& other) = default; + Mdp(Mdp&& other) = default; + Mdp& operator=(Mdp&& other) = default; #endif /*! @@ -46,11 +46,11 @@ namespace storm { Mdp(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, - storm::dd::Add transitionMatrix, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::set const& nondeterminismVariables, std::map labelToExpressionMap = std::map(), diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 4dc6ff31e..9115f3a25 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -15,15 +15,23 @@ namespace storm { namespace dd { - template class Dd; - template class Add; - template class Bdd; - template class DdManager; + template + class Dd; + + template + class Add; + + template + class Bdd; + + template + class DdManager; } namespace adapters { - template class AddExpressionAdapter; + template + class AddExpressionAdapter; } namespace models { @@ -35,11 +43,11 @@ namespace storm { /*! * Base class for all symbolic models. */ - template + template class Model : public storm::models::ModelBase { public: static const storm::dd::DdType DdType = Type; - typedef StandardRewardModel RewardModelType; + typedef StandardRewardModel RewardModelType; Model(Model const& other) = default; Model& operator=(Model const& other) = default; @@ -71,11 +79,11 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, - storm::dd::Add transitionMatrix, + storm::dd::Add transitionMatrix, std::set const& rowVariables, - std::shared_ptr> rowExpressionAdapter, + std::shared_ptr> rowExpressionAdapter, std::set const& columnVariables, - std::shared_ptr> columnExpressionAdapter, + std::shared_ptr> columnExpressionAdapter, std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap = std::map(), std::unordered_map const& rewardModels = std::unordered_map()); @@ -141,14 +149,14 @@ namespace storm { * * @return A matrix representing the transitions of the model. */ - storm::dd::Add const& getTransitionMatrix() const; + storm::dd::Add const& getTransitionMatrix() const; /*! * Retrieves the matrix representing the transitions of the model. * * @return A matrix representing the transitions of the model. */ - storm::dd::Add& getTransitionMatrix(); + storm::dd::Add& getTransitionMatrix(); /*! * Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices. @@ -176,7 +184,7 @@ namespace storm { * * @return An ADD that represents the diagonal of the transition matrix. */ - storm::dd::Add getRowColumnIdentity() const; + storm::dd::Add getRowColumnIdentity() const; /*! * Retrieves whether the model has a reward model with the given name. @@ -233,7 +241,7 @@ namespace storm { * * @param transitionMatrix The new transition matrix of the model. */ - void setTransitionMatrix(storm::dd::Add const& transitionMatrix); + void setTransitionMatrix(storm::dd::Add const& transitionMatrix); /*! * Retrieves the mapping of labels to their defining expressions. @@ -282,19 +290,19 @@ namespace storm { storm::dd::Bdd initialStates; // A matrix representing transition relation. - storm::dd::Add transitionMatrix; + storm::dd::Add transitionMatrix; // The meta variables used to encode the rows of the transition matrix. std::set rowVariables; // An adapter that can translate expressions to DDs over the row meta variables. - std::shared_ptr> rowExpressionAdapter; + std::shared_ptr> rowExpressionAdapter; // The meta variables used to encode the columns of the transition matrix. std::set columnVariables; // An adapter that can translate expressions to DDs over the column meta variables. - std::shared_ptr> columnExpressionAdapter; + std::shared_ptr> columnExpressionAdapter; // A vector holding all pairs of row and column meta variable pairs. This is used to swap the variables // in the DDs from row to column variables and vice versa. diff --git a/src/models/symbolic/StandardRewardModel.h b/src/models/symbolic/StandardRewardModel.h index 1eb1048d8..35afd71b0 100644 --- a/src/models/symbolic/StandardRewardModel.h +++ b/src/models/symbolic/StandardRewardModel.h @@ -9,7 +9,7 @@ namespace storm { namespace dd { - template + template class Add; template @@ -33,7 +33,7 @@ namespace storm { * @param stateActionRewardVector The vector of state-action rewards. * @param transitionRewardMatrix The matrix of transition rewards. */ - explicit StandardRewardModel(boost::optional> const& stateRewardVector, boost::optional> const& stateActionRewardVector, boost::optional> const& transitionRewardMatrix); + explicit StandardRewardModel(boost::optional> const& stateRewardVector, boost::optional> const& stateActionRewardVector, boost::optional> const& transitionRewardMatrix); /*! * Retrieves whether the reward model is empty. @@ -62,7 +62,7 @@ namespace storm { * * @return The state reward vector. */ - storm::dd::Add const& getStateRewardVector() const; + storm::dd::Add const& getStateRewardVector() const; /*! * Retrieves the state rewards of the reward model. Note that it is illegal to call this function if the @@ -70,14 +70,14 @@ namespace storm { * * @return The state reward vector. */ - storm::dd::Add& getStateRewardVector(); + storm::dd::Add& getStateRewardVector(); /*! * Retrieves an optional value that contains the state reward vector if there is one. * * @return The state reward vector if there is one. */ - boost::optional> const& getOptionalStateRewardVector() const; + boost::optional> const& getOptionalStateRewardVector() const; /*! * Retrieves whether the reward model has state-action rewards. @@ -92,7 +92,7 @@ namespace storm { * * @return The state-action reward vector. */ - storm::dd::Add const& getStateActionRewardVector() const; + storm::dd::Add const& getStateActionRewardVector() const; /*! * Retrieves the state-action rewards of the reward model. Note that it is illegal to call this function @@ -100,14 +100,14 @@ namespace storm { * * @return The state-action reward vector. */ - storm::dd::Add& getStateActionRewardVector(); + storm::dd::Add& getStateActionRewardVector(); /*! * Retrieves an optional value that contains the state-action reward vector if there is one. * * @return The state-action reward vector if there is one. */ - boost::optional> const& getOptionalStateActionRewardVector() const; + boost::optional> const& getOptionalStateActionRewardVector() const; /*! * Retrieves whether the reward model has transition rewards. @@ -122,7 +122,7 @@ namespace storm { * * @return The transition reward matrix. */ - storm::dd::Add const& getTransitionRewardMatrix() const; + storm::dd::Add const& getTransitionRewardMatrix() const; /*! * Retrieves the transition rewards of the reward model. Note that it is illegal to call this function @@ -130,14 +130,14 @@ namespace storm { * * @return The transition reward matrix. */ - storm::dd::Add& getTransitionRewardMatrix(); + storm::dd::Add& getTransitionRewardMatrix(); /*! * Retrieves an optional value that contains the transition reward matrix if there is one. * * @return The transition reward matrix if there is one. */ - boost::optional> const& getOptionalTransitionRewardMatrix() const; + boost::optional> const& getOptionalTransitionRewardMatrix() const; /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and @@ -147,7 +147,7 @@ namespace storm { * @param columnVariables The column variables of the model. * @return The full state-action reward vector. */ - storm::dd::Add getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables) const; + storm::dd::Add getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables) const; /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and @@ -159,7 +159,7 @@ namespace storm { * @param columnVariables The column variables of the model. * @return The full state-action reward vector. */ - storm::dd::Add getTotalRewardVector(storm::dd::Add const& filterAdd, storm::dd::Add const& transitionMatrix, std::set const& columnVariables) const; + storm::dd::Add getTotalRewardVector(storm::dd::Add const& filterAdd, storm::dd::Add const& transitionMatrix, std::set const& columnVariables) const; /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and @@ -170,14 +170,14 @@ namespace storm { * @param weights The weights used to scale the state-action reward vector. * @return The full state-action reward vector. */ - storm::dd::Add getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights) const; + storm::dd::Add getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights) const; /*! * Multiplies all components of the reward model with the given DD. * * @param filter The filter with which to multiply */ - StandardRewardModel& operator*=(storm::dd::Add const& filter); + StandardRewardModel& operator*=(storm::dd::Add const& filter); /*! * Divides the state reward vector of the reward model by the given divisor. @@ -185,17 +185,17 @@ namespace storm { * @param divisor The vector to divide by. * @return The resulting reward model. */ - StandardRewardModel divideStateRewardVector(storm::dd::Add const& divisor) const; + StandardRewardModel divideStateRewardVector(storm::dd::Add const& divisor) const; private: // The state reward vector. - boost::optional> optionalStateRewardVector; + boost::optional> optionalStateRewardVector; // A vector of state-action-based rewards. - boost::optional> optionalStateActionRewardVector; + boost::optional> optionalStateActionRewardVector; // A matrix of transition rewards. - boost::optional> optionalTransitionRewardMatrix; + boost::optional> optionalTransitionRewardMatrix; }; } diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 62510a035..fd074b1a1 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -1,8 +1,634 @@ #include "src/storage/dd/Add.h" +#include + +#include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/DdManager.h" + +#include "src/storage/SparseMatrix.h" + +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + namespace storm { namespace dd { + template + Add::Add(std::shared_ptr const> ddManager, InternalAdd const& internalAdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalAdd(internalAdd) { + // Intentionally left empty. + } + + template + bool Add::operator==(Add const& other) const { + return internalAdd == other.internalAdd; + } + + template + bool Add::operator!=(Add const& other) const { + return internalAdd != other.internalAdd; + } + + template + Add Add::ite(Add const& thenAdd, Add const& elseAdd) const { + std::set metaVariables = Dd::joinMetaVariables(thenAdd, elseAdd); + metaVariables.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); + return Add(this->getDdManager(), internalAdd.ite(thenAdd.internalAdd, elseAdd.internalAdd), metaVariables); + } + + template + Add Add::operator!() const { + return Add(this->getDdManager(), !internalAdd, this->getContainedMetaVariables()); + } + + template + Add Add::operator||(Add const& other) const { + return Add(this->getDdManager(), internalAdd || other.internalAdd, Dd::joinMetaVariables(*this, other)); + } + + template + Add& Add::operator|=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + internalAdd |= other.internalAdd; + return *this; + } + + template + Add Add::operator+(Add const& other) const { + return Add(this->getDdManager(), internalAdd + other.internalAdd, Dd::joinMetaVariables(*this, other)); + } + + template + Add& Add::operator+=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + internalAdd += other.internalAdd; + return *this; + } + + template + Add Add::operator*(Add const& other) const { + return Add(this->getDdManager(), internalAdd * other.internalAdd, Dd::joinMetaVariables(*this, other)); + } + + template + Add& Add::operator*=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + internalAdd *= other.internalAdd; + return *this; + } + + template + Add Add::operator-(Add const& other) const { + return Add(this->getDdManager(), internalAdd - other.internalAdd, Dd::joinMetaVariables(*this, other)); + } + + template + Add Add::operator-() const { + return this->getDdManager()->getAddZero() - *this; + } + + template + Add& Add::operator-=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + internalAdd -= other.internalAdd; + return *this; + } + + template + Add Add::operator/(Add const& other) const { + return Add(this->getDdManager(), internalAdd / other.internalAdd, Dd::joinMetaVariables(*this, other)); + } + + template + Add& Add::operator/=(Add const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + internalAdd /= other.internalAdd; + return *this; + } + + template + Add Add::equals(Add const& other) const { + return Add(this->getDdManager(), internalAdd.equals(other), Dd::joinMetaVariables(*this, other)); + } + + template + Add Add::notEquals(Add const& other) const { + return Add(this->getDdManager(), internalAdd.notEquals(other), Dd::joinMetaVariables(*this, other)); + + } + + template + Add Add::less(Add const& other) const { + return Add(this->getDdManager(), internalAdd.less(other), Dd::joinMetaVariables(*this, other)); + } + + template + Add Add::lessOrEqual(Add const& other) const { + return Add(this->getDdManager(), internalAdd.lessOrEqual(other), Dd::joinMetaVariables(*this, other)); + + } + + template + Add Add::greater(Add const& other) const { + return Add(this->getDdManager(), internalAdd.greater(other), Dd::joinMetaVariables(*this, other)); + } + + template + Add Add::greaterOrEqual(Add const& other) const { + return Add(this->getDdManager(), internalAdd.greaterOrEqual(other), Dd::joinMetaVariables(*this, other)); + + } + + template + Add Add::pow(Add const& other) const { + return Add(this->getDdManager(), internalAdd.pow(other), Dd::joinMetaVariables(*this, other)); + } + + template + Add Add::mod(Add const& other) const { + return Add(this->getDdManager(), internalAdd.mod(other), Dd::joinMetaVariables(*this, other)); + + } + + template + Add Add::logxy(Add const& other) const { + return Add(this->getDdManager(), internalAdd.logxy(other), Dd::joinMetaVariables(*this, other)); + + } + + template + Add Add::floor() const { + return Add(this->getDdManager(), internalAdd.floor(), this->getContainedMetaVariables()); + } + + template + Add Add::ceil() const { + return Add(this->getDdManager(), internalAdd.ceil(), this->getContainedMetaVariables()); + } + + template + Add Add::minimum(Add const& other) const { + return Add(this->getDdManager(), internalAdd.minimum(other), Dd::joinMetaVariables(*this, other)); + } + + template + Add Add::maximum(Add const& other) const { + return Add(this->getDdManager(), internalAdd.maximum(other), Dd::joinMetaVariables(*this, other)); + } + + template + Add Add::sumAbstract(std::set const& metaVariables) const { + Bdd cube = this->getCube(metaVariables); + return Add(this->getDdManager(), internalAdd.sumAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + } + + template + Add Add::minAbstract(std::set const& metaVariables) const { + Bdd cube = this->getCube(metaVariables); + return Add(this->getDdManager(), internalAdd.minAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + } + + template + Add Add::maxAbstract(std::set const& metaVariables) const { + Bdd cube = this->getCube(metaVariables); + return Add(this->getDdManager(), internalAdd.maxAbstract(cube), Dd::subtractMetaVariables(*this, cube)); + } + + template + bool Add::equalModuloPrecision(Add const& other, double precision, bool relative) const { + return internalAdd.equalModuloPrecision(other, precision, relative); + } + template + Add Add::swapVariables(std::vector> const& metaVariablePairs) const { + std::set newContainedMetaVariables; + std::vector> from; + std::vector> to; + for (auto const& metaVariablePair : metaVariablePairs) { + DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + + // Keep track of the contained meta variables in the DD. + if (this->containsMetaVariable(metaVariablePair.first)) { + newContainedMetaVariables.insert(metaVariablePair.second); + } + if (this->containsMetaVariable(metaVariablePair.second)) { + newContainedMetaVariables.insert(metaVariablePair.first); + } + + for (auto const& ddVariable : variable1.getDdVariables()) { + from.push_back(ddVariable.toAdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + to.push_back(ddVariable.toAdd()); + } + } + return Bdd(this->getDdManager(), internalAdd.swapVariables(from, to), newContainedMetaVariables); + } + + template + Add Add::multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const { + // Create the CUDD summation variables. + std::vector> summationDdVariables; + for (auto const& metaVariable : summationMetaVariables) { + for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { + summationDdVariables.push_back(ddVariable.toAdd()); + } + } + + std::set unionOfMetaVariables = Dd::joinMetaVariables(*this, otherMatrix); + std::set containedMetaVariables; + std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); + + return Add(this->getDdManager(), internalAdd.multiplyMatrix(otherMatrix, summationDdVariables), containedMetaVariables); + } + + template + Bdd Add::greater(ValueType const& value) const { + return Bdd(this->getDdManager(), internalAdd.greater(value), this->getContainedMetaVariables()); + } + + template + Bdd Add::greaterOrEqual(ValueType const& value) const { + return Bdd(this->getDdManager(), internalAdd.greaterOrEqual(value), this->getContainedMetaVariables()); + } + + template + Bdd Add::less(ValueType const& value) const { + return Bdd(this->getDdManager(), internalAdd.less(value), this->getContainedMetaVariables()); + } + + template + Bdd Add::lessOrEqual(ValueType const& value) const { + return Bdd(this->getDdManager(), internalAdd.lessOrEqual(value), this->getContainedMetaVariables()); + } + + template + Bdd Add::notZero() const { + return this->toBdd(); + } + + template + Add Add::constrain(Add const& constraint) const { + return Add(this->getDdManager(), internalAdd.constrain(constraint), Dd::joinMetaVariables(*this, constraint)); + } + + template + Add Add::restrict(Add const& constraint) const { + return Add(this->getDdManager(), internalAdd.restrict(constraint), Dd::joinMetaVariables(*this, constraint)); + } + + template + Bdd Add::getSupport() const { + return Bdd(this->getDdManager(), internalAdd.getSupport(), this->getContainedMetaVariables()); + } + + template + uint_fast64_t Add::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + } + return internalAdd.getNonZeroCount(numberOfDdVariables); + } + + template + uint_fast64_t Add::getLeafCount() const { + return internalAdd.getLeafCount(); + } + + template + uint_fast64_t Add::getNodeCount() const { + return internalAdd.getNodeCount(); + } + + template + ValueType Add::getMin() const { + return internalAdd.getMin(); + } + + template + ValueType Add::getMax() const { + return internalAdd.getMax(); + } + + template + void Add::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, ValueType const& targetValue) { + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(metaVariable, variableValue); + this->setValue(metaVariableToValueMap, targetValue); + } + + template + void Add::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, ValueType const& targetValue) { + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(metaVariable1, variableValue1); + metaVariableToValueMap.emplace(metaVariable2, variableValue2); + this->setValue(metaVariableToValueMap, targetValue); + } + + template + void Add::setValue(std::map const& metaVariableToValueMap, ValueType const& targetValue) { + Bdd valueEncoding = this->getDdManager()->getBddOne(); + for (auto const& nameValuePair : metaVariableToValueMap) { + valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + // Also record that the DD now contains the meta variable. + this->addMetaVariable(nameValuePair.first); + } + + internalAdd = valueEncoding.toAdd().ite(this->getDdManager()->getConstant(targetValue), internalAdd); + } + + template + ValueType Add::getValue(std::map const& metaVariableToValueMap) const { + std::set remainingMetaVariables(this->getContainedMetaVariables()); + Bdd valueEncoding = this->getDdManager()->getBddOne(); + for (auto const& nameValuePair : metaVariableToValueMap) { + valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + if (this->containsMetaVariable(nameValuePair.first)) { + remainingMetaVariables.erase(nameValuePair.first); + } + } + + STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given."); + + Add value = *this * valueEncoding.toAdd(); + value = value.sumAbstract(this->getContainedMetaVariables()); + return value.getMax(); + } + + template + bool Add::isOne() const { + return internalAdd.isOne(); + } + + template + bool Add::isZero() const { + return internalAdd.isZero(); + } + + template + bool Add::isConstant() const { + return internalAdd.isConstant(); + } + + template + uint_fast64_t Add::getIndex() const { + return internalAdd.getIndex(); + } + + template + std::vector Add::toVector() const { + return this->toVector(Odd(*this)); + } + + template + std::vector Add::toVector(Odd const& rowOdd) const { + std::vector result(rowOdd.getTotalOffset()); + std::vector ddVariableIndices = this->getDdManager().getSortedVariableIndices(); + addToVector(rowOdd, ddVariableIndices, result); + return result; + } + + template + std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector const& groupOffsets) const { + std::set rowMetaVariables; + + // Prepare the proper sets of meta variables. + for (auto const& variable : this->getContainedMetaVariables()) { + if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { + continue; + } + + rowMetaVariables.insert(variable); + } + std::vector ddGroupVariableIndices; + for (auto const& variable : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::vector ddRowVariableIndices; + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + } + + return internalAdd.toVector(ddGroupVariableIndices, rowOdd, ddRowVariableIndices, groupOffsets); + } + + template + storm::storage::SparseMatrix Add::toMatrix() const { + std::set rowVariables; + std::set columnVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnVariables.insert(variable); + } else { + rowVariables.insert(variable); + } + } + + return toMatrix(rowVariables, columnVariables, Odd(this->sumAbstract(rowVariables)), Odd(this->sumAbstract(columnVariables))); + } + + template + storm::storage::SparseMatrix Add::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); + } else { + rowMetaVariables.insert(variable); + } + } + + return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); + } + + template + storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::vector ddRowVariableIndices; + std::vector ddColumnVariableIndices; + + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); + + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); + + return internalAdd.toMatrix(rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); + } + + template + storm::storage::SparseMatrix Add::toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. + if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { + continue; + } + + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); + } else { + rowMetaVariables.insert(variable); + } + } + + // Create the canonical row group sizes and build the matrix. + return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + } + + template + storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::vector ddRowVariableIndices; + std::vector ddColumnVariableIndices; + std::vector ddGroupVariableIndices; + std::set rowAndColumnMetaVariables; + + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); + for (auto const& variable : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); + + return internalAdd.toMatrix(ddGroupVariableIndices, rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); + } + + template + std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. + if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { + continue; + } + + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); + } else { + rowMetaVariables.insert(variable); + } + } + + // Create the canonical row group sizes and build the matrix. + return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + } + + template + std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::vector ddRowVariableIndices; + std::vector ddColumnVariableIndices; + std::vector ddGroupVariableIndices; + std::set rowAndColumnMetaVariables; + + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); + for (auto const& variable : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); + + return internalAdd.toMatrixVector(vector.internalAdd, ddGroupVariableIndices, std::move(rowGroupIndices), rowOdd, ddRowVariableIndices, columnOdd, ddColumnVariableIndices); + } + + template + void Add::exportToDot(std::string const& filename) const { + internalAdd.exportToDot(filename, this->getDdManager()->getDdVariableNames()); + } + + template + AddIterator Add::begin(bool enumerateDontCareMetaVariables) const { + internalAdd.begin(this->getContainedMetaVariables(), enumerateDontCareMetaVariables); + } + + template + AddIterator Add::end(bool enumerateDontCareMetaVariables) const { + return internalAdd.end(enumerateDontCareMetaVariables); + } + + template + std::ostream& operator<<(std::ostream& out, Add const& add) { + out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl; + std::vector variableNames; + for (auto const& variable : add.getContainedMetaVariables()) { + variableNames.push_back(variable.getName()); + } + out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl; + return out; + } + + template + void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { + std::function fct = [] (ValueType const& a, ValueType const& b) -> ValueType { return a + b; }; + return internalAdd.composeVector(odd, ddVariableIndices, targetVector, fct); + } + + template + Add Add::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables) { + return Add(ddManager, InternalAdd::fromVector(ddManager, values, odd, ddManager->getSortedVariableIndices(metaVariables)), metaVariables); + } + + template + Bdd Add::toBdd() const { + return Bdd(this->getDdManager(), internalAdd.toBdd(), this->getContainedMetaVariables()); + } + template class Add; } } \ No newline at end of file diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index fe66826ac..94fa94b84 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -1,6 +1,8 @@ #ifndef STORM_STORAGE_DD_ADD_H_ #define STORM_STORAGE_DD_ADD_H_ +#include + #include "src/storage/dd/Dd.h" #include "src/storage/dd/DdType.h" @@ -8,25 +10,682 @@ namespace storm { namespace dd { + template + class Bdd; + + template + class Odd; + template - class Add { + class AddIterator; + + template + class Add : public Dd { + public: friend class DdManager; // Instantiate all copy/move constructors/assignments with the default implementation. Add() = default; - Add(Add const& other) = default; - Add& operator=(Add const& other) = default; - Add(Add&& other) = default; - Add& operator=(Add&& other) = default; + Add(Add const& other) = default; + Add& operator=(Add const& other) = default; + Add(Add&& other) = default; + Add& operator=(Add&& other) = default; + + /*! + * Retrieves whether the two DDs represent the same function. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the same function. + */ + bool operator==(Add const& other) const; + + /*! + * Retrieves whether the two DDs represent different functions. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the different functions. + */ + bool operator!=(Add const& other) const; + + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + * + * @param thenDd The ADD specifying the 'then' part. + * @param elseDd The ADD specifying the 'else' part. + * @return The ADD corresponding to the if-then-else of the operands. + */ + Add ite(Add const& thenAdd, Add const& elseAdd) const; + + /*! + * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in + * the result and vice versa. + * + * @return The resulting ADD. + */ + Add operator!() const; + + /*! + * Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be + * 0/1 ADDs. + * + * @param other The second ADD used for the operation. + * @return The logical or of the operands. + */ + Add operator||(Add const& other) const; + + /*! + * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a + * prerequisite, the operand ADDs need to be 0/1 ADDs. + * + * @param other The second ADD used for the operation. + * @return A reference to the current ADD after the operation + */ + Add& operator|=(Add const& other); + + /*! + * Adds the two ADDs. + * + * @param other The ADD to add to the current one. + * @return The result of the addition. + */ + Add operator+(Add const& other) const; + + /*! + * Adds the given ADD to the current one. + * + * @param other The ADD to add to the current one. + * @return A reference to the current ADD after the operation. + */ + Add& operator+=(Add const& other); + + /*! + * Multiplies the two ADDs. + * + * @param other The ADD to multiply with the current one. + * @return The result of the multiplication. + */ + Add operator*(Add const& other) const; + + /*! + * Multiplies the given ADD with the current one and assigns the result to the current ADD. + * + * @param other The ADD to multiply with the current one. + * @return A reference to the current ADD after the operation. + */ + Add& operator*=(Add const& other); + + /*! + * Subtracts the given ADD from the current one. + * + * @param other The ADD to subtract from the current one. + * @return The result of the subtraction. + */ + Add operator-(Add const& other) const; + + /*! + * Subtracts the ADD from the constant zero function. + * + * @return The resulting function represented as a ADD. + */ + Add operator-() const; + + /*! + * Subtracts the given ADD from the current one and assigns the result to the current ADD. + * + * @param other The ADD to subtract from the current one. + * @return A reference to the current ADD after the operation. + */ + Add& operator-=(Add const& other); + + /*! + * Divides the current ADD by the given one. + * + * @param other The ADD by which to divide the current one. + * @return The result of the division. + */ + Add operator/(Add const& other) const; + + /*! + * Divides the current ADD by the given one and assigns the result to the current ADD. + * + * @param other The ADD by which to divide the current one. + * @return A reference to the current ADD after the operation. + */ + Add& operator/=(Add const& other); + + /*! + * Retrieves the function that maps all evaluations to one that have identical function values. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add equals(Add const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one that have distinct function values. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add notEquals(Add const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less + * than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add less(Add const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or + * equal than the one in the given ADD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add lessOrEqual(Add const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add greater(Add const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * or equal than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add greaterOrEqual(Add const& other) const; + + /*! + * Retrieves the function that represents the current ADD to the power of the given ADD. + * + * @other The exponent function (given as an ADD). + * @retur The resulting ADD. + */ + Add pow(Add const& other) const; + + /*! + * Retrieves the function that represents the current ADD modulo the given ADD. + * + * @other The modul function (given as an ADD). + * @retur The resulting ADD. + */ + Add mod(Add const& other) const; + + /*! + * Retrieves the function that represents the logarithm of the current ADD to the bases given by the second + * ADD. + * + * @other The base function (given as an ADD). + * @retur The resulting ADD. + */ + Add logxy(Add const& other) const; + + /*! + * Retrieves the function that floors all values in the current ADD. + * + * @retur The resulting ADD. + */ + Add floor() const; + + /*! + * Retrieves the function that ceils all values in the current ADD. + * + * @retur The resulting ADD. + */ + Add ceil() const; + + /*! + * Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add minimum(Add const& other) const; + + /*! + * Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + Add maximum(Add const& other) const; + + /*! + * Sum-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Add sumAbstract(std::set const& metaVariables) const; + + /*! + * Min-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Add minAbstract(std::set const& metaVariables) const; + + /*! + * Max-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Add maxAbstract(std::set const& metaVariables) const; + + /*! + * Checks whether the current and the given ADD represent the same function modulo some given precision. + * + * @param other The ADD with which to compare. + * @param precision An upper bound on the maximal difference between any two function values that is to be + * tolerated. + * @param relative If set to true, not the absolute values have to be within the precision, but the relative + * values. + */ + bool equalModuloPrecision(Add const& other, double precision, bool relative = true) const; + + /*! + * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have + * the same number of underlying ADD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @return The resulting ADD. + */ + Add swapVariables(std::vector> const& metaVariablePairs) const; + + /*! + * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta + * variables. + * + * @param otherMatrix The matrix with which to multiply. + * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- + * matrix multiplication. + * @return An ADD representing the result of the matrix-matrix multiplication. + */ + Add multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value strictly + * larger than the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + Bdd greater(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value larger or equal + * to the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + Bdd greaterOrEqual(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value strictly + * lower than the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + Bdd less(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value less or equal + * to the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + Bdd lessOrEqual(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value unequal to + * zero are mapped to one and all others to zero. + * + * @return The resulting DD. + */ + Bdd notZero() const; + + /*! + * Computes the constraint of the current ADD with the given constraint. That is, the function value of the + * resulting ADD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting ADD. + */ + Add constrain(Add const& constraint) const; + + /*! + * Computes the restriction of the current ADD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting ADD. + */ + Add restrict(Add const& constraint) const; + + /*! + * Retrieves the support of the current ADD. + * + * @return The support represented as a BDD. + */ + Bdd getSupport() const override; + + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @return The number of encodings that are mapped to a non-zero value. + */ + virtual uint_fast64_t getNonZeroCount() const override; + + /*! + * Retrieves the number of leaves of the ADD. + * + * @return The number of leaves of the ADD. + */ + virtual uint_fast64_t getLeafCount() const override; + + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + virtual uint_fast64_t getNodeCount() const override; + + /*! + * Retrieves the lowest function value of any encoding. + * + * @return The lowest function value of any encoding. + */ + ValueType getMin() const; + + /*! + * Retrieves the highest function value of any encoding. + * + * @return The highest function value of any encoding. + */ + ValueType getMax() const; + + /*! + * Sets the function values of all encodings that have the given value of the meta variable to the given + * target value. + * + * @param metaVariable The meta variable that has to be equal to the given value. + * @param variableValue The value that the meta variable is supposed to have. This must be within the range + * of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, ValueType const& targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the two meta variables to the + * given target value. + * + * @param metaVariable1 The first meta variable that has to be equal to the first given + * value. + * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the + * range of the meta variable. + * @param metaVariable2 The second meta variable that has to be equal to the second given + * value. + * @param variableValue2 The value that the second meta variable is supposed to have. This must be within + * the range of the meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, ValueType const& targetValue); + + /*! + * Sets the function values of all encodings that have the given values of the given meta variables to the + * given target value. + * + * @param metaVariableToValueMap A mapping of meta variables to the values they are supposed to have. All + * values must be within the range of the respective meta variable. + * @param targetValue The new function value of the modified encodings. + */ + void setValue(std::map const& metaVariableToValueMap = std::map(), ValueType const& targetValue = 0); + + /*! + * Retrieves the value of the function when all meta variables are assigned the values of the given mapping. + * Note that the mapping must specify values for all meta variables contained in the DD. + * + * @param metaVariableToValueMap A mapping of meta variables to their values. + * @return The value of the function evaluated with the given input. + */ + ValueType getValue(std::map const& metaVariableToValueMap = std::map()) const; + + /*! + * Retrieves whether this ADD represents the constant one function. + * + * @return True if this ADD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this ADD represents the constant zero function. + * + * @return True if this ADD represents the constant zero function. + */ + bool isZero() const; + + /*! + * Retrieves whether this ADD represents a constant function. + * + * @return True if this ADD represents a constants function. + */ + bool isConstant() const; + + /*! + * Retrieves the index of the topmost variable in the DD. + * + * @return The index of the topmost variable in DD. + */ + virtual uint_fast64_t getIndex() const override; + + /*! + * Converts the ADD to a vector. + * + * @return The vector that is represented by this ADD. + */ + std::vector toVector() const; + + /*! + * Converts the ADD to a vector. The given offset-labeled DD is used to determine the correct row of + * each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @return The vector that is represented by this ADD. + */ + std::vector toVector(storm::dd::Odd const& rowOdd) const; + + /*! + * Converts the ADD to a row-grouped vector. The given offset-labeled DD is used to determine the correct + * row group of each entry. Note that the group meta variables are assumed to be at the very top in the + * variable ordering. + * + * @param groupMetaVariables The meta variables responsible for the row-grouping. + * @param rowOdd The ODD used for determining the correct row. + * @return The vector that is represented by this ADD. + */ + std::vector toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector const& groupOffsets) const; + + /*! + * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the + * row, whereas all primed variables are assumed to encode the column. + * + * @return The matrix that is represented by this ADD. + */ + storm::storage::SparseMatrix toMatrix() const; + + /*! + * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the + * row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used + * to determine the correct row and column, respectively, for each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD. + */ + storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the ADD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the + * correct row and column, respectively, for each entry. + * + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD. + */ + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to + * determine the correct row and column, respectively, for each entry. Note: this function assumes that + * the meta variables used to distinguish different row groups are at the very top of the ADD. + * + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD. + */ + storm::storage::SparseMatrix toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to a row-grouped vector. + * The given offset-labeled DDs are used to determine the correct row and column, respectively, for each + * entry. Note: this function assumes that the meta variables used to distinguish different row groups are + * at the very top of the ADD. + * + * @param vector The symbolic vector to convert. + * @param rowGroupSizes A vector specifying the sizes of the row groups. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD. + */ + std::pair, std::vector> toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToDot(std::string const& filename) const override; + + /*! + * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. + * + * @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. + * @return An iterator that points to the first meta variable assignment with a non-zero function value. + */ + AddIterator begin(bool enumerateDontCareMetaVariables = true) const; + + /*! + * Retrieves an iterator that points past the end of the container. + * + * @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. + * @return An iterator that points past the end of the container. + */ + AddIterator end(bool enumerateDontCareMetaVariables = true) const; + + friend std::ostream & operator<<(std::ostream& out, const Add& add); + + /*! + * Converts the ADD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as + * a call to notZero(). + * + * @return The corresponding BDD. + */ + Bdd toBdd() const; + private: + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddBdd The CUDD BDD to store. + * @param containedMetaVariables The meta variables that appear in the DD. + */ + Add(std::shared_ptr const> ddManager, InternalAdd const& internalAdd, std::set const& containedMetaVariables = std::set()); + /*! * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions. */ operator InternalAdd(); operator InternalAdd const() const; + /*! + * Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also + * translated to an explicit row-grouped vector with the same row-grouping. The given offset-labeled DDs + * are used to determine the correct row and column, respectively, for each entry. Note: this function + * assumes that the meta variables used to distinguish different row groups are at the very top of the ADD. + * + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector + * (if it was given). + */ + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to an equally row-grouped + * explicit vector. The given offset-labeled DDs are used to determine the correct row and column, + * respectively, for each entry. Note: this function assumes that the meta variables used to distinguish + * different row groups are at the very top of the ADD. + * + * @param vector The vector that is to be transformed to an equally grouped explicit vector. + * @param rowGroupSizes A vector specifying the sizes of the row groups. + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector + * (if it was given). + */ + std::pair, std::vector> toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Adds the current (DD-based) vector to the given explicit one. + * + * @param odd The ODD used for the translation. + * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. + * @param targetVector The vector to which the translated DD-based vector is to be added. + */ + void addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + + /*! + * Builds an ADD representing the given vector. + * + * @param ddManager The manager responsible for the ADD. + * @param values The vector that is to be represented by the ADD. + * @param odd The ODD used for the translation. + * @param metaVariables The meta variables used for the translation. + * @return The resulting (CUDD) ADD. + */ + static Add fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); + // The internal ADD that depends on the chosen library. - InternalAdd internalAdd; + InternalAdd internalAdd; }; } } diff --git a/src/storage/dd/DdForwardIterator.h b/src/storage/dd/AddIterator.h similarity index 66% rename from src/storage/dd/DdForwardIterator.h rename to src/storage/dd/AddIterator.h index 2eed23090..17186a874 100644 --- a/src/storage/dd/DdForwardIterator.h +++ b/src/storage/dd/AddIterator.h @@ -6,7 +6,8 @@ namespace storm { namespace dd { // Declare DdIterator class so we can then specialize it for the different DD types. - template class DdForwardIterator; + template + class DdForwardIterator; } } diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index a03655ffc..83c624f40 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -36,7 +36,7 @@ namespace storm { template template - Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { + Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { return Bdd(ddManager, InternalBdd::fromVector(ddManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables); } @@ -52,7 +52,7 @@ namespace storm { template Bdd Bdd::ite(Bdd const& thenBdd, Bdd const& elseBdd) const { - std::set metaVariables = Dd::joinMetaVariables(*this, thenBdd); + std::set metaVariables = Dd::joinMetaVariables(thenBdd, elseBdd); metaVariables.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); return Bdd(this->getDdManager(), internalBdd.ite(thenBdd.internalBdd, elseBdd.internalBdd), metaVariables); } diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index d83dbfd0a..c26d0f90f 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -263,7 +263,7 @@ namespace storm { * @return The resulting (CUDD) BDD. */ template - static Bdd fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + static Bdd fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); // The internal BDD that depends on the chosen library. InternalBdd internalBdd; diff --git a/src/storage/dd/cudd/CuddAdd.cpp b/src/storage/dd/cudd/CuddAdd.cpp deleted file mode 100644 index 55b40b62c..000000000 --- a/src/storage/dd/cudd/CuddAdd.cpp +++ /dev/null @@ -1,1084 +0,0 @@ -#include -#include -#include - -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" -#include "src/storage/dd/cudd/CuddOdd.h" -#include "src/storage/dd/cudd/CuddDdManager.h" -#include "src/utility/vector.h" -#include "src/utility/macros.h" - - -#include "src/storage/SparseMatrix.h" - - -#include "src/exceptions/IllegalFunctionCallException.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/exceptions/NotImplementedException.h" - -namespace storm { - namespace dd { - Add::Add(std::shared_ptr const> ddManager, ADD cuddAdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), cuddAdd(cuddAdd) { - // Intentionally left empty. - } - - Add::Add(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables) : Dd(ddManager, metaVariables) { - cuddAdd = fromVector(ddManager, values, odd, metaVariables); - } - - Bdd Add::toBdd() const { - return Bdd(this->getDdManager(), this->getCuddAdd().BddPattern(), this->getContainedMetaVariables()); - } - - ADD Add::getCuddAdd() const { - return this->cuddAdd; - } - - DdNode* Add::getCuddDdNode() const { - return this->getCuddAdd().getNode(); - } - - bool Add::operator==(Add const& other) const { - return this->getCuddAdd() == other.getCuddAdd(); - } - - bool Add::operator!=(Add const& other) const { - return !(*this == other); - } - - Add Add::ite(Add const& thenDd, Add const& elseDd) const { - std::set metaVariableNames; - std::set_union(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end(), elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end(), std::inserter(metaVariableNames, metaVariableNames.begin())); - metaVariableNames.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); - - return Add(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames); - } - - Add Add::operator!() const { - return Add(this->getDdManager(), ~this->getCuddAdd(), this->getContainedMetaVariables()); - } - - Add Add::operator||(Add const& other) const { - Add result(*this); - result |= other; - return result; - } - - Add& Add::operator|=(Add const& other) { - this->addMetaVariables(other.getContainedMetaVariables()); - this->cuddAdd = this->getCuddAdd() | other.getCuddAdd(); - return *this; - } - - Add Add::operator+(Add const& other) const { - Add result(*this); - result += other; - return result; - } - - Add& Add::operator+=(Add const& other) { - this->addMetaVariables(other.getContainedMetaVariables()); - this->cuddAdd = this->getCuddAdd() + other.getCuddAdd(); - return *this; - } - - Add Add::operator*(Add const& other) const { - Add result(*this); - result *= other; - return result; - } - - Add& Add::operator*=(Add const& other) { - this->addMetaVariables(other.getContainedMetaVariables()); - this->cuddAdd = this->getCuddAdd() * other.getCuddAdd(); - return *this; - } - - Add Add::operator-(Add const& other) const { - Add result(*this); - result -= other; - return result; - } - - Add Add::operator-() const { - return this->getDdManager()->getAddZero() - *this; - } - - Add& Add::operator-=(Add const& other) { - this->addMetaVariables(other.getContainedMetaVariables()); - this->cuddAdd = this->getCuddAdd() - other.getCuddAdd(); - return *this; - } - - Add Add::operator/(Add const& other) const { - Add result(*this); - result /= other; - return result; - } - - Add& Add::operator/=(Add const& other) { - this->addMetaVariables(other.getContainedMetaVariables()); - this->cuddAdd = this->getCuddAdd().Divide(other.getCuddAdd()); - return *this; - } - - Add Add::equals(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariables); - } - - Add Add::notEquals(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariables); - } - - Add Add::less(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariables); - } - - Add Add::lessOrEqual(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariables); - } - - Add Add::greater(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariables); - } - - Add Add::greaterOrEqual(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariables); - } - - Add Add::pow(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().Pow(other.getCuddAdd()), metaVariables); - } - - Add Add::mod(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().Mod(other.getCuddAdd()), metaVariables); - } - - Add Add::logxy(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().LogXY(other.getCuddAdd()), metaVariables); - } - - Add Add::floor() const { - return Add(this->getDdManager(), this->getCuddAdd().Floor(), this->getContainedMetaVariables()); - } - - Add Add::ceil() const { - return Add(this->getDdManager(), this->getCuddAdd().Ceil(), this->getContainedMetaVariables()); - } - - Add Add::minimum(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariables); - } - - Add Add::maximum(Add const& other) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariables); - } - - Add Add::sumAbstract(std::set const& metaVariables) const { - Bdd cubeDd = this->getDdManager()->getBddOne(); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); - } - - return Add(this->getDdManager(), this->getCuddAdd().ExistAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables); - } - - Add Add::minAbstract(std::set const& metaVariables) const { - Bdd cubeDd = this->getDdManager()->getBddOne(); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); - } - - return Add(this->getDdManager(), this->getCuddAdd().MinAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables); - } - - Add Add::maxAbstract(std::set const& metaVariables) const { - Bdd cubeDd = this->getDdManager()->getBddOne(); - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeDd &= ddMetaVariable.getCube(); - } - - return Add(this->getDdManager(), this->getCuddAdd().MaxAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables); - } - - bool Add::equalModuloPrecision(Add const& other, double precision, bool relative) const { - if (relative) { - return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); - } else { - return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); - } - } - - Add Add::swapVariables(std::vector> const& metaVariablePairs) const { - std::set newContainedMetaVariables; - std::vector from; - std::vector to; - for (auto const& metaVariablePair : metaVariablePairs) { - DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); - DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); - - // Check if it's legal so swap the meta variables. - if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) { - throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size."; - } - - // Keep track of the contained meta variables in the DD. - if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); - } - - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.toAdd().getCuddAdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.toAdd().getCuddAdd()); - } - } - - // Finally, call CUDD to swap the variables. - return Add(this->getDdManager(), this->getCuddAdd().SwapVariables(from, to), newContainedMetaVariables); - } - - Add Add::multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const { - // Create the CUDD summation variables. - std::vector summationDdVariables; - for (auto const& metaVariable : summationMetaVariables) { - for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { - summationDdVariables.push_back(ddVariable.toAdd().getCuddAdd()); - } - } - - std::set unionOfMetaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); - std::set containedMetaVariables; - std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - - return Add(this->getDdManager(), this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables); - } - - Bdd Add::greater(double value) const { - return Bdd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value), this->getContainedMetaVariables()); - } - - Bdd Add::greaterOrEqual(double value) const { - return Bdd(this->getDdManager(), this->getCuddAdd().BddThreshold(value), this->getContainedMetaVariables()); - } - - Bdd Add::less(double value) const { - return Bdd(this->getDdManager(), ~this->getCuddAdd().BddThreshold(value), this->getContainedMetaVariables()); - } - - Bdd Add::lessOrEqual(double value) const { - return Bdd(this->getDdManager(), ~this->getCuddAdd().BddStrictThreshold(value), this->getContainedMetaVariables()); - } - - Bdd Add::notZero() const { - return this->toBdd(); - } - - Add Add::constrain(Add const& constraint) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariables); - } - - Add Add::restrict(Add const& constraint) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Add(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariables); - } - - Bdd Add::getSupport() const { - return Bdd(this->getDdManager(), this->getCuddAdd().Support(), this->getContainedMetaVariables()); - } - - uint_fast64_t Add::getNonZeroCount() const { - std::size_t numberOfDdVariables = 0; - for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); - } - return static_cast(this->getCuddAdd().CountMinterm(static_cast(numberOfDdVariables))); - } - - uint_fast64_t Add::getLeafCount() const { - return static_cast(this->getCuddAdd().CountLeaves()); - } - - uint_fast64_t Add::getNodeCount() const { - return static_cast(this->getCuddAdd().nodeCount()); - } - - double Add::getMin() const { - ADD constantMinAdd = this->getCuddAdd().FindMin(); - return static_cast(Cudd_V(constantMinAdd.getNode())); - } - - double Add::getMax() const { - ADD constantMaxAdd = this->getCuddAdd().FindMax(); - return static_cast(Cudd_V(constantMaxAdd.getNode())); - } - - void Add::setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue) { - std::map metaVariableToValueMap; - metaVariableToValueMap.emplace(metaVariable, variableValue); - this->setValue(metaVariableToValueMap, targetValue); - } - - void Add::setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue) { - std::map metaVariableToValueMap; - metaVariableToValueMap.emplace(metaVariable1, variableValue1); - metaVariableToValueMap.emplace(metaVariable2, variableValue2); - this->setValue(metaVariableToValueMap, targetValue); - } - - void Add::setValue(std::map const& metaVariableToValueMap, double targetValue) { - Bdd valueEncoding = this->getDdManager()->getBddOne(); - for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); - // Also record that the DD now contains the meta variable. - this->addMetaVariable(nameValuePair.first); - } - - this->cuddAdd = valueEncoding.toAdd().getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->getCuddAdd()); - } - - double Add::getValue(std::map const& metaVariableToValueMap) const { - std::set remainingMetaVariables(this->getContainedMetaVariables()); - Bdd valueEncoding = this->getDdManager()->getBddOne(); - for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); - if (this->containsMetaVariable(nameValuePair.first)) { - remainingMetaVariables.erase(nameValuePair.first); - } - } - - STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given."); - - Add value = *this * valueEncoding.toAdd(); - value = value.sumAbstract(this->getContainedMetaVariables()); - return static_cast(Cudd_V(value.getCuddAdd().getNode())); - } - - bool Add::isOne() const { - return this->getCuddAdd().IsOne(); - } - - bool Add::isZero() const { - return this->getCuddAdd().IsZero(); - } - - bool Add::isConstant() const { - return Cudd_IsConstant(this->getCuddAdd().getNode()); - } - - uint_fast64_t Add::getIndex() const { - return static_cast(this->getCuddAdd().NodeReadIndex()); - } - - template - std::vector Add::toVector() const { - return this->toVector(Odd(*this)); - } - - template - std::vector Add::toVector(Odd const& rowOdd) const { - std::vector result(rowOdd.getTotalOffset()); - std::vector ddVariableIndices = this->getSortedVariableIndices(); - addToVector(rowOdd, ddVariableIndices, result); - return result; - } - - template - std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector groupOffsets) const { - std::set rowMetaVariables; - - // Prepare the proper sets of meta variables. - for (auto const& variable : this->getContainedMetaVariables()) { - if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { - continue; - } - - rowMetaVariables.insert(variable); - } - std::vector ddGroupVariableIndices; - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::vector ddRowVariableIndices; - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // Start by splitting the symbolic vector into groups. - std::vector> groups; - splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowMetaVariables); - - // Now iterate over the groups and add them to the resulting vector. - std::vector result(groupOffsets.back(), storm::utility::zero()); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - toVectorRec(groups[i].getCuddDdNode(), result, groupOffsets, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); - } - - return result; - } - - storm::storage::SparseMatrix Add::toMatrix() const { - std::set rowVariables; - std::set columnVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnVariables.insert(variable); - } else { - rowVariables.insert(variable); - } - } - - return toMatrix(rowVariables, columnVariables, Odd(this->sumAbstract(rowVariables)), Odd(this->sumAbstract(columnVariables))); - } - - storm::storage::SparseMatrix Add::toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::set rowMetaVariables; - std::set columnMetaVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnMetaVariables.insert(variable); - } else { - rowMetaVariables.insert(variable); - } - } - - return toMatrix(rowMetaVariables, columnMetaVariables, rowOdd, columnOdd); - } - - storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); - - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); - - // Prepare the vectors that represent the matrix. - std::vector rowIndications(rowOdd.getTotalOffset() + 1); - std::vector> columnsAndValues(this->getNonZeroCount()); - - // Create a trivial row grouping. - std::vector trivialRowGroupIndices(rowIndications.size()); - uint_fast64_t i = 0; - for (auto& entry : trivialRowGroupIndices) { - entry = i; - ++i; - } - - // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent - // it from actually generating the entries in the entry vector. - toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - - // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert - // the resulting (DD) vector to an explicit vector. - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - // Construct matrix and return result. - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); - } - - storm::storage::SparseMatrix Add::toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::set rowMetaVariables; - std::set columnMetaVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. - if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { - continue; - } - - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnMetaVariables.insert(variable); - } else { - rowMetaVariables.insert(variable); - } - } - - // Create the canonical row group sizes and build the matrix. - return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); - } - - storm::storage::SparseMatrix Add::toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - std::vector ddGroupVariableIndices; - std::set rowAndColumnMetaVariables; - boost::optional> optionalExplicitVector; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - - // Start by computing the offsets (in terms of rows) for each row group. - Add stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).toAdd().sumAbstract(groupMetaVariables); - std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); - rowGroupIndices.resize(rowGroupIndices.size() + 1); - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { - tmp2 = rowGroupIndices[i]; - rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowGroupIndices[0] = 0; - - // Next, we split the matrix into one for each group. This only works if the group variables are at the very - // top. - std::vector> groups; - splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); - - // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); - - // Now compute the indices at which the individual rows start. - std::vector rowIndications(rowGroupIndices.back() + 1); - - std::vector> statesWithGroupEnabled(groups.size()); - storm::dd::Add stateToRowGroupCount = this->getDdManager()->getAddZero(); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - - statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables).toAdd(); - stateToRowGroupCount += statesWithGroupEnabled[i]; - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; - modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - tmp = 0; - tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i]; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); - } - - std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::set rowMetaVariables; - std::set columnMetaVariables; - - for (auto const& variable : this->getContainedMetaVariables()) { - // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. - if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { - continue; - } - - if (variable.getName().size() > 0 && variable.getName().back() == '\'') { - columnMetaVariables.insert(variable); - } else { - rowMetaVariables.insert(variable); - } - } - - // Create the canonical row group sizes and build the matrix. - return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); - } - - std::pair,std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { - std::vector ddRowVariableIndices; - std::vector ddColumnVariableIndices; - std::vector ddGroupVariableIndices; - std::set rowAndColumnMetaVariables; - - for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddRowVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); - for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddColumnVariableIndices.push_back(ddVariable.getIndex()); - } - rowAndColumnMetaVariables.insert(variable); - } - std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); - for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddGroupVariableIndices.push_back(ddVariable.getIndex()); - } - } - std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - - // Transform the row group sizes to the actual row group indices. - rowGroupIndices.resize(rowGroupIndices.size() + 1); - uint_fast64_t tmp = 0; - uint_fast64_t tmp2 = 0; - for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { - tmp2 = rowGroupIndices[i]; - rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowGroupIndices[0] = 0; - - // Create the explicit vector we need to fill later. - std::vector explicitVector(rowGroupIndices.back()); - - // Next, we split the matrix into one for each group. This only works if the group variables are at the very top. - std::vector, Add>> groups; - splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables, rowMetaVariables); - - // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); - - // Now compute the indices at which the individual rows start. - std::vector rowIndications(rowGroupIndices.back() + 1); - - std::vector> statesWithGroupEnabled(groups.size()); - storm::dd::Add stateToRowGroupCount = this->getDdManager()->getAddZero(); - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - std::pair, storm::dd::Add> ddPair = groups[i]; - - toMatrixRec(ddPair.first.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); - toVectorRec(ddPair.second.getCuddDdNode(), explicitVector, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); - - statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnMetaVariables) || ddPair.second.notZero()).toAdd(); - stateToRowGroupCount += statesWithGroupEnabled[i]; - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; - modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. - tmp = 0; - tmp2 = 0; - for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { - tmp2 = rowIndications[i]; - rowIndications[i] = rowIndications[i - 1] + tmp; - std::swap(tmp, tmp2); - } - rowIndications[0] = 0; - - // Now actually fill the entry vector. - for (uint_fast64_t i = 0; i < groups.size(); ++i) { - auto const& dd = groups[i].first; - - toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - - statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); - } - - // Since we modified the rowGroupIndices, we need to restore the correct values. - modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); - - // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. - for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { - rowIndications[i] = rowIndications[i - 1]; - } - rowIndications[0] = 0; - - return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); - } - - template - void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { - // For the empty DD, we do not need to add any entries. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentRowLevel == maxLevel) { - result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); - } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { - toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); - toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); - } else { - toVectorRec(Cudd_E(dd), result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); - toVectorRec(Cudd_T(dd), result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); - } - } - - void Add::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { - // For the empty DD, we do not need to add any entries. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentRowLevel + currentColumnLevel == maxLevel) { - if (generateValues) { - columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); - } - ++rowIndications[rowGroupOffsets[currentRowOffset]]; - } else { - DdNode const* elseElse; - DdNode const* elseThen; - DdNode const* thenElse; - DdNode const* thenThen; - - if (ddColumnVariableIndices[currentColumnLevel] < dd->index) { - elseElse = elseThen = thenElse = thenThen = dd; - } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) { - elseElse = thenElse = Cudd_E(dd); - elseThen = thenThen = Cudd_T(dd); - } else { - DdNode const* elseNode = Cudd_E(dd); - if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) { - elseElse = elseThen = elseNode; - } else { - elseElse = Cudd_E(elseNode); - elseThen = Cudd_T(elseNode); - } - - DdNode const* thenNode = Cudd_T(dd); - if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) { - thenElse = thenThen = thenNode; - } else { - thenElse = Cudd_E(thenNode); - thenThen = Cudd_T(thenNode); - } - } - - // Visit else-else. - toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit else-then. - toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit then-else. - toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); - // Visit then-then. - toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); - } - } - - void Add::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const { - // For the empty DD, we do not need to create a group. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - if (currentLevel == maxLevel) { - groups.push_back(Add(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd), remainingMetaVariables)); - } else if (ddGroupVariableIndices[currentLevel] < dd->index) { - splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - } else { - splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables); - } - } - - void Add::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, Add>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables1, std::set const& remainingMetaVariables2) const { - // For the empty DD, we do not need to create a group. - if (dd1 == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - if (currentLevel == maxLevel) { - groups.push_back(std::make_pair(Add(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd1), remainingMetaVariables1), Add(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd2), remainingMetaVariables2))); - } else if (ddGroupVariableIndices[currentLevel] < dd1->index) { - if (ddGroupVariableIndices[currentLevel] < dd2->index) { - splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - } else { - splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - } - } else if (ddGroupVariableIndices[currentLevel] < dd2->index) { - splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - } else { - splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); - } - } - - template - void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { - std::function fct = [] (ValueType const& a, double const& b) -> ValueType { return a + b; }; - modifyVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, fct); - } - - template - void Add::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { - // For the empty DD, we do not need to add any entries. - if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentLevel == maxLevel) { - targetVector[currentOffset] = function(targetVector[currentOffset], Cudd_V(dd)); - } else if (ddVariableIndices[currentLevel] < dd->index) { - // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set - // and for the one in which it is not set. - modifyVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - modifyVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); - } else { - // Otherwise, we simply recursively call the function for both (different) cases. - modifyVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); - modifyVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); - } - } - - template - ADD Add::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables) { - std::vector ddVariableIndices = getSortedVariableIndices(*ddManager, metaVariables); - uint_fast64_t offset = 0; - return ADD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices)); - } - - template - DdNode* Add::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices) { - if (currentLevel == maxLevel) { - // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one - // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we - // need to copy the next value of the vector iff the then-offset is greater than zero. - if (odd.getThenOffset() > 0) { - return Cudd_addConst(manager, values[currentOffset++]); - } else { - return Cudd_ReadZero(manager); - } - } else { - // If the total offset is zero, we can just return the constant zero DD. - if (odd.getThenOffset() + odd.getElseOffset() == 0) { - return Cudd_ReadZero(manager); - } - - // Determine the new else-successor. - DdNode* elseSuccessor = nullptr; - if (odd.getElseOffset() > 0) { - elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices); - } else { - elseSuccessor = Cudd_ReadZero(manager); - } - Cudd_Ref(elseSuccessor); - - // Determine the new then-successor. - DdNode* thenSuccessor = nullptr; - if (odd.getThenOffset() > 0) { - thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices); - } else { - thenSuccessor = Cudd_ReadZero(manager); - } - Cudd_Ref(thenSuccessor); - - // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor); - DdNode* result = Cudd_addIthVar(manager, static_cast(ddVariableIndices[currentLevel])); - Cudd_Ref(result); - DdNode* newResult = Cudd_addIte(manager, result, thenSuccessor, elseSuccessor); - Cudd_Ref(newResult); - - // Dispose of the intermediate results - Cudd_RecursiveDeref(manager, result); - Cudd_RecursiveDeref(manager, thenSuccessor); - Cudd_RecursiveDeref(manager, elseSuccessor); - - // Before returning, we remove the protection imposed by the previous call to Cudd_Ref. - Cudd_Deref(newResult); - - return newResult; - } - } - - void Add::exportToDot(std::string const& filename) const { - if (filename.empty()) { - std::vector cuddAddVector = { this->getCuddAdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); - } else { - // Build the name input of the DD. - std::vector ddNames; - std::string ddName("f"); - ddNames.push_back(new char[ddName.size() + 1]); - std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); - - // Now build the variables names. - std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); - std::vector ddVariableNames; - for (auto const& element : ddVariableNamesAsStrings) { - ddVariableNames.push_back(new char[element.size() + 1]); - std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); - } - - // Open the file, dump the DD and close it again. - FILE* filePointer = fopen(filename.c_str() , "w"); - std::vector cuddAddVector = { this->getCuddAdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); - fclose(filePointer); - - // Finally, delete the names. - for (char* element : ddNames) { - delete[] element; - } - for (char* element : ddVariableNames) { - delete[] element; - } - } - } - - DdForwardIterator Add::begin(bool enumerateDontCareMetaVariables) const { - int* cube; - double value; - DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); - return DdForwardIterator(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables); - } - - DdForwardIterator Add::end(bool enumerateDontCareMetaVariables) const { - return DdForwardIterator(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); - } - - std::ostream& operator<<(std::ostream& out, const Add& add) { - out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl; - std::vector variableNames; - for (auto const& variable : add.getContainedMetaVariables()) { - variableNames.push_back(variable.getName()); - } - out << "contained variables: " << boost::algorithm::join(variableNames, ", ") << std::endl; - return out; - } - - // Explicitly instantiate some templated functions. - template std::vector Add::toVector() const; - template std::vector Add::toVector(Odd const& rowOdd) const; - template void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - template void Add::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; - template std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector groupOffsets) const; - template void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; - template std::vector Add::toVector() const; - template std::vector Add::toVector(Odd const& rowOdd) const; - template void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - template void Add::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; - - } -} \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddAdd.h b/src/storage/dd/cudd/CuddAdd.h deleted file mode 100644 index 324676129..000000000 --- a/src/storage/dd/cudd/CuddAdd.h +++ /dev/null @@ -1,828 +0,0 @@ -#ifndef STORM_STORAGE_DD_CUDDADD_H_ -#define STORM_STORAGE_DD_CUDDADD_H_ - -#include -#include - -#include "src/storage/dd/Add.h" -#include "src/storage/dd/cudd/CuddDd.h" -#include "src/storage/dd/cudd/CuddDdForwardIterator.h" -#include "src/storage/expressions/Variable.h" -#include "src/utility/OsDetection.h" - -// Include the C++-interface of CUDD. -#include "cuddObj.hh" - -namespace storm { - namespace storage { - template class SparseMatrix; - class BitVector; - template class MatrixEntry; - } - - namespace dd { - // Forward-declare some classes. - template class DdManager; - template class Odd; - template class Bdd; - - template<> - class Add : public Dd { - public: - // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. - friend class DdManager; - friend class DdForwardIterator; - friend class Bdd; - friend class Odd; - - /*! - * Creates an ADD from the given explicit vector. - * - * @param ddManager The manager responsible for this DD. - * @param values The vector that is to be represented by the ADD. - * @param odd An ODD that is used to do the translation. - * @param metaVariables The meta variables to use to encode the vector. - */ - Add(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); - - // Instantiate all copy/move constructors/assignments with the default implementation. - Add() = default; - Add(Add const& other) = default; - Add& operator=(Add const& other) = default; -#ifndef WINDOWS - Add(Add&& other) = default; - Add& operator=(Add&& other) = default; -#endif - - /*! - * Retrieves whether the two DDs represent the same function. - * - * @param other The DD that is to be compared with the current one. - * @return True if the DDs represent the same function. - */ - bool operator==(Add const& other) const; - - /*! - * Retrieves whether the two DDs represent different functions. - * - * @param other The DD that is to be compared with the current one. - * @return True if the DDs represent the different functions. - */ - bool operator!=(Add const& other) const; - - /*! - * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero - * function value to the function values specified by the first DD and all others to the function values - * specified by the second DD. - * - * @param thenDd The ADD specifying the 'then' part. - * @param elseDd The ADD specifying the 'else' part. - * @return The ADD corresponding to the if-then-else of the operands. - */ - Add ite(Add const& thenDd, Add const& elseDd) const; - - /*! - * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in - * the result and vice versa. - * - * @return The resulting ADD. - */ - Add operator!() const; - - /*! - * Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be - * 0/1 ADDs. - * - * @param other The second ADD used for the operation. - * @return The logical or of the operands. - */ - Add operator||(Add const& other) const; - - /*! - * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a - * prerequisite, the operand ADDs need to be 0/1 ADDs. - * - * @param other The second ADD used for the operation. - * @return A reference to the current ADD after the operation - */ - Add& operator|=(Add const& other); - - /*! - * Adds the two ADDs. - * - * @param other The ADD to add to the current one. - * @return The result of the addition. - */ - Add operator+(Add const& other) const; - - /*! - * Adds the given ADD to the current one. - * - * @param other The ADD to add to the current one. - * @return A reference to the current ADD after the operation. - */ - Add& operator+=(Add const& other); - - /*! - * Multiplies the two ADDs. - * - * @param other The ADD to multiply with the current one. - * @return The result of the multiplication. - */ - Add operator*(Add const& other) const; - - /*! - * Multiplies the given ADD with the current one and assigns the result to the current ADD. - * - * @param other The ADD to multiply with the current one. - * @return A reference to the current ADD after the operation. - */ - Add& operator*=(Add const& other); - - /*! - * Subtracts the given ADD from the current one. - * - * @param other The ADD to subtract from the current one. - * @return The result of the subtraction. - */ - Add operator-(Add const& other) const; - - /*! - * Subtracts the ADD from the constant zero function. - * - * @return The resulting function represented as a ADD. - */ - Add operator-() const; - - /*! - * Subtracts the given ADD from the current one and assigns the result to the current ADD. - * - * @param other The ADD to subtract from the current one. - * @return A reference to the current ADD after the operation. - */ - Add& operator-=(Add const& other); - - /*! - * Divides the current ADD by the given one. - * - * @param other The ADD by which to divide the current one. - * @return The result of the division. - */ - Add operator/(Add const& other) const; - - /*! - * Divides the current ADD by the given one and assigns the result to the current ADD. - * - * @param other The ADD by which to divide the current one. - * @return A reference to the current ADD after the operation. - */ - Add& operator/=(Add const& other); - - /*! - * Retrieves the function that maps all evaluations to one that have identical function values. - * - * @param other The ADD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add equals(Add const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one that have distinct function values. - * - * @param other The ADD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add notEquals(Add const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less - * than the one in the given ADD. - * - * @param other The ADD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add less(Add const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or - * equal than the one in the given ADD. - * - * @param other The DD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add lessOrEqual(Add const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater - * than the one in the given ADD. - * - * @param other The ADD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add greater(Add const& other) const; - - /*! - * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater - * or equal than the one in the given ADD. - * - * @param other The ADD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add greaterOrEqual(Add const& other) const; - - /*! - * Retrieves the function that represents the current ADD to the power of the given ADD. - * - * @other The exponent function (given as an ADD). - * @retur The resulting ADD. - */ - Add pow(Add const& other) const; - - /*! - * Retrieves the function that represents the current ADD modulo the given ADD. - * - * @other The modul function (given as an ADD). - * @retur The resulting ADD. - */ - Add mod(Add const& other) const; - - /*! - * Retrieves the function that represents the logarithm of the current ADD to the bases given by the second - * ADD. - * - * @other The base function (given as an ADD). - * @retur The resulting ADD. - */ - Add logxy(Add const& other) const; - - /*! - * Retrieves the function that floors all values in the current ADD. - * - * @retur The resulting ADD. - */ - Add floor() const; - - /*! - * Retrieves the function that ceils all values in the current ADD. - * - * @retur The resulting ADD. - */ - Add ceil() const; - - /*! - * Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs. - * - * @param other The ADD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add minimum(Add const& other) const; - - /*! - * Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs. - * - * @param other The ADD with which to perform the operation. - * @return The resulting function represented as an ADD. - */ - Add maximum(Add const& other) const; - - /*! - * Sum-abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Add sumAbstract(std::set const& metaVariables) const; - - /*! - * Min-abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Add minAbstract(std::set const& metaVariables) const; - - /*! - * Max-abstracts from the given meta variables. - * - * @param metaVariables The meta variables from which to abstract. - */ - Add maxAbstract(std::set const& metaVariables) const; - - /*! - * Checks whether the current and the given ADD represent the same function modulo some given precision. - * - * @param other The ADD with which to compare. - * @param precision An upper bound on the maximal difference between any two function values that is to be - * tolerated. - * @param relative If set to true, not the absolute values have to be within the precision, but the relative - * values. - */ - bool equalModuloPrecision(Add const& other, double precision, bool relative = true) const; - - /*! - * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have - * the same number of underlying ADD variables. - * - * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. - * @return The resulting ADD. - */ - Add swapVariables(std::vector> const& metaVariablePairs) const; - - /*! - * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta - * variables. - * - * @param otherMatrix The matrix with which to multiply. - * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- - * matrix multiplication. - * @return An ADD representing the result of the matrix-matrix multiplication. - */ - Add multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const; - - /*! - * Computes a BDD that represents the function in which all assignments with a function value strictly - * larger than the given value are mapped to one and all others to zero. - * - * @param value The value used for the comparison. - * @return The resulting BDD. - */ - Bdd greater(double value) const; - - /*! - * Computes a BDD that represents the function in which all assignments with a function value larger or equal - * to the given value are mapped to one and all others to zero. - * - * @param value The value used for the comparison. - * @return The resulting BDD. - */ - Bdd greaterOrEqual(double value) const; - - /*! - * Computes a BDD that represents the function in which all assignments with a function value strictly - * lower than the given value are mapped to one and all others to zero. - * - * @param value The value used for the comparison. - * @return The resulting BDD. - */ - Bdd less(double value) const; - - /*! - * Computes a BDD that represents the function in which all assignments with a function value less or equal - * to the given value are mapped to one and all others to zero. - * - * @param value The value used for the comparison. - * @return The resulting BDD. - */ - Bdd lessOrEqual(double value) const; - - /*! - * Computes a BDD that represents the function in which all assignments with a function value unequal to - * zero are mapped to one and all others to zero. - * - * @return The resulting DD. - */ - Bdd notZero() const; - - /*! - * Computes the constraint of the current ADD with the given constraint. That is, the function value of the - * resulting ADD will be the same as the current ones for all assignments mapping to one in the constraint - * and may be different otherwise. - * - * @param constraint The constraint to use for the operation. - * @return The resulting ADD. - */ - Add constrain(Add const& constraint) const; - - /*! - * Computes the restriction of the current ADD with the given constraint. That is, the function value of the - * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint - * and may be different otherwise. - * - * @param constraint The constraint to use for the operation. - * @return The resulting ADD. - */ - Add restrict(Add const& constraint) const; - - /*! - * Retrieves the support of the current ADD. - * - * @return The support represented as a BDD. - */ - Bdd getSupport() const override; - - /*! - * Retrieves the number of encodings that are mapped to a non-zero value. - * - * @return The number of encodings that are mapped to a non-zero value. - */ - virtual uint_fast64_t getNonZeroCount() const override; - - /*! - * Retrieves the number of leaves of the ADD. - * - * @return The number of leaves of the ADD. - */ - virtual uint_fast64_t getLeafCount() const override; - - /*! - * Retrieves the number of nodes necessary to represent the DD. - * - * @return The number of nodes in this DD. - */ - virtual uint_fast64_t getNodeCount() const override; - - /*! - * Retrieves the lowest function value of any encoding. - * - * @return The lowest function value of any encoding. - */ - double getMin() const; - - /*! - * Retrieves the highest function value of any encoding. - * - * @return The highest function value of any encoding. - */ - double getMax() const; - - /*! - * Sets the function values of all encodings that have the given value of the meta variable to the given - * target value. - * - * @param metaVariable The meta variable that has to be equal to the given value. - * @param variableValue The value that the meta variable is supposed to have. This must be within the range - * of the meta variable. - * @param targetValue The new function value of the modified encodings. - */ - void setValue(storm::expressions::Variable const& metaVariable, int_fast64_t variableValue, double targetValue); - - /*! - * Sets the function values of all encodings that have the given values of the two meta variables to the - * given target value. - * - * @param metaVariable1 The first meta variable that has to be equal to the first given - * value. - * @param variableValue1 The value that the first meta variable is supposed to have. This must be within the - * range of the meta variable. - * @param metaVariable2 The second meta variable that has to be equal to the second given - * value. - * @param variableValue2 The value that the second meta variable is supposed to have. This must be within - * the range of the meta variable. - * @param targetValue The new function value of the modified encodings. - */ - void setValue(storm::expressions::Variable const& metaVariable1, int_fast64_t variableValue1, storm::expressions::Variable const& metaVariable2, int_fast64_t variableValue2, double targetValue); - - /*! - * Sets the function values of all encodings that have the given values of the given meta variables to the - * given target value. - * - * @param metaVariableToValueMap A mapping of meta variables to the values they are supposed to have. All - * values must be within the range of the respective meta variable. - * @param targetValue The new function value of the modified encodings. - */ - void setValue(std::map const& metaVariableToValueMap = std::map(), double targetValue = 0); - - /*! - * Retrieves the value of the function when all meta variables are assigned the values of the given mapping. - * Note that the mapping must specify values for all meta variables contained in the DD. - * - * @param metaVariableToValueMap A mapping of meta variables to their values. - * @return The value of the function evaluated with the given input. - */ - double getValue(std::map const& metaVariableToValueMap = std::map()) const; - - /*! - * Retrieves whether this ADD represents the constant one function. - * - * @return True if this ADD represents the constant one function. - */ - bool isOne() const; - - /*! - * Retrieves whether this ADD represents the constant zero function. - * - * @return True if this ADD represents the constant zero function. - */ - bool isZero() const; - - /*! - * Retrieves whether this ADD represents a constant function. - * - * @return True if this ADD represents a constants function. - */ - bool isConstant() const; - - /*! - * Retrieves the index of the topmost variable in the DD. - * - * @return The index of the topmost variable in DD. - */ - virtual uint_fast64_t getIndex() const override; - - /*! - * Converts the ADD to a vector. - * - * @return The vector that is represented by this ADD. - */ - template - std::vector toVector() const; - - /*! - * Converts the ADD to a vector. The given offset-labeled DD is used to determine the correct row of - * each entry. - * - * @param rowOdd The ODD used for determining the correct row. - * @return The vector that is represented by this ADD. - */ - template - std::vector toVector(storm::dd::Odd const& rowOdd) const; - - /*! - * Converts the ADD to a row-grouped vector. The given offset-labeled DD is used to determine the correct - * row group of each entry. Note that the group meta variables are assumed to be at the very top in the - * variable ordering. - * - * @param groupMetaVariables The meta variables responsible for the row-grouping. - * @param rowOdd The ODD used for determining the correct row. - * @return The vector that is represented by this ADD. - */ - template - std::vector toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector groupOffsets) const; - - /*! - * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the - * row, whereas all primed variables are assumed to encode the column. - * - * @return The matrix that is represented by this ADD. - */ - storm::storage::SparseMatrix toMatrix() const; - - /*! - * Converts the ADD to a (sparse) double matrix. All contained non-primed variables are assumed to encode the - * row, whereas all primed variables are assumed to encode the column. The given offset-labeled DDs are used - * to determine the correct row and column, respectively, for each entry. - * - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this ADD. - */ - storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Converts the ADD to a (sparse) double matrix. The given offset-labeled DDs are used to determine the - * correct row and column, respectively, for each entry. - * - * @param rowMetaVariables The meta variables that encode the rows of the matrix. - * @param columnMetaVariables The meta variables that encode the columns of the matrix. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this ADD. - */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to - * determine the correct row and column, respectively, for each entry. Note: this function assumes that - * the meta variables used to distinguish different row groups are at the very top of the ADD. - * - * @param groupMetaVariables The meta variables that are used to distinguish different row groups. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this ADD. - */ - storm::storage::SparseMatrix toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to a row-grouped vector. - * The given offset-labeled DDs are used to determine the correct row and column, respectively, for each - * entry. Note: this function assumes that the meta variables used to distinguish different row groups are - * at the very top of the ADD. - * - * @param vector The symbolic vector to convert. - * @param rowGroupSizes A vector specifying the sizes of the row groups. - * @param groupMetaVariables The meta variables that are used to distinguish different row groups. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this ADD. - */ - std::pair, std::vector> toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Exports the DD to the given file in the dot format. - * - * @param filename The name of the file to which the DD is to be exported. - */ - void exportToDot(std::string const& filename = "") const override; - - /*! - * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. - * - * @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. - * @return An iterator that points to the first meta variable assignment with a non-zero function value. - */ - DdForwardIterator begin(bool enumerateDontCareMetaVariables = true) const; - - /*! - * Retrieves an iterator that points past the end of the container. - * - * @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. - * @return An iterator that points past the end of the container. - */ - DdForwardIterator end(bool enumerateDontCareMetaVariables = true) const; - - friend std::ostream & operator<<(std::ostream& out, const Add& add); - - /*! - * Converts the ADD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as - * a call to notZero(). - * - * @return The corresponding BDD. - */ - Bdd toBdd() const; - - private: - - /*! - * Retrieves the CUDD ADD object associated with this ADD. - * - * @return The CUDD ADD object associated with this ADD. - */ - ADD getCuddAdd() const; - - /*! - * Retrieves the raw DD node of CUDD associated with this ADD. - * - * @return The DD node of CUDD associated with this ADD. - */ - DdNode* getCuddDdNode() const; - - /*! - * Creates an ADD that encapsulates the given CUDD ADD. - * - * @param ddManager The manager responsible for this DD. - * @param cuddAdd The CUDD ADD to store. - * @param containedMetaVariables The meta variables that appear in the DD. - */ - Add(std::shared_ptr const> ddManager, ADD cuddAdd, std::set const& containedMetaVariables = std::set()); - - /*! - * Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also - * translated to an explicit row-grouped vector with the same row-grouping. The given offset-labeled DDs - * are used to determine the correct row and column, respectively, for each entry. Note: this function - * assumes that the meta variables used to distinguish different row groups are at the very top of the ADD. - * - * @param rowMetaVariables The meta variables that encode the rows of the matrix. - * @param columnMetaVariables The meta variables that encode the columns of the matrix. - * @param groupMetaVariables The meta variables that are used to distinguish different row groups. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector - * (if it was given). - */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to an equally row-grouped - * explicit vector. The given offset-labeled DDs are used to determine the correct row and column, - * respectively, for each entry. Note: this function assumes that the meta variables used to distinguish - * different row groups are at the very top of the ADD. - * - * @param vector The vector that is to be transformed to an equally grouped explicit vector. - * @param rowGroupSizes A vector specifying the sizes of the row groups. - * @param rowMetaVariables The meta variables that encode the rows of the matrix. - * @param columnMetaVariables The meta variables that encode the columns of the matrix. - * @param groupMetaVariables The meta variables that are used to distinguish different row groups. - * @param rowOdd The ODD used for determining the correct row. - * @param columnOdd The ODD used for determining the correct column. - * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector - * (if it was given). - */ - std::pair,std::vector> toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - - /*! - * Helper function to convert the DD into a (sparse) matrix. - * - * @param dd The DD to convert. - * @param rowIndications A vector indicating at which position in the columnsAndValues vector the entries - * of row i start. Note: this vector is modified in the computation. More concretely, each entry i in the - * vector will be increased by the number of entries in the row. This can be used to count the number - * of entries in each row. If the values are not to be modified, a copy needs to be provided or the entries - * need to be restored afterwards. - * @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful - * completion. - * @param rowGroupOffsets The row offsets at which a given row group starts. - * @param rowOdd The ODD used for the row translation. - * @param columnOdd The ODD used for the column translation. - * @param currentRowLevel The currently considered row level in the DD. - * @param currentColumnLevel The currently considered row level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param currentRowOffset The current row offset. - * @param currentColumnOffset The current row offset. - * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. - * @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered. - * @param generateValues If set to true, the vector columnsAndValues is filled with the actual entries, which - * only works if the offsets given in rowIndications are already correct. If they need to be computed first, - * this flag needs to be false. - */ - void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues = true) const; - - /*! - * Helper function to convert the DD into an (explicit) vector. - * - * @param dd The DD to convert. - * @param result The vector that will hold the values upon successful completion. - * @param rowGroupOffsets The row offsets at which a given row group starts. - * @param rowOdd The ODD used for the row translation. - * @param currentRowLevel The currently considered row level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param currentRowOffset The current row offset. - * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. - */ - template - void toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; - - /*! - * Splits the given matrix DD into the groups using the given group variables. - * - * @param dd The DD to split. - * @param groups A vector that is to be filled with the DDs for the individual groups. - * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. - * @param currentLevel The currently considered level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. - */ - void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; - - /*! - * Splits the given matrix and vector DDs into the groups using the given group variables. - * - * @param dd1 The matrix DD to split. - * @param dd2 The vector DD to split. - * @param groups A vector that is to be filled with the pairs of matrix/vector DDs for the individual groups. - * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. - * @param currentLevel The currently considered level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param remainingMetaVariables1 The meta variables that remain in the matrix DD after the groups have been split. - * @param remainingMetaVariables2 The meta variables that remain in the vector DD after the groups have been split. - */ - void splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, Add>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables1, std::set const& remainingMetaVariables2) const; - - /*! - * Adds the current (DD-based) vector to the given explicit one. - * - * @param odd The ODD used for the translation. - * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. - * @param targetVector The vector to which the translated DD-based vector is to be added. - */ - template - void addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; - - /*! - * Performs a recursive step to perform the given function between the given DD-based vector and the given - * explicit vector. - * - * @param dd The DD to add to the explicit vector. - * @param currentLevel The currently considered level in the DD. - * @param maxLevel The number of levels that need to be considered. - * @param currentOffset The current offset. - * @param odd The ODD used for the translation. - * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. - * @param targetVector The vector to which the translated DD-based vector is to be added. - */ - template - void modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; - - /*! - * Builds an ADD representing the given vector. - * - * @param ddManager The manager responsible for the ADD. - * @param values The vector that is to be represented by the ADD. - * @param odd The ODD used for the translation. - * @param metaVariables The meta variables used for the translation. - * @return The resulting (CUDD) ADD. - */ - template - static ADD fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); - - /*! - * Builds an ADD representing the given vector. - * - * @param manager The manager responsible for the ADD. - * @param currentOffset The current offset in the vector. - * @param currentLevel The current level in the DD. - * @param maxLevel The maximal level in the DD. - * @param values The vector that is to be represented by the ADD. - * @param odd The ODD used for the translation. - * @param ddVariableIndices The (sorted) list of DD variable indices to use. - * @return The resulting (CUDD) ADD node. - */ - template - static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices); - - // The ADD created by CUDD. - ADD cuddAdd; - }; - } -} - -#endif /* STORM_STORAGE_DD_CUDDADD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDdForwardIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp similarity index 77% rename from src/storage/dd/cudd/CuddDdForwardIterator.cpp rename to src/storage/dd/cudd/CuddAddIterator.cpp index 5401bccfa..e19d9396e 100644 --- a/src/storage/dd/cudd/CuddDdForwardIterator.cpp +++ b/src/storage/dd/cudd/CuddAddIterator.cpp @@ -1,4 +1,4 @@ -#include "src/storage/dd/cudd/CuddDdForwardIterator.h" +#include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/storage/dd/cudd/CuddDdManager.h" #include "src/storage/dd/DdMetaVariable.h" #include "src/utility/macros.h" @@ -6,11 +6,13 @@ namespace storm { namespace dd { - DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { + template + AddIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { // Intentionally left empty. } - DdForwardIterator::DdForwardIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { + template + AddIterator::DdForwardIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set 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) { @@ -19,13 +21,15 @@ namespace storm { } } - DdForwardIterator::DdForwardIterator(DdForwardIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { + template + AddIterator::DdForwardIterator(AddIterator&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { // Null-out the pointers of which we took possession. other.cube = nullptr; other.generator = nullptr; } - DdForwardIterator& DdForwardIterator::operator=(DdForwardIterator&& other) { + template + AddIterator& AddIterator::operator=(AddIterator&& other) { if (this != &other) { this->ddManager = other.ddManager; this->generator = other.generator; @@ -44,7 +48,8 @@ namespace storm { return *this; } - DdForwardIterator::~DdForwardIterator() { + template + AddIterator::~DdForwardIterator() { // We free the pointers sind Cudd allocates them using malloc rather than new/delete. if (this->cube != nullptr) { free(this->cube); @@ -54,7 +59,8 @@ namespace storm { } } - DdForwardIterator& DdForwardIterator::operator++() { + template + AddIterator& AddIterator::operator++() { STORM_LOG_ASSERT(!this->isAtEnd, "Illegally incrementing iterator that is already at its end."); // If there were no (relevant) don't cares or we have enumerated all combination, we need to eliminate the @@ -76,7 +82,8 @@ namespace storm { return *this; } - void DdForwardIterator::treatNextInCube() { + template + void AddIterator::treatNextInCube() { // Start by increasing the counter and check which bits we need to set/unset in the new valuation. ++this->cubeCounter; @@ -99,7 +106,8 @@ namespace storm { } } - void DdForwardIterator::treatNewCube() { + template + void AddIterator::treatNewCube() { this->relevantDontCareDdVariables.clear(); // Now loop through the bits of all meta variables and check whether they need to be set, not set or are @@ -150,7 +158,8 @@ namespace storm { this->cubeCounter = 0; } - bool DdForwardIterator::operator==(DdForwardIterator const& other) const { + template + bool AddIterator::operator==(AddIterator const& other) const { if (this->isAtEnd && other.isAtEnd) { return true; } else { @@ -162,12 +171,16 @@ namespace storm { } } - bool DdForwardIterator::operator!=(DdForwardIterator const& other) const { + template + bool AddIterator::operator!=(AddIterator const& other) const { return !(*this == other); } - std::pair DdForwardIterator::operator*() const { + template + std::pair AddIterator::operator*() const { return std::make_pair(currentValuation, value); } + + template class AddIterator; } } \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDdForwardIterator.h b/src/storage/dd/cudd/CuddAddIterator.h similarity index 81% rename from src/storage/dd/cudd/CuddDdForwardIterator.h rename to src/storage/dd/cudd/CuddAddIterator.h index e6498458d..c5790c372 100644 --- a/src/storage/dd/cudd/CuddDdForwardIterator.h +++ b/src/storage/dd/cudd/CuddAddIterator.h @@ -1,5 +1,5 @@ -#ifndef STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ -#define STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ +#ifndef STORM_STORAGE_DD_CUDDAddIterator_H_ +#define STORM_STORAGE_DD_CUDDAddIterator_H_ #include #include @@ -7,7 +7,7 @@ #include #include -#include "src/storage/dd/DdForwardIterator.h" +#include "src/storage/dd/AddIterator.h" #include "src/storage/expressions/SimpleValuation.h" // Include the C++-interface of CUDD. @@ -19,31 +19,31 @@ namespace storm { template class DdManager; template class Add; - template<> - class DdForwardIterator { + template + class AddIterator { public: friend class Add; // Default-instantiate the constructor. - DdForwardIterator(); + AddIterator(); // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then. - DdForwardIterator(DdForwardIterator const& other) = delete; - DdForwardIterator& operator=(DdForwardIterator const& other) = delete; + AddIterator(AddIterator const& other) = delete; + AddIterator& operator=(AddIterator const& other) = delete; // Provide move-construction and move-assignment, though. - DdForwardIterator(DdForwardIterator&& other); - DdForwardIterator& operator=(DdForwardIterator&& other); + AddIterator(AddIterator&& other); + AddIterator& operator=(AddIterator&& other); /*! * Destroys the forward iterator and frees the generator as well as the cube if they are not the nullptr. */ - ~DdForwardIterator(); + ~AddIterator(); /*! * Moves the iterator one position forward. */ - DdForwardIterator& operator++(); + AddIterator& operator++(); /*! * Returns a pair consisting of a valuation of meta variables and the value to which this valuation is @@ -60,7 +60,7 @@ namespace storm { * @param other The iterator with which to compare. * @return True if the two iterators are considered equal. */ - bool operator==(DdForwardIterator const& other) const; + bool operator==(AddIterator const& other) const; /*! * Compares the iterator with the given one. Two iterators are considered unequal iff they are not @@ -69,7 +69,7 @@ namespace storm { * @param other The iterator with which to compare. * @return True if the two iterators are considered unequal. */ - bool operator!=(DdForwardIterator const& other) const; + bool operator!=(AddIterator const& other) const; private: /*! @@ -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 const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); + AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); /*! * Recreates the internal information when a new cube needs to be treated. @@ -133,4 +133,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_CUDDAddIterator_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddOdd.h b/src/storage/dd/cudd/CuddOdd.h index d39fa2a8b..3a9e65883 100644 --- a/src/storage/dd/cudd/CuddOdd.h +++ b/src/storage/dd/cudd/CuddOdd.h @@ -5,7 +5,7 @@ #include #include "src/storage/dd/Odd.h" -#include "src/storage/dd/cudd/CuddAdd.h" +#include "src/storage/dd/Add.h" #include "src/utility/OsDetection.h" // Include the C++-interface of CUDD. diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index e69de29bb..6cccf9d67 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -0,0 +1,757 @@ +#include "src/storage/dd/cudd/InternalCuddAdd.h" + +#include "src/storage/dd/cudd/CuddOdd.h" + +#include "src/storage/dd/cudd/InternalCuddDdManager.h" +#include "src/storage/dd/cudd/InternalCuddBdd.h" + +#include "src/storage/SparseMatrix.h" + +#include "src/utility/constants.h" + +namespace storm { + namespace dd { + template + bool InternalAdd::operator==(InternalAdd const& other) const { + return this->getCuddAdd() == other.getCuddAdd(); + } + + template + bool InternalAdd::operator!=(InternalAdd const& other) const { + return !(*this == other); + } + + template + InternalAdd InternalAdd::ite(InternalAdd const& thenDd, InternalAdd const& elseDd) const { + return InternalAdd(ddManager, this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd())); + } + + template + InternalAdd InternalAdd::operator!() const { + return InternalAdd(ddManager, ~this->getCuddAdd()); + } + + template + InternalAdd InternalAdd::operator||(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd() | other.getCuddAdd()); + } + + template + InternalAdd& InternalAdd::operator|=(InternalAdd const& other) { + this->cuddAdd = this->getCuddAdd() | other.getCuddAdd(); + } + + template + InternalAdd InternalAdd::operator+(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd() + other.getCuddAdd()); + } + + template + InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { + this->cuddAdd = this->getCuddAdd() + other.getCuddAdd(); + } + + template + InternalAdd InternalAdd::operator*(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd() * other.getCuddAdd()); + } + + template + InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { + this->cuddAdd = this->getCuddAdd() * other.getCuddAdd(); + } + + template + InternalAdd InternalAdd::operator-(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd() - other.getCuddAdd()); + } + + template + InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { + this->cuddAdd = this->getCuddAdd() - other.getCuddAdd(); + } + + template + InternalAdd InternalAdd::operator/(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd() / other.getCuddAdd()); + } + + template + InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + this->cuddAdd = this->getCuddAdd() / other.getCuddAdd(); + } + + template + InternalAdd InternalAdd::equals(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().Equals(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::notEquals(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().NotEquals(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::less(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().LessThan(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().LessThanOrEqual(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::greater(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().GreaterThan(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::pow(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().Pow(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::mod(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().Mod(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().LogXY(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::floor() const { + return InternalAdd(ddManager, this->getCuddAdd().Floor()); + } + + template + InternalAdd InternalAdd::ceil() const { + return InternalAdd(ddManager, this->getCuddAdd().Ceil()); + } + + template + InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().Minimum(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + return InternalAdd(ddManager, this->getCuddAdd().Maximum(other.getCuddAdd())); + } + + template + InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->getCuddAdd().ExistAbstract(cube.getCuddBdd())); + } + + template + InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->getCuddAdd().MinAbstract(cube.getCuddBdd())); + } + + template + InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->getCuddAdd().MaxAbstract(cube.getCuddBdd())); + } + + template + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { + if (relative) { + return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); + } else { + return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); + } + }; + + template + InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { + std::vector fromAdd; + std::vector toAdd; + for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { + fromAdd.push_back(it1->getCuddAdd()); + toAdd.push_back(it2->getCuddAdd()); + } + return InternalBdd(ddManager, this->getCuddBdd().SwapVariables(fromAdd, toAdd)); + } + + template + InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + // Create the CUDD summation variables. + std::vector summationAdds; + for (auto const& ddVariable : summationDdVariables) { + summationAdds.push_back(ddVariable.toAdd().getCuddAdd()); + } + + return InternalAdd(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds)); + } + + template + InternalBdd InternalAdd::greater(ValueType const& value) const { + return InternalBdd(ddManager, this->getCuddAdd().BddStrictThreshold(value)); + } + + template + InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { + return InternalBdd(ddManager, this->getCuddAdd().BddThreshold(value)); + } + + template + InternalBdd InternalAdd::less(ValueType const& value) const { + return InternalBdd(ddManager, ~this->getCuddAdd().BddThreshold(value)); + } + + template + InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { + return InternalBdd(ddManager, ~this->getCuddAdd().BddStrictThreshold(value)); + } + + template + InternalBdd InternalAdd::notZero() const { + return this->toBdd(); + } + + template + InternalAdd InternalAdd::constrain(InternalAdd const& constraint) const { + return InternalAdd(ddManager, this->getCuddAdd().Constrain(constraint.getCuddAdd())); + } + + template + InternalAdd InternalAdd::restrict(InternalAdd const& constraint) const { + return InternalAdd(ddManager, this->getCuddAdd().Restrict(constraint.getCuddAdd())); + } + + template + InternalBdd InternalAdd::getSupport() const { + return InternalBdd(ddManager, this->getCuddAdd().Support()); + } + + template + uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + return static_cast(this->getCuddAdd().CountMinterm(static_cast(numberOfDdVariables))); + } + + template + uint_fast64_t InternalAdd::getLeafCount() const { + return static_cast(this->getCuddAdd().CountLeaves()); + } + + template + uint_fast64_t InternalAdd::getNodeCount() const { + return static_cast(this->getCuddAdd().nodeCount()); + } + + template + ValueType InternalAdd::getMin() const { + ADD constantMinAdd = this->getCuddAdd().FindMin(); + return static_cast(Cudd_V(constantMinAdd.getNode())); + } + + template + ValueType InternalAdd::getMax() const { + ADD constantMaxAdd = this->getCuddAdd().FindMax(); + return static_cast(Cudd_V(constantMaxAdd.getNode())); + } + + template + InternalBdd InternalAdd::toBdd() const { + return InternalBdd(ddManager, this->getCuddAdd().BddPattern()); + } + + template + bool InternalAdd::isOne() const { + return this->getCuddAdd().IsOne(); + } + + template + bool InternalAdd::isZero() const { + return this->getCuddAdd().IsZero(); + } + + template + bool InternalAdd::isConstant() const { + return Cudd_IsConstant(this->getCuddAdd().getNode()); + } + + template + uint_fast64_t InternalAdd::getIndex() const { + return static_cast(this->getCuddAdd().NodeReadIndex()); + } + + template + void InternalAdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { + // Build the name input of the DD. + std::vector ddNames; + std::string ddName("f"); + ddNames.push_back(new char[ddName.size() + 1]); + std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); + + // Now build the variables names. + std::vector ddVariableNames; + for (auto const& element : ddVariableNamesAsStrings) { + ddVariableNames.push_back(new char[element.size() + 1]); + std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); + } + + // Open the file, dump the DD and close it again. + FILE* filePointer = fopen(filename.c_str() , "w"); + std::vector cuddAddVector = { this->getCuddAdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); + fclose(filePointer); + + // Finally, delete the names. + for (char* element : ddNames) { + delete[] element; + } + for (char* element : ddVariableNames) { + delete[] element; + } + } + + template + AddIterator InternalAdd::begin(std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + int* cube; + double value; + DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); + return AddIterator(ddManager, generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &metaVariables, enumerateDontCareMetaVariables); + } + + template + AddIterator InternalAdd::end(bool enumerateDontCareMetaVariables) const { + return AddIterator(ddManager, nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); + } + + template + ADD InternalAdd::getCuddAdd() const { + return this->cuddAdd; + } + + template + DdNode* InternalAdd::getCuddDdNode() const { + return this->getCuddAdd().getNode(); + } + + template + std::vector InternalAdd::toVector(std::vector const& ddGroupVariableIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, std::vector const& groupOffsets) const { + // Start by splitting the symbolic vector into groups. + std::vector> groups; + splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + + // Now iterate over the groups and add them to the resulting vector. + std::vector result(groupOffsets.back(), storm::utility::zero()); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + toVectorRec(groups[i].getCuddDdNode(), result, groupOffsets, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); + } + + return result; + } + + template + void InternalAdd::addToExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { + composeVector(odd, ddVariableIndices, targetVector, std::plus()); + } + + template + void InternalAdd::composeVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + composeVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, function); + } + + template + void InternalAdd::composeVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { + // For the empty DD, we do not need to add any entries. + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentLevel == maxLevel) { + targetVector[currentOffset] = function(targetVector[currentOffset], Cudd_V(dd)); + } else if (ddVariableIndices[currentLevel] < dd->index) { + // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set + // and for the one in which it is not set. + composeVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + } else { + // Otherwise, we simply recursively call the function for both (different) cases. + composeVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + composeVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); + } + } + + template + void InternalAdd::toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { + // For the empty DD, we do not need to add any entries. + if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentRowLevel == maxLevel) { + result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); + } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { + toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); + toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); + } else { + toVectorRec(Cudd_E(dd), result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); + toVectorRec(Cudd_T(dd), result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); + } + } + + template + storm::storage::SparseMatrix InternalAdd::toMatrix(storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) const { + // Prepare the vectors that represent the matrix. + std::vector rowIndications(rowOdd.getTotalOffset() + 1); + std::vector> columnsAndValues(this->getNonZeroCount()); + + // Create a trivial row grouping. + std::vector trivialRowGroupIndices(rowIndications.size()); + uint_fast64_t i = 0; + for (auto& entry : trivialRowGroupIndices) { + entry = i; + ++i; + } + + // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent + // it from actually generating the entries in the entry vector. + toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + + // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert + // the resulting (DD) vector to an explicit vector. + + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { + tmp2 = rowIndications[i]; + rowIndications[i] = rowIndications[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowIndications[0] = 0; + + // Now actually fill the entry vector. + toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. + for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { + rowIndications[i] = rowIndications[i - 1]; + } + rowIndications[0] = 0; + + // Construct matrix and return result. + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(trivialRowGroupIndices), false); + } + + template + void InternalAdd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { + // For the empty DD, we do not need to add any entries. + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentRowLevel + currentColumnLevel == maxLevel) { + if (generateValues) { + columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); + } + ++rowIndications[rowGroupOffsets[currentRowOffset]]; + } else { + DdNode const* elseElse; + DdNode const* elseThen; + DdNode const* thenElse; + DdNode const* thenThen; + + if (ddColumnVariableIndices[currentColumnLevel] < dd->index) { + elseElse = elseThen = thenElse = thenThen = dd; + } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) { + elseElse = thenElse = Cudd_E(dd); + elseThen = thenThen = Cudd_T(dd); + } else { + DdNode const* elseNode = Cudd_E(dd); + if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) { + elseElse = elseThen = elseNode; + } else { + elseElse = Cudd_E(elseNode); + elseThen = Cudd_T(elseNode); + } + + DdNode const* thenNode = Cudd_T(dd); + if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) { + thenElse = thenThen = thenNode; + } else { + thenElse = Cudd_E(thenNode); + thenThen = Cudd_T(thenNode); + } + } + + // Visit else-else. + toMatrixRec(elseElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit else-then. + toMatrixRec(elseThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit then-else. + toMatrixRec(thenElse, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset, ddRowVariableIndices, ddColumnVariableIndices, generateValues); + // Visit then-then. + toMatrixRec(thenThen, rowIndications, columnsAndValues, rowGroupOffsets, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(), currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues); + } + } + + template + storm::storage::SparseMatrix InternalAdd::toMatrix(std::vector const& ddGroupVariableIndices, InternalBdd const& groupVariableCube, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const { + // Start by computing the offsets (in terms of rows) for each row group. + InternalAdd stateToNumberOfChoices = this->notZero().existsAbstract(columnVariableCube).toAdd().sumAbstract(groupVariableCube); + std::vector rowGroupIndicesAsValueType = stateToNumberOfChoices.toVector(rowOdd); + std::vector rowGroupIndices(rowGroupIndicesAsValueType.size() + 1); + std::transform(rowGroupIndicesAsValueType.begin(), rowGroupIndicesAsValueType.end(), rowGroupIndices.begin(), [] (ValueType const& value) { return static_cast(value); }); + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { + tmp2 = rowGroupIndices[i]; + rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowGroupIndices[0] = 0; + + // Next, we split the matrix into one for each group. This only works if the group variables are at the very + // top. + std::vector> groups; + splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + + // Create the actual storage for the non-zero entries. + std::vector> columnsAndValues(this->getNonZeroCount()); + + // Now compute the indices at which the individual rows start. + std::vector rowIndications(rowGroupIndices.back() + 1); + + std::vector> statesWithGroupEnabled(groups.size()); + InternalAdd stateToRowGroupCount = this->getDdManager()->getAddZero(); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i]; + + toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + + statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnVariableCube).toAdd(); + stateToRowGroupCount += statesWithGroupEnabled[i]; + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; + composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); + + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. + tmp = 0; + tmp2 = 0; + for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { + tmp2 = rowIndications[i]; + rowIndications[i] = rowIndications[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowIndications[0] = 0; + + // Now actually fill the entry vector. + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i]; + + toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); + + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. + for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { + rowIndications[i] = rowIndications[i - 1]; + } + rowIndications[0] = 0; + + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true); + } + + template + std::pair, std::vector> InternalAdd::toMatrixVector(InternalAdd const& vector, std::vector const& ddGroupVariableIndices, std::vector&& rowGroupIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) { + // Transform the row group sizes to the actual row group indices. + rowGroupIndices.resize(rowGroupIndices.size() + 1); + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { + tmp2 = rowGroupIndices[i]; + rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowGroupIndices[0] = 0; + + // Create the explicit vector we need to fill later. + std::vector explicitVector(rowGroupIndices.back()); + + // Next, we split the matrix into one for each group. This only works if the group variables are at the very top. + std::vector, InternalAdd>> groups; + splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + + // Create the actual storage for the non-zero entries. + std::vector> columnsAndValues(this->getNonZeroCount()); + + // Now compute the indices at which the individual rows start. + std::vector rowIndications(rowGroupIndices.back() + 1); + + std::vector> statesWithGroupEnabled(groups.size()); + storm::dd::InternalAdd stateToRowGroupCount = this->getDdManager()->getAddZero(); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + std::pair, storm::dd::InternalAdd> ddPair = groups[i]; + + toMatrixRec(ddPair.first.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + toVectorRec(ddPair.second.getCuddDdNode(), explicitVector, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); + + statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnVariableCube) || ddPair.second.notZero()).toAdd(); + stateToRowGroupCount += statesWithGroupEnabled[i]; + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; + composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); + + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. + tmp = 0; + tmp2 = 0; + for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { + tmp2 = rowIndications[i]; + rowIndications[i] = rowIndications[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowIndications[0] = 0; + + // Now actually fill the entry vector. + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i].first; + + toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + composeVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); + + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. + for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { + rowIndications[i] = rowIndications[i - 1]; + } + rowIndications[0] = 0; + + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), true), std::move(explicitVector)); + } + + template + void InternalAdd::splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { + // For the empty DD, we do not need to create a group. + if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd))); + } else if (ddGroupVariableIndices[currentLevel] < dd->index) { + splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } else { + splitGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } + + template + void InternalAdd::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { + // For the empty DD, we do not need to create a group. + if (dd1 == Cudd_ReadZero(ddManager->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(ddManager->getCuddManager().getManager())) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(std::make_pair(InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd1)), + InternalAdd(ddManager, ADD(ddManager->getCuddManager(), dd2)))); + } else if (ddGroupVariableIndices[currentLevel] < dd1->index) { + if (ddGroupVariableIndices[currentLevel] < dd2->index) { + splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } else { + splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } else if (ddGroupVariableIndices[currentLevel] < dd2->index) { + splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } else { + splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } + + template + InternalAdd InternalAdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices) { + uint_fast64_t offset = 0; + return InternalAdd(ddManager, ADD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices))); + } + + template + DdNode* InternalAdd::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices) { + if (currentLevel == maxLevel) { + // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one + // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we + // need to copy the next value of the vector iff the then-offset is greater than zero. + if (odd.getThenOffset() > 0) { + return Cudd_addConst(manager, values[currentOffset++]); + } else { + return Cudd_ReadZero(manager); + } + } else { + // If the total offset is zero, we can just return the constant zero DD. + if (odd.getThenOffset() + odd.getElseOffset() == 0) { + return Cudd_ReadZero(manager); + } + + // Determine the new else-successor. + DdNode* elseSuccessor = nullptr; + if (odd.getElseOffset() > 0) { + elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices); + } else { + elseSuccessor = Cudd_ReadZero(manager); + } + Cudd_Ref(elseSuccessor); + + // Determine the new then-successor. + DdNode* thenSuccessor = nullptr; + if (odd.getThenOffset() > 0) { + thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices); + } else { + thenSuccessor = Cudd_ReadZero(manager); + } + Cudd_Ref(thenSuccessor); + + // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor); + DdNode* result = Cudd_addIthVar(manager, static_cast(ddVariableIndices[currentLevel])); + Cudd_Ref(result); + DdNode* newResult = Cudd_addIte(manager, result, thenSuccessor, elseSuccessor); + Cudd_Ref(newResult); + + // Dispose of the intermediate results + Cudd_RecursiveDeref(manager, result); + Cudd_RecursiveDeref(manager, thenSuccessor); + Cudd_RecursiveDeref(manager, elseSuccessor); + + // Before returning, we remove the protection imposed by the previous call to Cudd_Ref. + Cudd_Deref(newResult); + + return newResult; + } + } + + template class InternalAdd; + } +} \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index fa754584a..a86ff5776 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -6,24 +6,37 @@ #include "src/storage/dd/DdType.h" #include "src/storage/dd/InternalAdd.h" +#include "src/storage/expressions/Variable.h" + // Include the C++-interface of CUDD. #include "cuddObj.hh" namespace storm { namespace storage { - template class SparseMatrix; + template + class SparseMatrix; + class BitVector; - template class MatrixEntry; + + template + class MatrixEntry; } namespace dd { - // Forward-declare some classes. - template class DdManager; - template class Odd; - template class Bdd; + template + class InternalDdManager; + + template + class InternalBdd; + + template + class AddIterator; + + template + class Odd; template - class InternalAdd : public Dd { + class InternalAdd { public: /*! * Creates an ADD that encapsulates the given CUDD ADD. @@ -32,8 +45,478 @@ namespace storm { * @param cuddAdd The CUDD ADD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Add(InternalDdManager const* ddManager, ADD cuddAdd); + InternalAdd(InternalDdManager const* ddManager, ADD cuddAdd); + + // Instantiate all copy/move constructors/assignments with the default implementation. + InternalAdd() = default; + InternalAdd(InternalAdd const& other) = default; + InternalAdd& operator=(InternalAdd const& other) = default; + InternalAdd(InternalAdd&& other) = default; + InternalAdd& operator=(InternalAdd&& other) = default; + + /*! + * Retrieves whether the two DDs represent the same function. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the same function. + */ + bool operator==(InternalAdd const& other) const; + + /*! + * Retrieves whether the two DDs represent different functions. + * + * @param other The DD that is to be compared with the current one. + * @return True if the DDs represent the different functions. + */ + bool operator!=(InternalAdd const& other) const; + + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + * + * @param thenDd The ADD specifying the 'then' part. + * @param elseDd The ADD specifying the 'else' part. + * @return The ADD corresponding to the if-then-else of the operands. + */ + InternalAdd ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; + + /*! + * Logically inverts the current ADD. That is, all inputs yielding non-zero values will be mapped to zero in + * the result and vice versa. + * + * @return The resulting ADD. + */ + InternalAdd operator!() const; + + /*! + * Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be + * 0/1 ADDs. + * + * @param other The second ADD used for the operation. + * @return The logical or of the operands. + */ + InternalAdd operator||(InternalAdd const& other) const; + + /*! + * Performs a logical or of the current and the given ADD and assigns it to the current ADD. As a + * prerequisite, the operand ADDs need to be 0/1 ADDs. + * + * @param other The second ADD used for the operation. + * @return A reference to the current ADD after the operation + */ + InternalAdd& operator|=(InternalAdd const& other); + + /*! + * Adds the two ADDs. + * + * @param other The ADD to add to the current one. + * @return The result of the addition. + */ + InternalAdd operator+(InternalAdd const& other) const; + + /*! + * Adds the given ADD to the current one. + * + * @param other The ADD to add to the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator+=(InternalAdd const& other); + + /*! + * Multiplies the two ADDs. + * + * @param other The ADD to multiply with the current one. + * @return The result of the multiplication. + */ + InternalAdd operator*(InternalAdd const& other) const; + + /*! + * Multiplies the given ADD with the current one and assigns the result to the current ADD. + * + * @param other The ADD to multiply with the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator*=(InternalAdd const& other); + + /*! + * Subtracts the given ADD from the current one. + * + * @param other The ADD to subtract from the current one. + * @return The result of the subtraction. + */ + InternalAdd operator-(InternalAdd const& other) const; + + /*! + * Subtracts the given ADD from the current one and assigns the result to the current ADD. + * + * @param other The ADD to subtract from the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator-=(InternalAdd const& other); + + /*! + * Divides the current ADD by the given one. + * + * @param other The ADD by which to divide the current one. + * @return The result of the division. + */ + InternalAdd operator/(InternalAdd const& other) const; + + /*! + * Divides the current ADD by the given one and assigns the result to the current ADD. + * + * @param other The ADD by which to divide the current one. + * @return A reference to the current ADD after the operation. + */ + InternalAdd& operator/=(InternalAdd const& other); + + /*! + * Retrieves the function that maps all evaluations to one that have identical function values. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd equals(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one that have distinct function values. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd notEquals(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less + * than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd less(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are less or + * equal than the one in the given ADD. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd lessOrEqual(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd greater(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to one whose function value in the first ADD are greater + * or equal than the one in the given ADD. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd greaterOrEqual(InternalAdd const& other) const; + + /*! + * Retrieves the function that represents the current ADD to the power of the given ADD. + * + * @other The exponent function (given as an ADD). + * @retur The resulting ADD. + */ + InternalAdd pow(InternalAdd const& other) const; + + /*! + * Retrieves the function that represents the current ADD modulo the given ADD. + * + * @other The modul function (given as an ADD). + * @retur The resulting ADD. + */ + InternalAdd mod(InternalAdd const& other) const; + + /*! + * Retrieves the function that represents the logarithm of the current ADD to the bases given by the second + * ADD. + * + * @other The base function (given as an ADD). + * @retur The resulting ADD. + */ + InternalAdd logxy(InternalAdd const& other) const; + + /*! + * Retrieves the function that floors all values in the current ADD. + * + * @retur The resulting ADD. + */ + InternalAdd floor() const; + + /*! + * Retrieves the function that ceils all values in the current ADD. + * + * @retur The resulting ADD. + */ + InternalAdd ceil() const; + + /*! + * Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd minimum(InternalAdd const& other) const; + + /*! + * Retrieves the function that maps all evaluations to the maximum of the function values of the two ADDs. + * + * @param other The ADD with which to perform the operation. + * @return The resulting function represented as an ADD. + */ + InternalAdd maximum(InternalAdd const& other) const; + + /*! + * Sum-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + InternalAdd sumAbstract(InternalBdd const& cube) const; + + /*! + * Min-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + InternalAdd minAbstract(InternalBdd const& cube) const; + + /*! + * Max-abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + InternalAdd maxAbstract(InternalBdd const& cube) const; + + /*! + * Checks whether the current and the given ADD represent the same function modulo some given precision. + * + * @param other The ADD with which to compare. + * @param precision An upper bound on the maximal difference between any two function values that is to be + * tolerated. + * @param relative If set to true, not the absolute values have to be within the precision, but the relative + * values. + */ + bool equalModuloPrecision(InternalAdd const& other, double precision, bool relative = true) const; + + /*! + * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have + * the same number of underlying ADD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @return The resulting ADD. + */ + InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; + + /*! + * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta + * variables. + * + * @param otherMatrix The matrix with which to multiply. + * @param summationMetaVariables The names of the meta variables over which to sum during the matrix- + * matrix multiplication. + * @return An ADD representing the result of the matrix-matrix multiplication. + */ + InternalAdd multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value strictly + * larger than the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd greater(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value larger or equal + * to the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd greaterOrEqual(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value strictly + * lower than the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd less(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value less or equal + * to the given value are mapped to one and all others to zero. + * + * @param value The value used for the comparison. + * @return The resulting BDD. + */ + InternalBdd lessOrEqual(ValueType const& value) const; + + /*! + * Computes a BDD that represents the function in which all assignments with a function value unequal to + * zero are mapped to one and all others to zero. + * + * @return The resulting DD. + */ + InternalBdd notZero() const; + + /*! + * Computes the constraint of the current ADD with the given constraint. That is, the function value of the + * resulting ADD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting ADD. + */ + InternalAdd constrain(InternalAdd const& constraint) const; + + /*! + * Computes the restriction of the current ADD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting ADD. + */ + InternalAdd restrict(InternalAdd const& constraint) const; + + /*! + * Retrieves the support of the current ADD. + * + * @return The support represented as a BDD. + */ + InternalBdd getSupport() const; + + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @return The number of encodings that are mapped to a non-zero value. + */ + virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; + + /*! + * Retrieves the number of leaves of the ADD. + * + * @return The number of leaves of the ADD. + */ + virtual uint_fast64_t getLeafCount() const; + + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + virtual uint_fast64_t getNodeCount() const; + + /*! + * Retrieves the lowest function value of any encoding. + * + * @return The lowest function value of any encoding. + */ + ValueType getMin() const; + + /*! + * Retrieves the highest function value of any encoding. + * + * @return The highest function value of any encoding. + */ + ValueType getMax() const; + + /*! + * Converts the ADD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as + * a call to notZero(). + * + * @return The corresponding BDD. + */ + InternalBdd toBdd() const; + + /*! + * Retrieves whether this ADD represents the constant one function. + * + * @return True if this ADD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this ADD represents the constant zero function. + * + * @return True if this ADD represents the constant zero function. + */ + bool isZero() const; + + /*! + * Retrieves whether this ADD represents a constant function. + * + * @return True if this ADD represents a constants function. + */ + bool isConstant() const; + + /*! + * Retrieves the index of the topmost variable in the DD. + * + * @return The index of the topmost variable in DD. + */ + virtual uint_fast64_t getIndex() const; + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + */ + void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const; + + /*! + * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. + * + * @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. + * @return An iterator that points to the first meta variable assignment with a non-zero function value. + */ + AddIterator begin(std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; + + /*! + * Retrieves an iterator that points past the end of the container. + * + * @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. + * @return An iterator that points past the end of the container. + */ + AddIterator end(bool enumerateDontCareMetaVariables = true) const; + + /*! + * Converts the ADD to a vector. The given offset-labeled DD is used to determine the correct row of + * each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @return The vector that is represented by this ADD. + */ + std::vector toVector(std::vector const& ddGroupVariableIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, std::vector const& groupOffsets) const; + + void addToExplicitVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + + void composeVector(storm::dd::Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + + storm::storage::SparseMatrix toMatrix(storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices) const; + + storm::storage::SparseMatrix toMatrix(std::vector const& ddGroupVariableIndices, InternalBdd const& groupVariableCube, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube) const; + + std::pair, std::vector> toMatrixVector(InternalAdd const& vector, std::vector const& ddGroupVariableIndices, std::vector&& rowGroupIndices, storm::dd::Odd const& rowOdd, std::vector const& ddRowVariableIndices, storm::dd::Odd const& columnOdd, std::vector const& ddColumnVariableIndices, InternalBdd const& columnVariableCube); + static InternalAdd fromVector(InternalDdManager const* ddManager, std::vector const& values, storm::dd::Odd const& odd, std::vector const& ddVariableIndices); private: /*! @@ -50,10 +533,105 @@ namespace storm { */ DdNode* getCuddDdNode() const; + /*! + * Performs a recursive step to perform the given function between the given DD-based vector and the given + * explicit vector. + * + * @param dd The DD to add to the explicit vector. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentOffset The current offset. + * @param odd The ODD used for the translation. + * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. + * @param targetVector The vector to which the translated DD-based vector is to be added. + */ + void composeVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + + /*! + * Helper function to convert the DD into an (explicit) vector. + * + * @param dd The DD to convert. + * @param result The vector that will hold the values upon successful completion. + * @param rowGroupOffsets The row offsets at which a given row group starts. + * @param rowOdd The ODD used for the row translation. + * @param currentRowLevel The currently considered row level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentRowOffset The current row offset. + * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. + */ + void toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; + + /*! + * Helper function to convert the DD into a (sparse) matrix. + * + * @param dd The DD to convert. + * @param rowIndications A vector indicating at which position in the columnsAndValues vector the entries + * of row i start. Note: this vector is modified in the computation. More concretely, each entry i in the + * vector will be increased by the number of entries in the row. This can be used to count the number + * of entries in each row. If the values are not to be modified, a copy needs to be provided or the entries + * need to be restored afterwards. + * @param columnsAndValues The vector that will hold the columns and values of non-zero entries upon successful + * completion. + * @param rowGroupOffsets The row offsets at which a given row group starts. + * @param rowOdd The ODD used for the row translation. + * @param columnOdd The ODD used for the column translation. + * @param currentRowLevel The currently considered row level in the DD. + * @param currentColumnLevel The currently considered row level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param currentRowOffset The current row offset. + * @param currentColumnOffset The current row offset. + * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. + * @param ddColumnVariableIndices The (sorted) indices of all DD row variables that need to be considered. + * @param generateValues If set to true, the vector columnsAndValues is filled with the actual entries, which + * only works if the offsets given in rowIndications are already correct. If they need to be computed first, + * this flag needs to be false. + */ + void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues = true) const; + + /*! + * Splits the given matrix DD into the groups using the given group variables. + * + * @param dd The DD to split. + * @param groups A vector that is to be filled with the DDs for the individual groups. + * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split. + */ + void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + + /*! + * Splits the given matrix and vector DDs into the groups using the given group variables. + * + * @param dd1 The matrix DD to split. + * @param dd2 The vector DD to split. + * @param groups A vector that is to be filled with the pairs of matrix/vector DDs for the individual groups. + * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param remainingMetaVariables1 The meta variables that remain in the matrix DD after the groups have been split. + * @param remainingMetaVariables2 The meta variables that remain in the vector DD after the groups have been split. + */ + void splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, InternalAdd>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + + /*! + * Builds an ADD representing the given vector. + * + * @param manager The manager responsible for the ADD. + * @param currentOffset The current offset in the vector. + * @param currentLevel The current level in the DD. + * @param maxLevel The maximal level in the DD. + * @param values The vector that is to be represented by the ADD. + * @param odd The ODD used for the translation. + * @param ddVariableIndices The (sorted) list of DD variable indices to use. + * @return The resulting (CUDD) ADD node. + */ + static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices); + InternalDdManager const* ddManager; - ADD cuddBdd; - } + ADD cuddAdd; + }; } } diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 04e3aabf0..b627e7912 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -27,12 +27,17 @@ namespace storm { template class InternalDdManager; + template + class InternalAdd; + template class Odd; template<> - class InternalBdd { + class InternalBdd { public: + friend class InternalAdd; + /*! * Creates a DD that encapsulates the given CUDD ADD. * diff --git a/src/utility/graph.h b/src/utility/graph.h index ddae2ed35..874f498a8 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -21,16 +21,24 @@ namespace storm { namespace models { namespace symbolic { - template class Model; - template class DeterministicModel; - template class NondeterministicModel; + template + class Model; + + template + class DeterministicModel; + + template + class NondeterministicModel; } } namespace dd { - template class Bdd; - template class Add; + template + class Bdd; + + template + class Add; } @@ -409,8 +417,8 @@ namespace storm { * @param psiStates The BDD containing all psi states of the model. * @return A BDD representing all such states. */ - template - storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template + storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes the set of states for which there does not exist a scheduler that achieves a probability greater @@ -422,8 +430,8 @@ namespace storm { * @param psiStates The psi states of the model. * @return A BDD representing all such states. */ - template - storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template + storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying @@ -435,8 +443,8 @@ namespace storm { * @param psiStates The BDD containing all psi states of the model. * @return A BDD representing all such states. */ - template - storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template + storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying @@ -448,8 +456,8 @@ namespace storm { * @param psiStates The BDD containing all psi states of the model. * @return A BDD representing all such states. */ - template - storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + template + storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; /*! * Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi. @@ -462,8 +470,8 @@ namespace storm { * all schedulers. * @return A BDD representing all such states. */ - template - storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); + template + storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); /*! * Computes the set of states for which there exists a scheduler that achieves probability one of satisfying @@ -477,14 +485,14 @@ namespace storm { * greater than zero. * @return A BDD representing all such states. */ - template - storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; + template + storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); - template - std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + template + std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template - std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; + template + std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Performs a topological sort of the states of the system according to the given transitions. diff --git a/src/utility/solver.h b/src/utility/solver.h index ed7528915..1b53deb80 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -30,8 +30,11 @@ namespace storm { } namespace dd { - template class Add; - template class Bdd; + template + class Add; + + template + class Bdd; } namespace expressions { @@ -45,19 +48,19 @@ namespace storm { template class SymbolicLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; }; template class SymbolicMinMaxLinearEquationSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const; + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) const; }; - template + template class SymbolicGameSolverFactory { public: - virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; template