From 7f75db279033a7f52f16cd7e564b9e3e19008001 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 6 Dec 2015 22:16:50 +0100 Subject: [PATCH] ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working. Former-commit-id: b11b2f74760e5df33c87f32a98476e2e70596fdb --- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 38 ++-- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 4 + .../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 8 +- .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 17 +- .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 31 ++-- .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 1 + .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 2 +- .../SymbolicPropositionalModelChecker.cpp | 6 + src/modelchecker/results/CheckResult.cpp | 8 + .../SymbolicQualitativeCheckResult.cpp | 1 + .../SymbolicQuantitativeCheckResult.cpp | 1 + src/solver/SymbolicGameSolver.cpp | 1 + src/solver/SymbolicLinearEquationSolver.cpp | 2 + src/storage/dd/Add.cpp | 10 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 6 +- src/storage/dd/cudd/InternalCuddAdd.h | 8 +- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 16 +- src/storage/dd/sylvan/InternalSylvanAdd.h | 10 +- src/storage/dd/sylvan/SylvanAddIterator.cpp | 161 ++++++++++++++++- src/storage/dd/sylvan/SylvanAddIterator.h | 92 ++++++++++ src/utility/solver.cpp | 2 + .../builder/DdPrismModelBuilderTest.cpp | 36 ++-- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 162 +++++++++++++++++- .../solver/FullySymbolicGameSolverTest.cpp | 60 ++++++- test/functional/storage/CuddDdTest.cpp | 2 +- test/functional/storage/SylvanDdTest.cpp | 85 ++++----- test/functional/utility/GraphTest.cpp | 3 +- 27 files changed, 637 insertions(+), 136 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index ed97cb6aa..f044e143d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -1134,8 +1134,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb) else if (val_b == 0) return b; else { MTBDD result; - if (val_a == 1) result = b; - else if (val_b == 1) result = a; + if (val_a == 1) result = mtbdd_regular(b); + else if (val_b == 1) result = mtbdd_regular(a); else result = mtbdd_uint64(val_a*val_b); int nega = mtbdd_isnegated(a); int negb = mtbdd_isnegated(b); @@ -1150,13 +1150,16 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb) else if (vval_b == 0.0) return b; else { MTBDD result; - if (vval_a == 1.0) result = b; - else if (vval_b == 1.0) result = a; + if (vval_a == 1.0) result = mtbdd_regular(b); + else if (vval_b == 1.0) result = mtbdd_regular(a); else result = mtbdd_double(vval_a*vval_b); int nega = mtbdd_isnegated(a); int negb = mtbdd_isnegated(b); - if (nega ^ negb) return mtbdd_negate(result); - else return result; + if (nega ^ negb) { + return mtbdd_negate(result); + } else { + return result; + } } } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { // both fraction @@ -1560,8 +1563,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, double vb = mtbdd_getdouble(b); if (mtbdd_isnegated(b)) vb = -vb; if (va == 0) return mtbdd_false; - va = (va - vb) / va; - if (va < 0) va = -va; + va = fabs((va - vb) / va); return (va < *(double*)&svalue) ? mtbdd_true : mtbdd_false; } @@ -2558,7 +2560,7 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb) } else if (mtbddnode_isleaf(n)) { uint32_t type = mtbddnode_gettype(n); uint64_t value = mtbddnode_getvalue(n); - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd)); + fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", mtbdd_regular(mtbdd)); switch (type) { case 0: fprintf(out, "%" PRIu64, value); @@ -2576,16 +2578,16 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb) fprintf(out, "\"];\n"); } else { fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n", - MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n)); + mtbdd_regular(mtbdd), mtbddnode_getvariable(n)); - mtbdd_fprintdot_rec(out, mtbddnode_getlow(n), cb); - mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n), cb); + mtbdd_fprintdot_rec(out, mtbdd_regular(mtbddnode_getlow(n)), cb); + mtbdd_fprintdot_rec(out, mtbdd_regular(mtbddnode_gethigh(n)), cb); - fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n", - mtbdd, mtbddnode_getlow(n)); + fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed dir=both arrowtail=%s];\n", + mtbdd, mtbdd_regular(mtbddnode_getlow(n)), mtbdd_isnegated(mtbddnode_getlow(n)) ? "dot" : "none"); fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", - mtbdd, MTBDD_STRIPMARK(mtbddnode_gethigh(n)), - mtbddnode_getcomp(n) ? "dot" : "none"); + mtbdd, mtbdd_regular(mtbddnode_gethigh(n)), + mtbdd_isnegated(mtbddnode_gethigh(n)) ? "dot" : "none"); } } @@ -2598,9 +2600,9 @@ mtbdd_fprintdot(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb) fprintf(out, "edge [dir = forward];\n"); fprintf(out, "root [style=invis];\n"); fprintf(out, "root -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", - MTBDD_STRIPMARK(mtbdd), MTBDD_HASMARK(mtbdd) ? "dot" : "none"); + mtbdd_regular(mtbdd), mtbdd_isnegated(mtbdd) ? "dot" : "none"); - mtbdd_fprintdot_rec(out, mtbdd, cb); + mtbdd_fprintdot_rec(out, mtbdd_regular(mtbdd), cb); mtbdd_unmark_rec(mtbdd); fprintf(out, "}\n"); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 12dbbcc46..93b71af57 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -539,4 +539,8 @@ int mtbdd_iszero(MTBDD dd) { return mtbdd_getnumer(dd) == 0; } return 0; +} + +int mtbdd_isnonzero(MTBDD dd) { + return mtbdd_iszero(dd) ? 0 : 1; } \ No newline at end of file diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index ef8b1c17c..63bc61c90 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -1,8 +1,3 @@ -/** - * Compute a - b - */ -#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b)) - /** * Binary operation Divide (for MTBDDs of same type) * Only for MTBDDs where all leaves are Integer or Double. @@ -107,7 +102,8 @@ TASK_DECL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD) TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t); #define mtbdd_non_zero_count(dd, nvars) CALL(mtbdd_non_zero_count, dd, nvars) -// Checks whether the given MTBDD represents a zero leaf. +// Checks whether the given MTBDD (does represents a zero leaf. int mtbdd_iszero(MTBDD); +int mtbdd_isnonzero(MTBDD); #define mtbdd_regular(dd) (dd & ~mtbdd_complement) diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 4630d42b7..7370e8b1d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -15,11 +15,11 @@ Bdd Less(const Mtbdd& other) const; Bdd LessOrEqual(const Mtbdd& other) const; - - double getDoubleMax() const; - double getDoubleMin() const; - + Mtbdd Minimum() const; + + Mtbdd Maximum() const; + bool EqualNorm(const Mtbdd& other, double epsilon) const; bool EqualNormRel(const Mtbdd& other, double epsilon) const; @@ -41,4 +41,11 @@ */ double NonZeroCount(size_t variableCount) const; - bool isValid() const; \ No newline at end of file + bool isValid() const; + + /** + * @brief Writes .dot file of this Bdd. Not thread-safe! + */ + void PrintDot(FILE *out) const; + + \ No newline at end of file diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 71ca7256e..8f060069e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -49,20 +49,6 @@ Mtbdd::LessOrEqual(const Mtbdd& other) const { return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd); } -double -Mtbdd::getDoubleMax() const { - LACE_ME; - MTBDD maxNode = mtbdd_maximum(mtbdd); - return mtbdd_getdouble(maxNode); -} - -double -Mtbdd::getDoubleMin() const { - LACE_ME; - MTBDD minNode = mtbdd_minimum(mtbdd); - return mtbdd_getdouble(minNode); -} - bool Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const { LACE_ME; @@ -122,3 +108,20 @@ Mtbdd::isValid() const { LACE_ME; return mtbdd_test_isvalid(mtbdd) == 1; } + +Mtbdd +Mtbdd::Minimum() const { + LACE_ME; + return mtbdd_minimum(mtbdd); +} + +Mtbdd +Mtbdd::Maximum() const { + LACE_ME; + return mtbdd_maximum(mtbdd); +} + +void +Mtbdd::PrintDot(FILE *out) const { + mtbdd_fprintdot(out, mtbdd, NULL); +} diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 7791bac56..b69c443a5 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -91,5 +91,6 @@ namespace storm { } template class SymbolicDtmcPrctlModelChecker; + template class SymbolicDtmcPrctlModelChecker; } } diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 56530a78b..e870174ce 100644 --- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -132,7 +132,6 @@ namespace storm { template storm::dd::Add SymbolicDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { - // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -179,6 +178,7 @@ namespace storm { } template class SymbolicDtmcPrctlHelper; + template class SymbolicDtmcPrctlHelper; } } diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 39c776d34..328c0f109 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -61,5 +61,11 @@ namespace storm { template storm::models::symbolic::Ctmc const& SymbolicPropositionalModelChecker::getModelAs() const; template storm::models::symbolic::Mdp const& SymbolicPropositionalModelChecker::getModelAs() const; template class SymbolicPropositionalModelChecker; + + template storm::models::symbolic::Dtmc const& SymbolicPropositionalModelChecker::getModelAs() const; + template storm::models::symbolic::Ctmc const& SymbolicPropositionalModelChecker::getModelAs() const; + template storm::models::symbolic::Mdp const& SymbolicPropositionalModelChecker::getModelAs() const; + template class SymbolicPropositionalModelChecker; + } } \ No newline at end of file diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp index fbf1deac2..40ca4badb 100644 --- a/src/modelchecker/results/CheckResult.cpp +++ b/src/modelchecker/results/CheckResult.cpp @@ -130,6 +130,7 @@ namespace storm { // Explicitly instantiate the template functions. template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; + template SymbolicQualitativeCheckResult& CheckResult::asSymbolicQualitativeCheckResult(); template SymbolicQualitativeCheckResult const& CheckResult::asSymbolicQualitativeCheckResult() const; template SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult(); @@ -137,6 +138,13 @@ namespace storm { template HybridQuantitativeCheckResult& CheckResult::asHybridQuantitativeCheckResult(); template HybridQuantitativeCheckResult const& CheckResult::asHybridQuantitativeCheckResult() const; + template SymbolicQualitativeCheckResult& CheckResult::asSymbolicQualitativeCheckResult(); + template SymbolicQualitativeCheckResult const& CheckResult::asSymbolicQualitativeCheckResult() const; + template SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult(); + template SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const; + template HybridQuantitativeCheckResult& CheckResult::asHybridQuantitativeCheckResult(); + template HybridQuantitativeCheckResult const& CheckResult::asHybridQuantitativeCheckResult() const; + #ifdef STORM_HAVE_CARL template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index b0f188ffe..2275b942f 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -66,5 +66,6 @@ namespace storm { } template class SymbolicQualitativeCheckResult; + template class SymbolicQualitativeCheckResult; } } \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index f837876e4..5031d9d88 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -91,5 +91,6 @@ namespace storm { // Explicitly instantiate the class. template class SymbolicQuantitativeCheckResult; + template class SymbolicQuantitativeCheckResult; } } \ No newline at end of file diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index 752c6818f..ccb762fbf 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -58,6 +58,7 @@ namespace storm { } template class SymbolicGameSolver; + template class SymbolicGameSolver; } } \ No newline at end of file diff --git a/src/solver/SymbolicLinearEquationSolver.cpp b/src/solver/SymbolicLinearEquationSolver.cpp index acb2a9f91..35f4f9a56 100644 --- a/src/solver/SymbolicLinearEquationSolver.cpp +++ b/src/solver/SymbolicLinearEquationSolver.cpp @@ -45,6 +45,7 @@ namespace storm { while (!converged && iterationCount < maximalNumberOfIterations) { storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); + storm::dd::Add tmp = lu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); tmp = b - tmp; tmp = tmp.swapVariables(this->rowColumnMetaVariablePairs); @@ -82,6 +83,7 @@ namespace storm { } template class SymbolicLinearEquationSolver; + template class SymbolicLinearEquationSolver; } } diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 64d02c99f..0ec72e15f 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -725,12 +725,18 @@ namespace storm { template AddIterator Add::begin(bool enumerateDontCareMetaVariables) const { - return internalAdd.begin(this->getDdManager(), this->getContainedMetaVariables(), enumerateDontCareMetaVariables); + uint_fast64_t numberOfDdVariables = 0; + for (auto const& metaVariable : this->getContainedMetaVariables()) { + auto const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); + numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables(); + } + + return internalAdd.begin(this->getDdManager(), Bdd::getCube(this->getDdManager(), this->getContainedMetaVariables()), numberOfDdVariables, this->getContainedMetaVariables(), enumerateDontCareMetaVariables); } template AddIterator Add::end(bool enumerateDontCareMetaVariables) const { - return internalAdd.end(this->getDdManager(), enumerateDontCareMetaVariables); + return internalAdd.end(this->getDdManager()); } template diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 1cbff380d..0573a9629 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -316,7 +316,7 @@ namespace storm { } template - AddIterator InternalAdd::begin(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const& variableCube, uint_fast64_t numberOfDdVariables, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { int* cube; double value; DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); @@ -324,8 +324,8 @@ namespace storm { } template - AddIterator InternalAdd::end(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables) const { - return AddIterator(fullDdManager, nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); + AddIterator InternalAdd::end(DdManager const& fullDdManager) const { + return AddIterator(fullDdManager, nullptr, nullptr, 0, true, nullptr, false); } template diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index b93a6205b..e235a4e6d 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -461,22 +461,22 @@ namespace storm { * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. * * @param fullDdManager The DD manager responsible for this ADD. + * @param variableCube The cube of variables contained in this ADD. + * @param numberOfDdVariables The number of variables contained in this ADD. * @param metaVariables The meta variables contained in the ADD. * @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(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; + AddIterator begin(DdManager const& fullDdManager, InternalBdd const& variableCube, uint_fast64_t numberOfDdVariables, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; /*! * Retrieves an iterator that points past the end of the container. * * @param fullDdManager The DD manager responsible for this ADD. - * @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(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables = true) const; + AddIterator end(DdManager const& fullDdManager) const; /*! * Composes the ADD with an explicit vector by performing a specified function between the entries of this diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 2fa479044..824a9dd43 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1,6 +1,8 @@ #include "src/storage/dd/sylvan/InternalSylvanAdd.h" +#include "src/storage/dd/sylvan/SylvanAddIterator.h" #include "src/storage/dd/sylvan/InternalSylvanDdManager.h" +#include "src/storage/dd/DdManager.h" #include "src/storage/SparseMatrix.h" @@ -246,12 +248,12 @@ namespace storm { template ValueType InternalAdd::getMin() const { - return static_cast(this->sylvanMtbdd.getDoubleMin()); + return getValue(this->sylvanMtbdd.Minimum().GetMTBDD()); } template ValueType InternalAdd::getMax() const { - return static_cast(this->sylvanMtbdd.getDoubleMax()); + return getValue(this->sylvanMtbdd.Maximum().GetMTBDD()); } template @@ -283,18 +285,18 @@ namespace storm { void InternalAdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - mtbdd_fprintdot(filePointer, this->sylvanMtbdd.GetMTBDD(), nullptr); + this->sylvanMtbdd.PrintDot(filePointer); fclose(filePointer); } template - AddIterator InternalAdd::begin(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + AddIterator InternalAdd::begin(DdManager const& fullDdManager, InternalBdd const& variableCube, uint_fast64_t numberOfDdVariables, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + return AddIterator::createBeginIterator(fullDdManager, this->getSylvanMtbdd(), variableCube.getSylvanBdd(), numberOfDdVariables, &metaVariables, enumerateDontCareMetaVariables); } template - AddIterator InternalAdd::end(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + AddIterator InternalAdd::end(DdManager const& fullDdManager) const { + return AddIterator::createEndIterator(fullDdManager); } template diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index c93793560..9aafc630e 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -40,6 +40,8 @@ namespace storm { template class InternalAdd { public: + friend class AddIterator; + /*! * Creates an ADD that encapsulates the given Sylvan MTBDD. * @@ -459,22 +461,22 @@ namespace storm { * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value. * * @param fullDdManager The DD manager responsible for this ADD. + * @param variableCube The cube of variables contained in this ADD. + * @param numberOfDdVariables The number of variables contained in this ADD. * @param metaVariables The meta variables contained in the ADD. * @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(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; + AddIterator begin(DdManager const& fullDdManager, InternalBdd const& variableCube, uint_fast64_t numberOfDdVariables, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; /*! * Retrieves an iterator that points past the end of the container. * * @param fullDdManager The DD manager responsible for this ADD. - * @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(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables = true) const; + AddIterator end(DdManager const& fullDdManager) const; /*! * Composes the ADD with an explicit vector by performing a specified function between the entries of this diff --git a/src/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storage/dd/sylvan/SylvanAddIterator.cpp index f6d067b63..4322aa1b6 100644 --- a/src/storage/dd/sylvan/SylvanAddIterator.cpp +++ b/src/storage/dd/sylvan/SylvanAddIterator.cpp @@ -1,5 +1,10 @@ #include "src/storage/dd/sylvan/SylvanAddIterator.h" +#include "src/storage/dd/sylvan/InternalSylvanAdd.h" + +#include "src/storage/dd/DdManager.h" +#include "src/storage/expressions/ExpressionManager.h" + #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" @@ -10,24 +15,172 @@ namespace storm { // Intentionally left empty. } + template + AddIterator::AddIterator(DdManager const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(&ddManager), mtbdd(mtbdd), variables(variables), cube(numberOfDdVariables), leaf(), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(0), 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) { + this->createGlobalToLocalIndexMapping(); + + // And then get ready for treating the first cube. + leaf = mtbdd_enum_first(mtbdd.GetMTBDD(), variables.GetBDD(), cube.data(), &mtbdd_isnonzero); + + if (leaf != mtbdd_false) { + this->treatNewCube(); + } else { + this->isAtEnd = true; + } + } + } + + template + void AddIterator::createGlobalToLocalIndexMapping() { + // Create the global to local index mapping. + std::vector globalIndices; + for (auto const& metaVariable : *this->metaVariables) { + auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable); + + for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { + globalIndices.push_back(ddVariable.getIndex()); + } + } + + std::sort(globalIndices.begin(), globalIndices.end()); + + for (auto it = globalIndices.begin(), ite = globalIndices.end(); it != ite; ++it) { + globalToLocalIndexMap[*it] = std::distance(globalIndices.begin(), it); + } + } + + template + AddIterator AddIterator::createBeginIterator(DdManager const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, std::set const* metaVariables, bool enumerateDontCareMetaVariables) { + return AddIterator(ddManager, mtbdd, variables, numberOfDdVariables, false, metaVariables, enumerateDontCareMetaVariables); + } + + template + AddIterator AddIterator::createEndIterator(DdManager const& ddManager) { + return AddIterator(ddManager, sylvan::Mtbdd(), sylvan::Bdd(), 0, true, nullptr, false); + } + template AddIterator& AddIterator::operator++() { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + 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 + // found solutions and get the next "first" cube. + if (this->relevantDontCareDdVariables.empty() || this->cubeCounter >= std::pow(2, this->relevantDontCareDdVariables.size()) - 1) { + leaf = mtbdd_enum_next(mtbdd.GetMTBDD(), variables.GetBDD(), cube.data(), &mtbdd_isnonzero); + + if (leaf != mtbdd_false) { + this->treatNewCube(); + } else { + this->isAtEnd = true; + } + } else { + // Treat the next solution of the cube. + this->treatNextInCube(); + } + + return *this; } template bool AddIterator::operator==(AddIterator const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + if (this->isAtEnd && other.isAtEnd) { + return true; + } else { + return this->ddManager == other.ddManager && this->mtbdd == other.mtbdd && this->variables == other.variables + && this->cube == other.cube && this->leaf == other.leaf && this->isAtEnd == other.isAtEnd + && this->metaVariables == other.metaVariables && this->cubeCounter == other.cubeCounter + && this->relevantDontCareDdVariables == other.relevantDontCareDdVariables + && this->currentValuation == other.currentValuation; + } } template bool AddIterator::operator!=(AddIterator const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return !(*this == other); } template std::pair AddIterator::operator*() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return std::make_pair(currentValuation, static_cast(InternalAdd::getValue(leaf))); + } + + 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 + // don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete + // valuations later. + for (auto const& metaVariable : *this->metaVariables) { + bool metaVariableAppearsInCube = false; + std::vector> localRelenvantDontCareDdVariables; + auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable); + if (ddMetaVariable.getType() == MetaVariableType::Bool) { + if (this->cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables().front().getIndex())] == 0) { + metaVariableAppearsInCube = true; + currentValuation.setBooleanValue(metaVariable, false); + } else if (this->cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables().front().getIndex())] == 1) { + metaVariableAppearsInCube = true; + currentValuation.setBooleanValue(metaVariable, true); + } else { + localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0)); + } + } else { + int_fast64_t intValue = 0; + for (uint_fast64_t bitIndex = 0; bitIndex < ddMetaVariable.getNumberOfDdVariables(); ++bitIndex) { + if (cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables()[bitIndex].getIndex())] == 0) { + // Leave bit unset. + metaVariableAppearsInCube = true; + } else if (cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables()[bitIndex].getIndex())] == 1) { + intValue |= 1ull << (ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1); + metaVariableAppearsInCube = true; + } else { + // Temporarily leave bit unset so we can iterate trough the other option later. + // Add the bit to the relevant don't care bits. + localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1)); + } + } + if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { + currentValuation.setBitVectorValue(metaVariable, intValue + ddMetaVariable.getLow()); + } + } + + // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the + // missing bits to later enumerate all possible valuations. + if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { + relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end()); + } + } + + // Finally, reset the cube counter. + this->cubeCounter = 0; + } + + template + void AddIterator::treatNextInCube() { + // Start by increasing the counter and check which bits we need to set/unset in the new valuation. + ++this->cubeCounter; + + for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) { + auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<0>(this->relevantDontCareDdVariables[index])); + if (ddMetaVariable.getType() == MetaVariableType::Bool) { + if ((this->cubeCounter & (1ull << index)) != 0) { + currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), true); + } else { + currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), false); + } + } else { + storm::expressions::Variable const& metaVariable = std::get<0>(this->relevantDontCareDdVariables[index]); + if ((this->cubeCounter & (1ull << index)) != 0) { + currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); + } else { + currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); + } + } + } } template class AddIterator; diff --git a/src/storage/dd/sylvan/SylvanAddIterator.h b/src/storage/dd/sylvan/SylvanAddIterator.h index cbf75076c..dc3523aa0 100644 --- a/src/storage/dd/sylvan/SylvanAddIterator.h +++ b/src/storage/dd/sylvan/SylvanAddIterator.h @@ -1,9 +1,13 @@ #ifndef STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ #define STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_ +#include + #include "src/storage/dd/AddIterator.h" #include "src/storage/expressions/SimpleValuation.h" +#include "sylvan_obj.hpp" + namespace storm { namespace dd { // Forward-declare the DdManager class. @@ -61,6 +65,94 @@ namespace storm { bool operator!=(AddIterator const& other) const; private: + /*! + * Constructs a forward iterator using the given generator with the given set of relevant meta variables. + * + * @param ddManager The manager responsible for the DD over which to iterate. + * @param mtbdd The MTBDD over which to iterate. + * @param variables The variables contained in the MTBDD, represented as a cube. + * @param numberOfDdVariables The number of DD variables contained in this MTBDD. + * @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any + * more. + * @param metaVariables The meta variables that appear in the DD. + * @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. + */ + AddIterator(DdManager const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables); + + /*! + * Creates an iterator to the function argument-value-pairs of the given MTBDD. + * + * @param ddManager The manager responsible for the DD over which to iterate. + * @param mtbdd The MTBDD over which to iterate. + * @param variables The variables contained in the MTBDD, represented as a cube. + * @param numberOfDdVariables The number of DD variables contained in this MTBDD. + * @param metaVariables The meta variables that appear in the DD. + * @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. + */ + static AddIterator createBeginIterator(DdManager const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, std::set const* metaVariables, bool enumerateDontCareMetaVariables = true); + + /*! + * Creates an iterator that can be used to determine the end of the iteration process. + * + * @param ddManager The manager responsible for the DD over which to iterate. + */ + static AddIterator createEndIterator(DdManager const& ddManager); + + /*! + * Recreates the internal information when a new cube needs to be treated. + */ + void treatNewCube(); + + /*! + * Updates the internal information when the next solution of the current cube needs to be treated. + */ + void treatNextInCube(); + + /*! + * Creates the mapping of global variable indices to local ones. + */ + void createGlobalToLocalIndexMapping(); + + // The manager responsible for the meta variables (and therefore the underlying DD). + DdManager const* ddManager; + + // The MTBDD over which to iterate. + sylvan::Mtbdd mtbdd; + + // The cube of variables in the MTBDD. + sylvan::Bdd variables; + + // The currently considered cube of the DD. + std::vector cube; + + // The function value of the current cube, represented by the corresponding leaf. + MTBDD leaf; + + // A flag that indicates whether the iterator is at its end and may not be moved further. This is also used + // for the check against the end iterator. + bool isAtEnd; + + // The set of meta variables appearing in the DD. + std::set const* metaVariables; + + // A mapping from global variable indices to local (i.e. appearing the MTBDD) ones. + std::unordered_map globalToLocalIndexMap; + + // A flag that indicates whether the iterator is supposed to enumerate meta variable valuations even if + // they don't influence the function value. + bool enumerateDontCareMetaVariables; + + // A number that represents how many assignments of the current cube have already been returned previously. + // This is needed, because cubes may represent many assignments (if they have don't care variables). + uint_fast64_t cubeCounter; + + // A vector of tuples of the form . + std::vector> relevantDontCareDdVariables; + + // The current valuation of meta variables. + storm::expressions::SimpleValuation currentValuation; }; } diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index b6fd0ef8d..0c1e10278 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -189,8 +189,10 @@ namespace storm { } template class SymbolicLinearEquationSolverFactory; + template class SymbolicLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicGameSolverFactory; + template class SymbolicGameSolverFactory; template class LinearEquationSolverFactory; template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index f2974a8cd..ac29790e5 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -17,16 +17,15 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - // FIXME: re-enable as soon as sylvan ADD-iterator is done. -// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); -// model = storm::builder::DdPrismModelBuilder::translateProgram(program); -// EXPECT_EQ(677ul, model->getNumberOfStates()); -// EXPECT_EQ(867ul, model->getNumberOfTransitions()); + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(677ul, model->getNumberOfStates()); + EXPECT_EQ(867ul, model->getNumberOfTransitions()); -// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); -// model = storm::builder::DdPrismModelBuilder::translateProgram(program); -// EXPECT_EQ(8607ul, model->getNumberOfStates()); -// EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); @@ -180,16 +179,15 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); - // FIXME: re-enable after Sylvan ADD iterator is done. -// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); -// model = storm::builder::DdPrismModelBuilder::translateProgram(program); -// -// EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); -// mdp = model->as>(); -// -// EXPECT_EQ(37ul, mdp->getNumberOfStates()); -// EXPECT_EQ(59ul, mdp->getNumberOfTransitions()); -// EXPECT_EQ(59ul, mdp->getNumberOfChoices()); + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(37ul, mdp->getNumberOfStates()); + EXPECT_EQ(59ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(59ul, mdp->getNumberOfChoices()); } TEST(DdPrismModelBuilderTest_Cudd, Mdp) { diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index a91eb0d30..bb9247c67 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -17,7 +17,7 @@ #include "src/settings/modules/GeneralSettings.h" -TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { +TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); // A parser that we use for conveniently constructing the formulas. @@ -78,7 +78,68 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); } -TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { +TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + // Build the die model with its reward model. +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("coin_flips"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); // A parser that we use for conveniently constructing the formulas. @@ -122,7 +183,51 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); } -TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { +TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); // A parser that we use for conveniently constructing the formulas. @@ -174,3 +279,54 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); } +TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + // Build the die model with its reward model. +#ifdef WINDOWS + storm::builder::DdPrismModelBuilder::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("num_rounds"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); + + result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} \ No newline at end of file diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index 89a8f67b5..2cf00f1e7 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -8,7 +8,7 @@ #include "src/solver/SymbolicGameSolver.h" #include "src/settings/modules/NativeEquationSolverSettings.h" -TEST(FullySymbolicGameSolverTest, Solve) { +TEST(FullySymbolicGameSolverTest, Solve_Cudd) { // Create some variables. std::shared_ptr> manager(new storm::dd::DdManager()); std::pair state = manager->addMetaVariable("x", 1, 4); @@ -59,6 +59,64 @@ TEST(FullySymbolicGameSolverTest, Solve) { result = result.sumAbstract({state.first}); EXPECT_NEAR(0.2, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); + x = manager->getAddZero(); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b); + result *= manager->getEncoding(state.first, 1).template toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(FullySymbolicGameSolverTest, Solve_Sylvan) { + // Create some variables. + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair state = manager->addMetaVariable("x", 1, 4); + std::pair pl1 = manager->addMetaVariable("a", 0, 1); + std::pair pl2 = manager->addMetaVariable("b", 0, 1); + + storm::dd::Bdd allRows = manager->getBddZero(); + std::set rowMetaVariables({state.first}); + std::set columnMetaVariables({state.second}); + std::vector> rowColumnMetaVariablePairs = {state}; + std::set player1Variables({pl1.first}); + std::set player2Variables({pl2.first}); + + // Construct simple game. + storm::dd::Add matrix = manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 2).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.6); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 1).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.4); + + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 2).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(0.2); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 3).template toAdd() * manager->getEncoding(pl1.first, 0).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(0.8); + + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 3).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.5); + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 4).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 0).template toAdd() * manager->getConstant(0.5); + + matrix += manager->getEncoding(state.first, 1).template toAdd() * manager->getEncoding(state.second, 1).template toAdd() * manager->getEncoding(pl1.first, 1).template toAdd() * manager->getEncoding(pl2.first, 1).template toAdd() * manager->getConstant(1); + + std::unique_ptr> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory()); + std::unique_ptr> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables); + + // Create solution and target state vector. + storm::dd::Add x = manager->template getAddZero(); + storm::dd::Add b = manager->getEncoding(state.first, 2).template toAdd() + manager->getEncoding(state.first, 4).template toAdd(); + + // Now solve the game with different strategies for the players. + storm::dd::Add result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b); + result *= manager->getEncoding(state.first, 1).template toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + x = manager->getAddZero(); + result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b); + result *= manager->getEncoding(state.first, 1).template toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0.5, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + x = manager->getAddZero(); + result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b); + result *= manager->getEncoding(state.first, 1).template toAdd(); + result = result.sumAbstract({state.first}); + EXPECT_NEAR(0.2, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision()); + x = manager->getAddZero(); result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b); result *= manager->getEncoding(state.first, 1).template toAdd(); diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 86cb1db33..18742b688 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -275,7 +275,7 @@ TEST(CuddDd, GetSetValueTest) { EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap)); } -TEST(CuddDd, ForwardIteratorTest) { +TEST(CuddDd, AddIteratorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); std::pair y = manager->addMetaVariable("y", 0, 3); diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 9cf188c24..85a152cff 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -278,48 +278,49 @@ TEST(SylvanDd, GetSetValueTest) { EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap)); } -//TEST(SylvanDd, ForwardIteratorTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// std::pair x = manager->addMetaVariable("x", 1, 9); -// std::pair y = manager->addMetaVariable("y", 0, 3); -// -// storm::dd::Add dd; -// ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd()); -// -// storm::dd::AddIterator it, ite; -// ASSERT_NO_THROW(it = dd.begin()); -// ASSERT_NO_THROW(ite = dd.end()); -// std::pair valuationValuePair; -// uint_fast64_t numberOfValuations = 0; -// while (it != ite) { -// ASSERT_NO_THROW(valuationValuePair = *it); -// ASSERT_NO_THROW(++it); -// ++numberOfValuations; -// } -// EXPECT_EQ(9ul, numberOfValuations); -// -// dd = manager->getRange(x.first).template toAdd(); -// dd = dd.ite(manager->template getAddOne(), manager->template getAddOne()); -// ASSERT_NO_THROW(it = dd.begin()); -// ASSERT_NO_THROW(ite = dd.end()); -// numberOfValuations = 0; -// while (it != ite) { -// ASSERT_NO_THROW(valuationValuePair = *it); -// ASSERT_NO_THROW(++it); -// ++numberOfValuations; -// } -// EXPECT_EQ(16ul, numberOfValuations); -// -// ASSERT_NO_THROW(it = dd.begin(false)); -// ASSERT_NO_THROW(ite = dd.end()); -// numberOfValuations = 0; -// while (it != ite) { -// ASSERT_NO_THROW(valuationValuePair = *it); -// ASSERT_NO_THROW(++it); -// ++numberOfValuations; -// } -// EXPECT_EQ(1ul, numberOfValuations); -//} +TEST(SylvanDd, AddIteratorTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + std::pair y = manager->addMetaVariable("y", 0, 3); + + storm::dd::Add dd; + ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd()); + + storm::dd::AddIterator it, ite; + ASSERT_NO_THROW(it = dd.begin()); + ASSERT_NO_THROW(ite = dd.end()); + std::pair valuationValuePair; + uint_fast64_t numberOfValuations = 0; + dd.exportToDot("dd.dot"); + while (it != ite) { + ASSERT_NO_THROW(valuationValuePair = *it); + ASSERT_NO_THROW(++it); + ++numberOfValuations; + } + EXPECT_EQ(9ul, numberOfValuations); + + dd = manager->getRange(x.first).template toAdd(); + dd = dd.ite(manager->template getAddOne(), manager->template getAddOne()); + ASSERT_NO_THROW(it = dd.begin()); + ASSERT_NO_THROW(ite = dd.end()); + numberOfValuations = 0; + while (it != ite) { + ASSERT_NO_THROW(valuationValuePair = *it); + ASSERT_NO_THROW(++it); + ++numberOfValuations; + } + EXPECT_EQ(16ul, numberOfValuations); + + ASSERT_NO_THROW(it = dd.begin(false)); + ASSERT_NO_THROW(ite = dd.end()); + numberOfValuations = 0; + while (it != ite) { + ASSERT_NO_THROW(valuationValuePair = *it); + ASSERT_NO_THROW(++it); + ++numberOfValuations; + } + EXPECT_EQ(1ul, numberOfValuations); +} TEST(SylvanDd, AddOddTest) { std::shared_ptr> manager(new storm::dd::DdManager()); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 726dc2dc2..b337b0ca9 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -36,8 +36,7 @@ TEST(GraphTest, SymbolicProb01_Cudd) { EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount()); } -// FIXME: re-enable as soon as the ADD iterator of sylvan works. -TEST(DISABLED_GraphTest, SymbolicProb01_Sylvan) { +TEST(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> model = storm::builder::DdPrismModelBuilder::translateProgram(program);