diff --git a/CHANGELOG.md b/CHANGELOG.md index 56004ed4f..75d2a807c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ Long run average computation via ValueIteration, LP based MDP model checking, pa - c++ api changes: Building model takes BuilderOptions instead of extended list of Booleans, does not depend on settings anymore. - storm-cli-utilities now contains cli related stuff, instead of storm-lib - storm-pars: support for welldefinedness constraints in mdps. +- symbolic (MT/BDD) bisimulation ### Version 1.1.0 (2017/8) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index fb92720d0..09fb51ccf 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -125,6 +125,8 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) { std::lock_guard lock(rationalNumberMutex); #endif + std::cout << "got ptr for eq check " << a << std::endl; + return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0; } diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index d12f1f420..75fe87254 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -63,12 +63,10 @@ namespace storm { std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { auto const& coreSettings = storm::settings::getModule(); - storm::solver::EquationSolverType equationSolver; - if (coreSettings.isEquationSolverSetFromDefaultValue()) { + storm::solver::EquationSolverType equationSolver = coreSettings.getEquationSolver(); + if (coreSettings.isEquationSolverSetFromDefaultValue() && equationSolver != storm::solver::EquationSolverType::Elimination) { STORM_LOG_WARN("Selecting the elimination solver to guarantee exact results. If you want to override this, please explicitly specify a different equation solver."); equationSolver = storm::solver::EquationSolverType::Elimination; - } else { - equationSolver = coreSettings.getEquationSolver(); } if (equationSolver != storm::solver::EquationSolverType::Elimination) { diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index feaeb4313..6385c1d93 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -175,7 +175,7 @@ namespace storm { bool skipped = false; BDD elsePartitionNode; BDD thenPartitionNode; - if (sylvan_var(partitionNode) == sylvan_var(stateVariablesCube)) { + if (storm::dd::InternalBdd::matchesVariableIndex(partitionNode, sylvan_var(stateVariablesCube))) { elsePartitionNode = sylvan_low(partitionNode); thenPartitionNode = sylvan_high(partitionNode); } else { @@ -652,7 +652,7 @@ namespace storm { } else { MTBDD vectorT; MTBDD vectorE; - if (sylvan_var(vector) == sylvan_var(variables)) { + if (storm::dd::InternalAdd::matchesVariableIndex(vector, sylvan_var(variables))) { vectorT = sylvan_high(vector); vectorE = sylvan_low(vector); } else { @@ -661,7 +661,7 @@ namespace storm { BDD representativesT; BDD representativesE; - if (sylvan_var(representativesNode) == sylvan_var(variables)) { + if (storm::dd::InternalBdd::matchesVariableIndex(representativesNode, sylvan_var(variables))) { representativesT = sylvan_high(representativesNode); representativesE = sylvan_low(representativesNode); } else { @@ -692,7 +692,7 @@ namespace storm { STORM_LOG_ASSERT(!odd.isTerminalNode(), "Expected non-terminal node."); BDD partitionT; BDD partitionE; - if (sylvan_var(partitionNode) == sylvan_var(variables)) { + if (storm::dd::InternalBdd::matchesVariableIndex(partitionNode, sylvan_var(variables))) { partitionT = sylvan_high(partitionNode); partitionE = sylvan_low(partitionNode); } else { @@ -701,7 +701,7 @@ namespace storm { BDD representativesT; BDD representativesE; - if (sylvan_var(representativesNode) == sylvan_var(variables)) { + if (storm::dd::InternalBdd::matchesVariableIndex(representativesNode, sylvan_var(variables))) { representativesT = sylvan_high(representativesNode); representativesE = sylvan_low(representativesNode); } else { @@ -714,6 +714,7 @@ namespace storm { } void extractTransitionMatrixRec(MTBDD transitionMatrixNode, storm::dd::Odd const& sourceOdd, uint64_t sourceOffset, BDD targetPartitionNode, BDD representativesNode, BDD variables, BDD nondeterminismVariables, storm::dd::Odd const* stateOdd, uint64_t stateOffset) { + // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero // as all states of the model have to be contained. if (mtbdd_iszero(transitionMatrixNode) || representativesNode == sylvan_false) { @@ -736,7 +737,7 @@ namespace storm { MTBDD e; // Determine whether the variable was skipped in the matrix. - if (sylvan_var(transitionMatrixNode) == sylvan_var(variables)) { + if (storm::dd::InternalAdd::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) { t = sylvan_high(transitionMatrixNode); e = sylvan_low(transitionMatrixNode); } else { @@ -753,7 +754,7 @@ namespace storm { MTBDD e; MTBDD et; MTBDD ee; - if (sylvan_var(transitionMatrixNode) == sylvan_var(variables)) { + if (storm::dd::InternalAdd::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) { // Source node was not skipped in transition matrix. t = sylvan_high(transitionMatrixNode); e = sylvan_low(transitionMatrixNode); @@ -761,7 +762,7 @@ namespace storm { t = e = transitionMatrixNode; } - if (sylvan_var(t) == sylvan_var(variables) + 1) { + if (storm::dd::InternalAdd::matchesVariableIndex(t, sylvan_var(variables) + 1)) { // Target node was not skipped in transition matrix. tt = sylvan_high(t); te = sylvan_low(t); @@ -770,7 +771,7 @@ namespace storm { tt = te = t; } if (t != e) { - if (sylvan_var(e) == sylvan_var(variables) + 1) { + if (storm::dd::InternalAdd::matchesVariableIndex(e, sylvan_var(variables) + 1)) { // Target node was not skipped in transition matrix. et = sylvan_high(e); ee = sylvan_low(e); @@ -785,7 +786,7 @@ namespace storm { BDD targetT; BDD targetE; - if (sylvan_var(targetPartitionNode) == sylvan_var(variables)) { + if (storm::dd::InternalBdd::matchesVariableIndex(targetPartitionNode, sylvan_var(variables))) { // Node was not skipped in target partition. targetT = sylvan_high(targetPartitionNode); targetE = sylvan_low(targetPartitionNode); @@ -796,7 +797,7 @@ namespace storm { BDD representativesT; BDD representativesE; - if (sylvan_var(representativesNode) == sylvan_var(variables)) { + if (storm::dd::InternalBdd::matchesVariableIndex(representativesNode, sylvan_var(variables))) { // Node was not skipped in representatives. representativesT = sylvan_high(representativesNode); representativesE = sylvan_low(representativesNode); diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index 59ea80db0..3dcb5a5b9 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -371,7 +371,7 @@ namespace storm { offset = 0; } - if (sylvan_var(partitionNode) - offset == sylvan_var(nonBlockVariablesNode)) { + if (storm::dd::InternalAdd::matchesVariableIndex(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { partitionThen = sylvan_high(partitionNode); partitionElse = sylvan_low(partitionNode); skippedBoth = false; @@ -379,7 +379,7 @@ namespace storm { partitionThen = partitionElse = partitionNode; } - if (sylvan_var(signatureNode) == sylvan_var(nonBlockVariablesNode)) { + if (storm::dd::InternalAdd::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) { signatureThen = sylvan_high(signatureNode); signatureElse = sylvan_low(signatureNode); skippedBoth = false; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 47b5ffa8d..46167f116 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -81,6 +81,11 @@ namespace storm { } #endif + template + bool InternalAdd::matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset) { + return !mtbdd_isleaf(node) && static_cast(sylvan_var(node) + offset) == variableIndex; + } + template bool InternalAdd::operator==(InternalAdd const& other) const { return this->sylvanMtbdd == other.sylvanMtbdd; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 687d829af..201048b6f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -612,6 +612,16 @@ namespace storm { */ static ValueType getValue(MTBDD const& node); + /*! + * Retrieves whether the topmost variable in the MTBDD is the one with the given index. + * + * @param The top node of the MTBDD. + * @param variableIndex The variable index. + * @param offset An offset that is applied to the index of the top variable in the MTBDD. + * @return True iff the MTBDD's top variable has the given index. + */ + static bool matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset = 0); + private: /*! * Recursively builds the ODD from an ADD. diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 6868b6972..00e12dfdb 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -283,7 +283,7 @@ namespace storm { // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentRowLevel == maxLevel) { result.set(currentRowOffset, true); - } else if (ddRowVariableIndices[currentRowLevel] < sylvan_var(dd)) { + } else if (bdd_isterminal(dd) || ddRowVariableIndices[currentRowLevel] < sylvan_var(dd)) { toVectorRec(dd, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); toVectorRec(dd, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); } else { @@ -390,7 +390,7 @@ namespace storm { if (currentLevel == maxLevel) { result[currentIndex++] = values[currentOffset]; - } else if (ddVariableIndices[currentLevel] < sylvan_var(dd)) { + } else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) { // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set // and for the one in which it is not set. filterExplicitVectorRec(dd, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values); @@ -424,7 +424,7 @@ namespace storm { if (currentLevel == maxLevel) { result.set(currentIndex++, values.get(currentOffset)); - } else if (ddVariableIndices[currentLevel] < sylvan_var(dd)) { + } else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) { // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set // and for the one in which it is not set. filterExplicitVectorRec(dd, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values); @@ -527,6 +527,10 @@ namespace storm { return newNodeVariable; } + bool InternalBdd::matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset) { + return !sylvan_isconst(node) && static_cast(sylvan_var(node) + offset) == variableIndex; + } + template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index 54371a3c3..6c07449c7 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -374,6 +374,16 @@ namespace storm { */ void filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const; + /*! + * Retrieves whether the topmost variable in the BDD is the one with the given index. + * + * @param The top node of the BDD. + * @param variableIndex The variable index. + * @param offset An offset that is applied to the index of the top variable in the BDD. + * @return True iff the BDD's top variable has the given index. + */ + static bool matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset = 0); + friend struct std::hash>; /*!