diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 91a00a497..9e91b2123 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -241,28 +241,28 @@ namespace storm { DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { fromBdds.push_back(ddVariable.getInternalBdd()); - std::cout << "from - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl; } } -// std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); for (auto const& metaVariable : to) { STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); DdMetaVariable const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { toBdds.push_back(ddVariable.getInternalBdd()); - std::cout << "to - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl; } } -// std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); + std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd const& a, InternalBdd const& b) { return a.getLevel() < b.getLevel(); } ); std::set newContainedMetaVariables = to; std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); + STORM_LOG_ASSERT(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes."); + if (fromBdds.size() == toBdds.size()) { return Add(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables); } else { InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); - for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) { + for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) { cube &= fromBdds[index]; } fromBdds.resize(toBdds.size()); diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index f1fee9ab6..d17bbd3d4 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -344,11 +344,13 @@ namespace storm { std::set newContainedMetaVariables = to; std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); + STORM_LOG_ASSERT(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes."); + if (fromBdds.size() == toBdds.size()) { return Bdd(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); } else { InternalBdd cube = this->getDdManager().getBddOne().getInternalBdd(); - for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) { + for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) { cube &= fromBdds[index]; } fromBdds.resize(toBdds.size()); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index dd1ce6d6b..e28c80aaa 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -1090,35 +1090,19 @@ namespace storm { std::set blockPrimeAndColumnVariables; std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end())); storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); - storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables()); - (model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables())).exportToDot("tmp0.dot"); - quotientTransitionMatrix.exportToDot("tmp1.dot"); - std::cout << "q1 size: " << quotientTransitionMatrix.getNodeCount() << ", " << quotientTransitionMatrix.getNonZeroCount() << std::endl; - quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("tmp1_1.dot"); -// quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("tmp1_1.dot"); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables()).renameVariablesAbstract(blockVariableSet, model.getColumnVariables()); // Pick a representative from each block. auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); partitionAsBdd &= representatives; - partitionAsAdd *= partitionAsBdd.template toAdd(); - partitionAsAdd.exportToDot("partrepr.dot"); - partitionAsAdd.sumAbstract(model.getRowVariables()).exportToDot("part2.dot"); - std::cout << "part size " << partitionAsAdd.getNodeCount() << ", " << partitionAsAdd.getNonZeroCount() << std::endl; - - auto tmp1 = partitionAsAdd.multiplyMatrix(quotientTransitionMatri, model.getRowVariables()); - auto tmp2 = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables()); - std::cout << "size1: " << tmp1.getNodeCount() << ", " << tmp1.getNonZeroCount() << std::endl; - std::cout << "size2: " << tmp2.getNodeCount() << ", " << tmp2.getNonZeroCount() << std::endl; - if (tmp1 != tmp2) { - tmp1.exportToDot("tmp1__.dot"); - tmp2.exportToDot("tmp2__.dot"); - (tmp2-tmp1).exportToDot("diff.dot"); - STORM_LOG_ASSERT(false, "error"); + partitionAsAdd = partitionAsBdd.template toAdd(); + + // Workaround for problem with CUDD. Matrix-Matrix multiplication yields other result than multiplication+sum-abstract... + if (DdType == storm::dd::DdType::CUDD) { + quotientTransitionMatrix = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); + } else { + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); } - quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).exportToDot("tmp2.dot"); - quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(model.getColumnVariables()).exportToDot("tmp2_2.dot"); -// quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(blockPrimeVariableSet).exportToDot("tmp2_2.dot"); - quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()); end = std::chrono::high_resolution_clock::now(); // Check quotient matrix for sanity. @@ -1127,9 +1111,6 @@ namespace storm { } else { STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one() + storm::utility::convertNumber(1e-6)).isZero(), "Illegal entries in quotient matrix."); } - quotientTransitionMatrix.exportToDot("trans.dot"); - quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("trans1.dot"); - quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd().exportToDot("trans2.dot"); STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd(), storm::utility::convertNumber(1e-6)), "Illegal probabilistic matrix."); STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); @@ -1160,11 +1141,11 @@ namespace storm { if (modelType == storm::models::ModelType::Dtmc) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); } else if (modelType == storm::models::ModelType::Ctmc) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); } else if (modelType == storm::models::ModelType::Mdp) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); } else { - return std::shared_ptr>(new storm::models::symbolic::MarkovAutomaton(model.getManager().asSharedPointer(), model. template as>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); + return std::shared_ptr>(new storm::models::symbolic::MarkovAutomaton(model.getManager().asSharedPointer(), model. template as>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 158060519..11c6b12ca 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -202,7 +202,6 @@ namespace storm { for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromAdd.push_back(it1->getCuddBdd().Add()); toAdd.push_back(it2->getCuddBdd().Add()); - std::cout << fromAdd.back().NodeReadIndex() << " <-> " << toAdd.back().NodeReadIndex() << std::endl; } return InternalAdd(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); } diff --git a/src/test/storm/storage/CuddDdTest.cpp b/src/test/storm/storage/CuddDdTest.cpp index 499be2a12..bc6ffab10 100644 --- a/src/test/storm/storage/CuddDdTest.cpp +++ b/src/test/storm/storage/CuddDdTest.cpp @@ -589,6 +589,29 @@ TEST(CuddDd, MultiplyMatrixTest) { EXPECT_TRUE(dd3 == dd2 * manager->template getConstant(2)); } +TEST(CuddDd, MultiplyMatrixTest2) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 0, 2); + std::pair b = manager->addMetaVariable("b", 0, 2); + + storm::dd::Add p = manager->getAddZero(); + p += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(b.first, 0, true)).template toAdd(); + p += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(b.first, 2, true)).template toAdd(); + + storm::dd::Add q = manager->getAddZero(); + q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(0.3); + q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(0.3); + q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 2, true)).template toAdd() * manager->template getConstant(0.7); + q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 2, true)).template toAdd() * manager->template getConstant(0.7); + q += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(x.second, 0, true)).template toAdd() * manager->template getConstant(1); + + storm::dd::Add r = q.multiplyMatrix(p, {x.first}); + + ASSERT_EQ(12, r.getNodeCount()); + ASSERT_EQ(4, r.getLeafCount()); + ASSERT_EQ(3, r.getNonZeroCount()); +} + TEST(CuddDd, GetSetValueTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9);