sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

workaround for quotient extraction using the original variables

main
dehnert 8 years ago
parent
10f8ddc343
commit
27d6e48dad
5 changed files with 42 additions and 37 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/storm/storage/dd/Add.cpp
  2. 4
      src/storm/storage/dd/Bdd.cpp
  3. 41
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  4. 1
      src/storm/storage/dd/cudd/InternalCuddAdd.cpp
  5. 23
      src/test/storm/storage/CuddDdTest.cpp

10
src/storm/storage/dd/Add.cpp
View File

@ -241,28 +241,28 @@ namespace storm {
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
fromBdds.push_back(ddVariable.getInternalBdd()); 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<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
for (auto const& metaVariable : to) { for (auto const& metaVariable : to) {
STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present."); STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present.");
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable); DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) { for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
toBdds.push_back(ddVariable.getInternalBdd()); 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<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
std::set<storm::expressions::Variable> newContainedMetaVariables = to; std::set<storm::expressions::Variable> newContainedMetaVariables = to;
std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); 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()) { if (fromBdds.size() == toBdds.size()) {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables); return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables);
} else { } else {
InternalBdd<LibraryType> cube = this->getDdManager().getBddOne().getInternalBdd(); InternalBdd<LibraryType> 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]; cube &= fromBdds[index];
} }
fromBdds.resize(toBdds.size()); fromBdds.resize(toBdds.size());

4
src/storm/storage/dd/Bdd.cpp
View File

@ -344,11 +344,13 @@ namespace storm {
std::set<storm::expressions::Variable> newContainedMetaVariables = to; std::set<storm::expressions::Variable> newContainedMetaVariables = to;
std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin())); 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()) { if (fromBdds.size() == toBdds.size()) {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables); return Bdd<LibraryType>(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
} else { } else {
InternalBdd<LibraryType> cube = this->getDdManager().getBddOne().getInternalBdd(); InternalBdd<LibraryType> 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]; cube &= fromBdds[index];
} }
fromBdds.resize(toBdds.size()); fromBdds.resize(toBdds.size());

41
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -1090,35 +1090,19 @@ namespace storm {
std::set<storm::expressions::Variable> blockPrimeAndColumnVariables; std::set<storm::expressions::Variable> blockPrimeAndColumnVariables;
std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end())); std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end()));
storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>(); storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> 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<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables()).renameVariablesAbstract(blockVariableSet, model.getColumnVariables());
// Pick a representative from each block. // Pick a representative from each block.
auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives(); auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
partitionAsBdd &= representatives; partitionAsBdd &= representatives;
partitionAsAdd *= partitionAsBdd.template toAdd<ValueType>();
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<ValueType>();
// 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(); end = std::chrono::high_resolution_clock::now();
// Check quotient matrix for sanity. // Check quotient matrix for sanity.
@ -1127,9 +1111,6 @@ namespace storm {
} else { } else {
STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(1e-6)).isZero(), "Illegal entries in quotient matrix."); STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(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<ValueType>().exportToDot("trans2.dot");
STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd<ValueType>(), storm::utility::convertNumber<ValueType>(1e-6)), "Illegal probabilistic matrix."); STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd<ValueType>(), storm::utility::convertNumber<ValueType>(1e-6)), "Illegal probabilistic matrix.");
STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms."); STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
@ -1160,11 +1141,11 @@ namespace storm {
if (modelType == storm::models::ModelType::Dtmc) { if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels)); return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Ctmc) { } else if (modelType == storm::models::ModelType::Ctmc) {
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Mdp) { } else if (modelType == storm::models::ModelType::Mdp) {
return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
} else { } else {
return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
} }
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");

1
src/storm/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -202,7 +202,6 @@ namespace storm {
for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
fromAdd.push_back(it1->getCuddBdd().Add()); fromAdd.push_back(it1->getCuddBdd().Add());
toAdd.push_back(it2->getCuddBdd().Add()); toAdd.push_back(it2->getCuddBdd().Add());
std::cout << fromAdd.back().NodeReadIndex() << " <-> " << toAdd.back().NodeReadIndex() << std::endl;
} }
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd));
} }

23
src/test/storm/storage/CuddDdTest.cpp
View File

@ -589,6 +589,29 @@ TEST(CuddDd, MultiplyMatrixTest) {
EXPECT_TRUE(dd3 == dd2 * manager->template getConstant<double>(2)); EXPECT_TRUE(dd3 == dd2 * manager->template getConstant<double>(2));
} }
TEST(CuddDd, MultiplyMatrixTest2) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 0, 2);
std::pair<storm::expressions::Variable, storm::expressions::Variable> b = manager->addMetaVariable("b", 0, 2);
storm::dd::Add<storm::dd::DdType::CUDD, double> p = manager->getAddZero<double>();
p += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(b.first, 0, true)).template toAdd<double>();
p += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(b.first, 2, true)).template toAdd<double>();
storm::dd::Add<storm::dd::DdType::CUDD, double> q = manager->getAddZero<double>();
q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() * manager->template getConstant<double>(0.3);
q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() * manager->template getConstant<double>(0.3);
q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 2, true)).template toAdd<double>() * manager->template getConstant<double>(0.7);
q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 2, true)).template toAdd<double>() * manager->template getConstant<double>(0.7);
q += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() * manager->template getConstant<double>(1);
storm::dd::Add<storm::dd::DdType::CUDD, double> r = q.multiplyMatrix(p, {x.first});
ASSERT_EQ(12, r.getNodeCount());
ASSERT_EQ(4, r.getLeafCount());
ASSERT_EQ(3, r.getNonZeroCount());
}
TEST(CuddDd, GetSetValueTest) { TEST(CuddDd, GetSetValueTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>()); std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9); std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);

Write Preview
Loading…
Cancel
Save