From 8657fb0181d94eb3638277e72ddecbae7ec1387b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 2 Dec 2015 16:36:52 +0100
Subject: [PATCH] introduced relational product operations to prob0/1
algorithms (where possible)
Former-commit-id: 7fcd642030671518151c965e67e5155515a28122
---
src/builder/DdPrismModelBuilder.cpp | 11 ---
src/storage/dd/Bdd.cpp | 30 +++++++-
src/storage/dd/Bdd.h | 20 ++++-
src/storage/dd/cudd/InternalCuddBdd.cpp | 7 +-
src/storage/dd/cudd/InternalCuddBdd.h | 11 +++
src/storage/dd/sylvan/InternalSylvanBdd.cpp | 29 ++++---
src/storage/dd/sylvan/InternalSylvanBdd.h | 11 +++
.../dd/sylvan/InternalSylvanDdManager.cpp | 5 ++
src/utility/graph.cpp | 46 ++++++++---
test/functional/utility/GraphTest.cpp | 77 ++++++++++++++++++-
10 files changed, 199 insertions(+), 48 deletions(-)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 993fca443..0f636adfb 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -1175,15 +1175,6 @@ namespace storm {
STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis.");
changed = false;
storm::dd::Bdd<Type> tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables);
-
- storm::dd::Bdd<Type> tmp2 = reachableStates.andExists(transitionBdd, generationInfo.rowMetaVariables);
- tmp2 = tmp2.swapVariables(generationInfo.rowColumnMetaVariablePairs);
-
- tmp2.exportToDot("tmp2.dot");
- tmp.exportToDot("tmp.dot");
-
- assert(tmp == tmp2);
-
storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates);
// Check whether new states were indeed discovered.
@@ -1193,8 +1184,6 @@ namespace storm {
reachableStates |= newReachableStates;
- std::cout << "iter: " << iteration << " with nnz: " << reachableStates.getNonZeroCount() << std::endl;
-
++iteration;
} while (changed);
diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp
index 87234b0e1..7b30ccfed 100644
--- a/src/storage/dd/Bdd.cpp
+++ b/src/storage/dd/Bdd.cpp
@@ -144,9 +144,8 @@ namespace storm {
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
- std::set<storm::expressions::Variable> tmpMetaVariables = Dd<LibraryType>::joinMetaVariables(*this, relation);
std::set<storm::expressions::Variable> newMetaVariables;
- std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+ std::set_difference(relation.getContainedMetaVariables().begin(), relation.getContainedMetaVariables().end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
std::vector<InternalBdd<LibraryType>> rowVariables;
for (auto const& metaVariable : rowMetaVariables) {
@@ -169,9 +168,8 @@ namespace storm {
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::inverseRelationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
- std::set<storm::expressions::Variable> tmpMetaVariables = Dd<LibraryType>::joinMetaVariables(*this, relation);
std::set<storm::expressions::Variable> newMetaVariables;
- std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+ std::set_difference(relation.getContainedMetaVariables().begin(), relation.getContainedMetaVariables().end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
std::vector<InternalBdd<LibraryType>> rowVariables;
for (auto const& metaVariable : rowMetaVariables) {
@@ -192,6 +190,30 @@ namespace storm {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.inverseRelationalProduct(relation, rowVariables, columnVariables), newMetaVariables);
}
+ template<DdType LibraryType>
+ Bdd<LibraryType> Bdd<LibraryType>::inverseRelationalProductWithExtendedRelation(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
+ std::set<storm::expressions::Variable> newMetaVariables;
+ std::set_difference(relation.getContainedMetaVariables().begin(), relation.getContainedMetaVariables().end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+
+ std::vector<InternalBdd<LibraryType>> rowVariables;
+ for (auto const& metaVariable : rowMetaVariables) {
+ DdMetaVariable<LibraryType> const& variable = this->getDdManager()->getMetaVariable(metaVariable);
+ for (auto const& ddVariable : variable.getDdVariables()) {
+ rowVariables.push_back(ddVariable);
+ }
+ }
+
+ std::vector<InternalBdd<LibraryType>> columnVariables;
+ for (auto const& metaVariable : columnMetaVariables) {
+ DdMetaVariable<LibraryType> const& variable = this->getDdManager()->getMetaVariable(metaVariable);
+ for (auto const& ddVariable : variable.getDdVariables()) {
+ columnVariables.push_back(ddVariable);
+ }
+ }
+
+ return Bdd<LibraryType>(this->getDdManager(), internalBdd.inverseRelationalProductWithExtendedRelation(relation, rowVariables, columnVariables), newMetaVariables);
+ }
+
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
std::set<storm::expressions::Variable> newContainedMetaVariables;
diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h
index 95a801bee..a64cebf28 100644
--- a/src/storage/dd/Bdd.h
+++ b/src/storage/dd/Bdd.h
@@ -187,8 +187,9 @@ namespace storm {
Bdd<LibraryType> restrict(Bdd<LibraryType> const& constraint) const;
/*!
- * Computes the relational product of the current BDD and the given BDD representing a relation. Note that
- * this operation assumes that the row and column variables are interleaved.
+ * Computes the relational product of the current BDD and the given BDD representing a relation.
+ * Note that this operation assumes that the row and column variables are interleaved and that the relation
+ * only contains the row and column variables.
*
* @param relation The relation to use.
* @param rowMetaVariables The row meta variables used in the relation.
@@ -199,7 +200,8 @@ namespace storm {
/*!
* Computes the inverse relational product of the current BDD and the given BDD representing a relation.
- * Note that this operation assumes that the row and column variables are interleaved.
+ * Note that this operation assumes that the row and column variables are interleaved and that the relation
+ * only contains the row and column variables.
*
* @param relation The relation to use.
* @param rowMetaVariables The row meta variables used in the relation.
@@ -208,6 +210,18 @@ namespace storm {
*/
Bdd<LibraryType> inverseRelationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const;
+ /*!
+ * Computes the inverse relational product of the current BDD and the given BDD representing a relation that
+ * contains more variables than just the row and column variables.
+ * Note that this operation assumes that the row and column variables are interleaved.
+ *
+ * @param relation The relation to use.
+ * @param rowMetaVariables The row meta variables used in the relation.
+ * @param columnMetaVariables The row meta variables used in the relation.
+ * @return The inverse relational product.
+ */
+ Bdd<LibraryType> inverseRelationalProductWithExtendedRelation(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const;
+
/*!
* Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have
* the same number of underlying BDD variables.
diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp
index a257c9640..9bd13653c 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddBdd.cpp
@@ -46,11 +46,14 @@ namespace storm {
cube &= variable;
}
- InternalBdd<DdType::CUDD> result = this->andExists(relation, cube);
- result = result.swapVariables(rowVariables, columnVariables);
+ InternalBdd<DdType::CUDD> result = this->swapVariables(rowVariables, columnVariables).andExists(relation, cube);
return result;
}
+ InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const {
+ return this->inverseRelationalProduct(relation, rowVariables, columnVariables);
+ }
+
InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::ite(InternalBdd<DdType::CUDD> const& thenDd, InternalBdd<DdType::CUDD> const& elseDd) const {
return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()));
}
diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h
index 4358e491f..b8c02da06 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.h
+++ b/src/storage/dd/cudd/InternalCuddBdd.h
@@ -95,6 +95,17 @@ namespace storm {
* @return The ralational product.
*/
InternalBdd<DdType::CUDD> inverseRelationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;
+
+ /*!
+ * Computes the inverse relational product of the current BDD and the given BDD representing a relation that
+ * contains more than just the row and column variables.
+ *
+ * @param relation The relation to use.
+ * @param rowVariables The row variables of the relation represented as individual BDDs.
+ * @param columnVariables The row variables of the relation represented as individual BDDs.
+ * @return The ralational product.
+ */
+ InternalBdd<DdType::CUDD> inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;
/*!
* Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero
diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
index c2e72a97a..f7cedfe04 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
@@ -31,25 +31,22 @@ namespace storm {
}
InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::relationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const {
- InternalBdd<DdType::Sylvan> cube = ddManager->getBddOne();
- for (auto const& variable : rowVariables) {
- cube &= variable;
- }
- for (auto const& variable : columnVariables) {
- cube &= variable;
- }
-
- this->exportToDot("set.dot", {});
- relation.exportToDot("relation.dot", {});
- cube.exportToDot("cube.dot", {});
-
- InternalBdd<DdType::Sylvan> result(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, cube.sylvanBdd));
- result.exportToDot("result.dot", {});
- return result;
+ return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, sylvan::Bdd(sylvan_false)));
}
InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::inverseRelationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+ return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.RelPrev(relation.sylvanBdd, sylvan::Bdd(sylvan_false)));
+ }
+
+ InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const {
+ // Currently, there is no specialized version to perform this operation, so we fall back to the regular operations.
+
+ InternalBdd<DdType::Sylvan> columnCube = ddManager->getBddOne();
+ for (auto const& variable : columnVariables) {
+ columnCube &= variable;
+ }
+
+ return this->swapVariables(rowVariables, columnVariables).andExists(relation, columnCube);
}
InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::ite(InternalBdd<DdType::Sylvan> const& thenDd, InternalBdd<DdType::Sylvan> const& elseDd) const {
diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h
index 5777f391d..9502c2136 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.h
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.h
@@ -85,6 +85,17 @@ namespace storm {
*/
InternalBdd<DdType::Sylvan> inverseRelationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const;
+ /*!
+ * Computes the inverse relational product of the current BDD and the given BDD representing a relation that
+ * contains more than just the row and column variables.
+ *
+ * @param relation The relation to use.
+ * @param rowVariables The row variables of the relation represented as individual BDDs.
+ * @param columnVariables The row variables of the relation represented as individual BDDs.
+ * @return The ralational product.
+ */
+ InternalBdd<DdType::Sylvan> inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) 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
diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
index c30da4863..c754887bb 100644
--- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -29,6 +29,11 @@ namespace storm {
InternalDdManager<DdType::Sylvan>::~InternalDdManager() {
--numberOfInstances;
if (numberOfInstances == 0) {
+ // Enable this to print the sylvan statistics to a file.
+// FILE* filePointer = fopen("sylvan.stats", "w");
+// sylvan_stats_report(filePointer, 0);
+// fclose(filePointer);
+
sylvan::Sylvan::quitPackage();
lace_exit();
}
diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
index 81856a665..17384fa55 100644
--- a/src/utility/graph.cpp
+++ b/src/utility/graph.cpp
@@ -194,9 +194,7 @@ namespace storm {
}
lastIterationStates = statesWithProbabilityGreater0;
- statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs());
- statesWithProbabilityGreater0 &= transitionMatrix;
- statesWithProbabilityGreater0 = statesWithProbabilityGreater0.existsAbstract(model.getColumnVariables());
+ statesWithProbabilityGreater0 = statesWithProbabilityGreater0.inverseRelationalProduct(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
statesWithProbabilityGreater0 &= phiStates;
statesWithProbabilityGreater0 |= lastIterationStates;
++iterations;
@@ -677,8 +675,7 @@ namespace storm {
storm::dd::Bdd<Type> abstractedTransitionMatrix = transitionMatrix.existsAbstract(model.getNondeterminismVariables());
while (lastIterationStates != statesWithProbabilityGreater0E) {
lastIterationStates = statesWithProbabilityGreater0E;
- statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs());
- statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(abstractedTransitionMatrix, model.getColumnVariables());
+ statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.inverseRelationalProduct(abstractedTransitionMatrix, model.getRowVariables(), model.getColumnVariables());
statesWithProbabilityGreater0E &= phiStates;
statesWithProbabilityGreater0E |= lastIterationStates;
++iterations;
@@ -702,8 +699,7 @@ namespace storm {
uint_fast64_t iterations = 0;
while (lastIterationStates != statesWithProbabilityGreater0A) {
lastIterationStates = statesWithProbabilityGreater0A;
- statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs());
- statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrix, model.getColumnVariables());
+ statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
statesWithProbabilityGreater0A |= model.getIllegalMask();
statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.universalAbstract(model.getNondeterminismVariables());
statesWithProbabilityGreater0A &= phiStates;
@@ -757,8 +753,7 @@ namespace storm {
storm::dd::Bdd<Type> temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs());
temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables());
- storm::dd::Bdd<Type> temporary2 = innerStates.swapVariables(model.getRowColumnMetaVariablePairs());
- temporary2 = transitionMatrix.andExists(temporary2, model.getColumnVariables());
+ storm::dd::Bdd<Type> temporary2 = innerStates.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
temporary = temporary.andExists(temporary2, model.getNondeterminismVariables());
temporary &= phiStates;
@@ -1051,7 +1046,6 @@ namespace storm {
#ifdef STORM_HAVE_CARL
-
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates);
@@ -1107,6 +1101,8 @@ namespace storm {
#endif
+ // Instantiations for CUDD.
+
template storm::dd::Bdd<storm::dd::DdType::CUDD> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::Model<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& statesWithProbabilityGreater0);
@@ -1133,6 +1129,36 @@ namespace storm {
template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates);
+
+
+ // Instantiations for Sylvan.
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0);
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01(storm::models::symbolic::DeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Add<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0A);
+
+ template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0E);
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Max(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
+ template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+
} // namespace graph
} // namespace utility
} // namespace storm
diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp
index d92b6e887..c6baf90b1 100644
--- a/test/functional/utility/GraphTest.cpp
+++ b/test/functional/utility/GraphTest.cpp
@@ -15,7 +15,7 @@
#include "src/storage/dd/Bdd.h"
#include "src/storage/dd/DdManager.h"
-TEST(GraphTest, SymbolicProb01) {
+TEST(GraphTest, SymbolicProb01_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -36,7 +36,29 @@ TEST(GraphTest, SymbolicProb01) {
EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount());
}
-TEST(GraphTest, SymbolicProb01MinMax) {
+// FIXME: re-enable as soon as the ADD iterator of sylvan works.
+TEST(DISABLED_GraphTest, SymbolicProb01_Sylvan) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+
+ ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
+
+ std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observe0Greater1")));
+ EXPECT_EQ(4409ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(1316ul, statesWithProbability01.second.getNonZeroCount());
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observeIGreater1")));
+ EXPECT_EQ(1091ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(4802ul, statesWithProbability01.second.getNonZeroCount());
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observeOnlyTrueSender")));
+ EXPECT_EQ(5829ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount());
+}
+
+TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -87,6 +109,57 @@ TEST(GraphTest, SymbolicProb01MinMax) {
EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
}
+TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+
+ ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+
+ std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("elected")));
+ EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("elected")));
+ EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+
+ ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
+ EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount());
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
+ EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount());
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
+ EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount());
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
+ EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+
+ ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("collision_max_backoff")));
+ EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
+
+ ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("collision_max_backoff")));
+ EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
+ EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
+}
+
TEST(GraphTest, ExplicitProb01) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);