diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
index b927031e0..9c959be09 100644
--- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
@@ -7,6 +7,7 @@
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidPropertyException.h"
@@ -29,7 +30,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- storm::dd::Add<DdType> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilitiesHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
+ std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilitiesHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
// probability 0 and 1 of satisfying the until-formula.
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates);
@@ -46,7 +47,7 @@ namespace storm {
// Check whether we need to compute exact probabilities for some states.
if (qualitative) {
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
- return statesWithProbability01.second.toAdd() + maybeStates.toAdd() * model.getManager().getConstant(0.5);
+ return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd() + maybeStates.toAdd() * model.getManager().getConstant(0.5)));
} else {
// If there are maybe states, we need to solve an equation system.
if (!maybeStates.isZero()) {
@@ -86,17 +87,11 @@ namespace storm {
solver->solveEquationSystem(x, b);
// Now that we have the explicit solution of the system, we need to transform it to a symbolic representation.
- STORM_LOG_DEBUG("Converting the explicit result to a symbolic form.");
- storm::dd::Add<DdType> numericResult(model.getManager().asSharedPointer(), x, odd, model.getRowVariables());
-
- return statesWithProbability01.second.toAdd() + numericResult;
+ return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.toAdd(), maybeStates, odd, x));
} else {
- return statesWithProbability01.second.toAdd();
+ return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd()));
}
}
-
- exit(-1);
- return storm::dd::Add<DdType>();
}
template<storm::dd::DdType DdType, typename ValueType>
@@ -105,7 +100,7 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
- return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->computeUntilProbabilitiesHelper(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory)));
+ return this->computeUntilProbabilitiesHelper(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, typename ValueType>
diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
index ff9e63762..bc722f57f 100644
--- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
@@ -22,7 +22,7 @@ namespace storm {
private:
// The methods that perform the actual checking.
- static storm::dd::Add<DdType> computeUntilProbabilitiesHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
+ static std::unique_ptr<CheckResult> computeUntilProbabilitiesHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
// An object that is used for retrieving linear equation solvers.
std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp
index b518b0667..e6f0db4aa 100644
--- a/src/modelchecker/results/CheckResult.cpp
+++ b/src/modelchecker/results/CheckResult.cpp
@@ -8,6 +8,7 @@
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidOperationException.h"
@@ -22,6 +23,10 @@ namespace storm {
return false;
}
+ bool CheckResult::isHybrid() const {
+ return false;
+ }
+
bool CheckResult::isQuantitative() const {
return false;
}
@@ -55,6 +60,10 @@ namespace storm {
return false;
}
+ bool CheckResult::isHybridQuantitativeCheckResult() const {
+ return false;
+ }
+
ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() {
return dynamic_cast<ExplicitQualitativeCheckResult&>(*this);
}
@@ -108,6 +117,16 @@ namespace storm {
SymbolicQuantitativeCheckResult<Type> const& CheckResult::asSymbolicQuantitativeCheckResult() const {
return dynamic_cast<SymbolicQuantitativeCheckResult<Type> const&>(*this);
}
+
+ template <storm::dd::DdType Type>
+ HybridQuantitativeCheckResult<Type>& CheckResult::asHybridQuantitativeCheckResult() {
+ return dynamic_cast<HybridQuantitativeCheckResult<Type>&>(*this);
+ }
+
+ template <storm::dd::DdType Type>
+ HybridQuantitativeCheckResult<Type> const& CheckResult::asHybridQuantitativeCheckResult() const {
+ return dynamic_cast<HybridQuantitativeCheckResult<Type> const&>(*this);
+ }
// Explicitly instantiate the template functions.
template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
@@ -116,6 +135,8 @@ namespace storm {
template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asSymbolicQualitativeCheckResult() const;
template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asSymbolicQuantitativeCheckResult();
template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+ template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asHybridQuantitativeCheckResult();
+ template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asHybridQuantitativeCheckResult() const;
#ifdef STORM_HAVE_CARL
template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h
index 05aefd984..93ff1399f 100644
--- a/src/modelchecker/results/CheckResult.h
+++ b/src/modelchecker/results/CheckResult.h
@@ -16,6 +16,7 @@ namespace storm {
template <typename ValueType> class ExplicitQuantitativeCheckResult;
template <storm::dd::DdType Type> class SymbolicQualitativeCheckResult;
template <storm::dd::DdType Type> class SymbolicQuantitativeCheckResult;
+ template <storm::dd::DdType Type> class HybridQuantitativeCheckResult;
// The base class of all check results.
class CheckResult {
@@ -31,12 +32,14 @@ namespace storm {
// Methods to retrieve the actual type of the check result.
virtual bool isExplicit() const;
virtual bool isSymbolic() const;
+ virtual bool isHybrid() const;
virtual bool isQuantitative() const;
virtual bool isQualitative() const;
virtual bool isExplicitQualitativeCheckResult() const;
virtual bool isExplicitQuantitativeCheckResult() const;
virtual bool isSymbolicQualitativeCheckResult() const;
virtual bool isSymbolicQuantitativeCheckResult() const;
+ virtual bool isHybridQuantitativeCheckResult() const;
virtual bool isResultForAllStates() const;
QualitativeCheckResult& asQualitativeCheckResult();
@@ -65,6 +68,12 @@ namespace storm {
template <storm::dd::DdType Type>
SymbolicQuantitativeCheckResult<Type> const& asSymbolicQuantitativeCheckResult() const;
+
+ template <storm::dd::DdType Type>
+ HybridQuantitativeCheckResult<Type>& asHybridQuantitativeCheckResult();
+
+ template <storm::dd::DdType Type>
+ HybridQuantitativeCheckResult<Type> const& asHybridQuantitativeCheckResult() const;
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
};
diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
new file mode 100644
index 000000000..f6bb4136d
--- /dev/null
+++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
@@ -0,0 +1,128 @@
+#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/exceptions/InvalidOperationException.h"
+
+namespace storm {
+ namespace modelchecker {
+ template<storm::dd::DdType Type>
+ HybridQuantitativeCheckResult<Type>::HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd<Type> const& odd, std::vector<double> const& explicitValues) : reachableStates(reachableStates), symbolicStates(symbolicStates), symbolicValues(symbolicValues), explicitStates(explicitStates), odd(odd), explicitValues(explicitValues) {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType Type>
+ std::unique_ptr<CheckResult> HybridQuantitativeCheckResult<Type>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
+ storm::dd::Bdd<Type> symbolicResult;
+
+ // First compute the symbolic part of the result.
+ if (comparisonType == storm::logic::ComparisonType::Less) {
+ symbolicResult = symbolicValues.less(bound);
+ } else if (comparisonType == storm::logic::ComparisonType::LessEqual) {
+ symbolicResult = symbolicValues.lessOrEqual(bound);
+ } else if (comparisonType == storm::logic::ComparisonType::Greater) {
+ symbolicResult = symbolicValues.greater(bound);
+ } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) {
+ symbolicResult = symbolicValues.greaterOrEqual(bound);
+ }
+
+ // Then translate the explicit part to a symbolic format and simultaneously to a qualitative result.
+ symbolicResult |= storm::dd::Bdd<Type>(this->reachableStates.getDdManager(), this->explicitValues, this->odd, this->symbolicValues.getContainedMetaVariables(), comparisonType, bound);
+
+ return std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(reachableStates, symbolicResult));
+ }
+
+ template<storm::dd::DdType Type>
+ bool HybridQuantitativeCheckResult<Type>::isHybrid() const {
+ return true;
+ }
+
+ template<storm::dd::DdType Type>
+ bool HybridQuantitativeCheckResult<Type>::isResultForAllStates() const {
+ return true;
+ }
+
+ template<storm::dd::DdType Type>
+ bool HybridQuantitativeCheckResult<Type>::isHybridQuantitativeCheckResult() const {
+ return true;
+ }
+
+ template<storm::dd::DdType Type>
+ storm::dd::Bdd<Type> const& HybridQuantitativeCheckResult<Type>::getSymbolicStates() const {
+ return symbolicStates;
+ }
+
+ template<storm::dd::DdType Type>
+ storm::dd::Add<Type> const& HybridQuantitativeCheckResult<Type>::getSymbolicValueVector() const {
+ return symbolicValues;
+ }
+
+ template<storm::dd::DdType Type>
+ storm::dd::Bdd<Type> const& HybridQuantitativeCheckResult<Type>::getExplicitStates() const {
+ return explicitStates;
+ }
+
+ template<storm::dd::DdType Type>
+ storm::dd::Odd<Type> const& HybridQuantitativeCheckResult<Type>::getOdd() const {
+ return odd;
+ }
+
+ template<storm::dd::DdType Type>
+ std::vector<double> const& HybridQuantitativeCheckResult<Type>::getExplicitValueVector() const {
+ return explicitValues;
+ }
+
+ template<storm::dd::DdType Type>
+ std::ostream& HybridQuantitativeCheckResult<Type>::writeToStream(std::ostream& out) const {
+ out << "[";
+ bool first = true;
+ if (!this->symbolicStates.isZero()) {
+ if (this->symbolicValues.isZero()) {
+ out << "0";
+ } else {
+ for (auto valuationValuePair : this->symbolicValues) {
+ if (!first) {
+ out << ", ";
+ } else {
+ first = false;
+ }
+ out << valuationValuePair.second;
+ }
+ }
+ }
+ if (!this->explicitStates.isZero()) {
+ for (auto const& element : this->explicitValues) {
+ if (!first) {
+ out << ", ";
+ } else {
+ first = false;
+ }
+ out << element;
+ }
+ }
+ out << "]";
+ return out;
+ }
+
+ template<storm::dd::DdType Type>
+ void HybridQuantitativeCheckResult<Type>::filter(QualitativeCheckResult const& filter) {
+ STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter hybrid check result with non-symbolic filter.");
+
+ // First, we filter the symbolic values.
+ this->symbolicStates = this->symbolicStates && filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
+ this->symbolicValues *= symbolicStates.toAdd();
+
+ // Next, we filter the explicit values.
+
+ // Start by computing the new set of states that is stored explictly and the corresponding ODD.
+ this->explicitStates = this->explicitStates && filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
+ storm::dd::Odd<Type> newOdd(explicitStates);
+
+ // Then compute the new vector of explicit values and set the new data fields.
+ this->explicitValues = this->odd.filterExplicitVector(explicitStates, this->explicitValues);
+ this->odd = newOdd;
+ }
+
+ // Explicitly instantiate the class.
+ template class HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>;
+ }
+}
\ No newline at end of file
diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h
new file mode 100644
index 000000000..d8239f8c9
--- /dev/null
+++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h
@@ -0,0 +1,69 @@
+#ifndef STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_
+#define STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_
+
+#include "src/storage/dd/DdType.h"
+#include "src/storage/dd/CuddAdd.h"
+#include "src/storage/dd/CuddBdd.h"
+#include "src/storage/dd/CuddOdd.h"
+#include "src/modelchecker/results/QuantitativeCheckResult.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+ namespace modelchecker {
+ template<storm::dd::DdType Type>
+ class HybridQuantitativeCheckResult : public QuantitativeCheckResult {
+ public:
+ HybridQuantitativeCheckResult() = default;
+ HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd<Type> const& odd, std::vector<double> const& explicitValues);
+
+ HybridQuantitativeCheckResult(HybridQuantitativeCheckResult const& other) = default;
+ HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult const& other) = default;
+#ifndef WINDOWS
+ HybridQuantitativeCheckResult(HybridQuantitativeCheckResult&& other) = default;
+ HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default;
+#endif
+
+ virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override;
+
+ virtual bool isHybrid() const override;
+ virtual bool isResultForAllStates() const override;
+
+ virtual bool isHybridQuantitativeCheckResult() const override;
+
+ storm::dd::Bdd<Type> const& getSymbolicStates() const;
+
+ storm::dd::Add<Type> const& getSymbolicValueVector() const;
+
+ storm::dd::Bdd<Type> const& getExplicitStates() const;
+
+ storm::dd::Odd<Type> const& getOdd() const;
+
+ std::vector<double> const& getExplicitValueVector() const;
+
+ virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+ virtual void filter(QualitativeCheckResult const& filter) override;
+
+ private:
+ // The set of all reachable states.
+ storm::dd::Bdd<Type> reachableStates;
+
+ // The set of all states whose result is stored symbolically.
+ storm::dd::Bdd<Type> symbolicStates;
+
+ // The symbolic value vector.
+ storm::dd::Add<Type> symbolicValues;
+
+ // The set of all states whose result is stored explicitly.
+ storm::dd::Bdd<Type> explicitStates;
+
+ // The ODD that enables translation of the explicit values to a symbolic format.
+ storm::dd::Odd<Type> odd;
+
+ // The explicit value vector.
+ std::vector<double> explicitValues;
+ };
+ }
+}
+
+#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
index fc18df5c6..088b15a63 100644
--- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
@@ -42,7 +42,7 @@ namespace storm {
}
template<storm::dd::DdType Type>
- storm::dd::Dd<Type> const& SymbolicQuantitativeCheckResult<Type>::getValueVector() const {
+ storm::dd::Add<Type> const& SymbolicQuantitativeCheckResult<Type>::getValueVector() const {
return values;
}
diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h
index ee1c172d7..5f0ba0600 100644
--- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h
+++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h
@@ -28,7 +28,7 @@ namespace storm {
virtual bool isSymbolicQuantitativeCheckResult() const override;
- storm::dd::Dd<Type> const& getValueVector() const;
+ storm::dd::Add<Type> const& getValueVector() const;
virtual std::ostream& writeToStream(std::ostream& out) const override;
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 9a8affbd1..880d15d82 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -730,7 +730,6 @@ namespace storm {
}
#endif
-
template<typename ValueType>
std::vector<ValueType> SparseMatrix<ValueType>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<ValueType> const& otherMatrix) const {
std::vector<ValueType> result(rowCount, storm::utility::zero<ValueType>());
@@ -755,7 +754,6 @@ namespace storm {
return result;
}
-
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyWithVector(std::vector<ValueType> const& vector, std::vector<ValueType>& result) const {
#ifdef STORM_HAVE_INTELTBB
diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp
index b311682f8..6d920f05d 100644
--- a/src/storage/dd/CuddBdd.cpp
+++ b/src/storage/dd/CuddBdd.cpp
@@ -1,8 +1,10 @@
#include <cstring>
#include <algorithm>
+#include <functional>
-#include "src/storage/dd/CuddBdd.h"
#include "src/storage/dd/CuddAdd.h"
+#include "src/storage/dd/CuddBdd.h"
+#include "src/storage/dd/CuddOdd.h"
#include "src/storage/dd/CuddDdManager.h"
#include "src/utility/macros.h"
@@ -14,6 +16,24 @@ namespace storm {
// Intentionally left empty.
}
+ Bdd<DdType::CUDD>::Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd<DdType::CUDD>(ddManager, metaVariables) {
+ switch (comparisonType) {
+ case storm::logic::ComparisonType::Less:
+ this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
+ break;
+ case storm::logic::ComparisonType::LessEqual:
+ this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
+ break;
+ case storm::logic::ComparisonType::Greater:
+ this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
+ break;
+ case storm::logic::ComparisonType::GreaterEqual:
+ this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
+ break;
+ }
+
+ }
+
Add<DdType::CUDD> Bdd<DdType::CUDD>::toAdd() const {
return Add<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables());
}
@@ -253,6 +273,70 @@ namespace storm {
}
}
+ template<typename ValueType>
+ BDD Bdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
+ std::vector<uint_fast64_t> ddVariableIndices = getSortedVariableIndices(*ddManager, metaVariables);
+ uint_fast64_t offset = 0;
+ return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter));
+ }
+
+ template<typename ValueType>
+ DdNode* Bdd<DdType::CUDD>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter) {
+ 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) {
+ if (filter(values[currentOffset++])) {
+ return Cudd_ReadOne(manager);
+ } else {
+ return Cudd_ReadLogicZero(manager);
+ }
+ } 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, filter);
+ } else {
+ elseSuccessor = Cudd_ReadLogicZero(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, filter);
+ } else {
+ thenSuccessor = Cudd_ReadLogicZero(manager);
+ }
+ Cudd_Ref(thenSuccessor);
+
+ // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
+ DdNode* result = Cudd_bddIthVar(manager, static_cast<int>(ddVariableIndices[currentLevel]));
+ Cudd_Ref(result);
+ DdNode* newResult = Cudd_bddIte(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;
+ }
+ }
+
std::ostream& operator<<(std::ostream& out, const Bdd<DdType::CUDD>& bdd) {
bdd.exportToDot();
return out;
diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h
index 7ba62cceb..1868edf2e 100644
--- a/src/storage/dd/CuddBdd.h
+++ b/src/storage/dd/CuddBdd.h
@@ -1,6 +1,7 @@
#ifndef STORM_STORAGE_DD_CUDDBDD_H_
#define STORM_STORAGE_DD_CUDDBDD_H_
+#include "src/logic/ComparisonType.h"
#include "src/storage/dd/Bdd.h"
#include "src/storage/dd/CuddDd.h"
#include "src/storage/dd/CuddAdd.h"
@@ -20,6 +21,18 @@ namespace storm {
template<>
class Bdd<DdType::CUDD> : public Dd<DdType::CUDD> {
public:
+ /*!
+ * Constructs a BDD representation of all encodings that are in the requested relation with the given value.
+ *
+ * @param ddManager The DD manager responsible for the resulting BDD.
+ * @param explicitValues The explicit values to compare to the given value.
+ * @param odd The ODD used for the translation from the explicit representation to a symbolic one.
+ * @param metaVariables The meta variables to use for the symbolic encoding.
+ * @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
+ * @param value The value to compare with.
+ */
+ Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+
// Declare the DdManager and DdIterator class as friend so it can access the internals of a DD.
friend class DdManager<DdType::CUDD>;
friend class DdForwardIterator<DdType::CUDD>;
@@ -274,6 +287,34 @@ namespace storm {
*/
Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+ /*!
+ * Builds a BDD representing the values that make the given filter function evaluate to true.
+ *
+ * @param ddManager The manager responsible for the BDD.
+ * @param values The values that are to be checked against the filter function.
+ * @param odd The ODD used for the translation.
+ * @param metaVariables The meta variables used for the translation.
+ * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
+ * @return The resulting (CUDD) BDD.
+ */
+ template<typename ValueType>
+ static BDD fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
+
+ /*!
+ * Builds a BDD representing the values that make the given filter function evaluate to true.
+ *
+ * @param manager The manager responsible for the BDD.
+ * @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 values that are to be checked against the filter function.
+ * @param odd The ODD used for the translation.
+ * @param ddVariableIndices The (sorted) list of DD variable indices to use.
+ * @return The resulting (CUDD) BDD node.
+ */
+ template<typename ValueType>
+ static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter);
+
// The BDD created by CUDD.
BDD cuddBdd;
};
diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp
index 31bc42dd6..46ed679b6 100644
--- a/src/storage/dd/CuddOdd.cpp
+++ b/src/storage/dd/CuddOdd.cpp
@@ -37,7 +37,7 @@ namespace storm {
// Now construct the ODD structure from the BDD.
std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
-
+
// Finally, move the children of the root ODD into this ODD.
this->elseNode = std::move(rootOdd->elseNode);
this->thenNode = std::move(rootOdd->thenNode);
@@ -95,6 +95,54 @@ namespace storm {
return this->elseNode == nullptr && this->thenNode == nullptr;
}
+ std::vector<double> Odd<DdType::CUDD>::filterExplicitVector(storm::dd::Bdd<DdType::CUDD> const& selectedValues, std::vector<double> const& values) const {
+ std::vector<double> result(selectedValues.getNonZeroCount());
+
+ // First, we need to determine the involved DD variables indices.
+ std::vector<uint_fast64_t> ddVariableIndices = selectedValues.getSortedVariableIndices();
+
+ uint_fast64_t currentIndex = 0;
+ addSelectedValuesToVectorRec(selectedValues.getCuddDdNode(), selectedValues.getDdManager()->getCuddManager(), 0, Cudd_IsComplement(selectedValues.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, *this, result, currentIndex, values);
+ return result;
+ }
+
+ void Odd<DdType::CUDD>::addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values) {
+ // If there are no more values to select, we can directly return.
+ if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
+ return;
+ } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
+ return;
+ }
+
+ if (currentLevel == maxLevel) {
+ // If the DD is not the zero leaf, then the then-offset is 1.
+ bool selected = false;
+ if (dd != Cudd_ReadLogicZero(manager.getManager())) {
+ selected = !complement;
+ }
+
+ if (selected) {
+ result[currentIndex++] = values[currentOffset];
+ }
+ } 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.
+ addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
+ addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
+ } else {
+ // Otherwise, we compute the ODDs for both the then- and else successors.
+ DdNode* thenDdNode = Cudd_T(dd);
+ DdNode* elseDdNode = Cudd_E(dd);
+
+ // Determine whether we have to evaluate the successors as if they were complemented.
+ bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
+ bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
+
+ addSelectedValuesToVectorRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
+ addSelectedValuesToVectorRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
+ }
+ }
+
std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels) {
// Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
@@ -140,7 +188,7 @@ namespace storm {
boost::hash_combine(result, key.second);
return result;
}
-
+
std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels) {
// Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement));
diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h
index 9269e4ab1..4a03a3c26 100644
--- a/src/storage/dd/CuddOdd.h
+++ b/src/storage/dd/CuddOdd.h
@@ -103,6 +103,15 @@ namespace storm {
*/
bool isTerminalNode() const;
+ /*!
+ * Filters the given explicit vector using the symbolic representation of which values to select.
+ *
+ * @param selectedValues A symbolic representation of which values to select.
+ * @param values The value vector from which to select the values.
+ * @return The resulting vector.
+ */
+ std::vector<double> filterExplicitVector(storm::dd::Bdd<DdType::CUDD> const& selectedValues, std::vector<double> const& values) const;
+
private:
// Declare a hash functor that is used for the unique tables in the construction process.
class HashFunctor {
@@ -150,6 +159,23 @@ namespace storm {
*/
static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels);
+
+ /*!
+ * Adds the selected values the target vector.
+ *
+ * @param dd The current node of the DD representing the selected values.
+ * @param manager The manager responsible for the DD.
+ * @param currentLevel The currently considered level in the DD.
+ * @param maxLevel The number of levels that need to be considered.
+ * @param ddVariableIndices The sorted list of variable indices to use.
+ * @param currentOffset The offset along the path taken in the DD representing the selected values.
+ * @param odd The current ODD node.
+ * @param result The target vector to which to write the values.
+ * @param currentIndex The index at which the next element is to be written.
+ * @param values The value vector from which to select the values.
+ */
+ static void addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values);
+
// The then- and else-nodes.
std::shared_ptr<Odd<DdType::CUDD>> elseNode;
std::shared_ptr<Odd<DdType::CUDD>> thenNode;