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

lifted representative generation from ADDs to BDDs

main
dehnert 8 years ago
parent
722cb3109c
commit
f55fab0924
1 changed files with 39 additions and 38 deletions
Unified View
  1. 77
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

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

@ -33,25 +33,21 @@ namespace storm {
namespace dd { namespace dd {
namespace bisimulation { namespace bisimulation {
template<storm::dd::DdType DdType, typename ValueType> template<storm::dd::DdType DdType>
class InternalRepresentativeComputer; class InternalRepresentativeComputer;
template<storm::dd::DdType DdType, typename ValueType> template<storm::dd::DdType DdType>
class InternalRepresentativeComputerBase { class InternalRepresentativeComputerBase {
public: public:
InternalRepresentativeComputerBase(Partition<DdType, ValueType> const& partition, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables) : partition(partition), rowVariables(rowVariables), columnVariables(columnVariables) { InternalRepresentativeComputerBase(storm::dd::Bdd<DdType> const& partitionBdd, std::set<storm::expressions::Variable> const& rowVariables) : rowVariables(rowVariables), partitionBdd(partitionBdd) {
if (partition.storedAsAdd()) { ddManager = &partitionBdd.getDdManager();
ddManager = &partition.asAdd().getDdManager();
} else {
ddManager = &partition.asBdd().getDdManager();
}
internalDdManager = &ddManager->getInternalDdManager(); internalDdManager = &ddManager->getInternalDdManager();
// Create state variables cube. // Create state variables cube.
this->columnVariablesCube = ddManager->getBddOne(); this->rowVariablesCube = ddManager->getBddOne();
for (auto const& var : columnVariables) { for (auto const& var : rowVariables) {
auto const& metaVariable = ddManager->getMetaVariable(var); auto const& metaVariable = ddManager->getMetaVariable(var);
this->columnVariablesCube &= metaVariable.getCube(); this->rowVariablesCube &= metaVariable.getCube();
} }
} }
@ -59,27 +55,27 @@ namespace storm {
storm::dd::DdManager<DdType> const* ddManager; storm::dd::DdManager<DdType> const* ddManager;
storm::dd::InternalDdManager<DdType> const* internalDdManager; storm::dd::InternalDdManager<DdType> const* internalDdManager;
Partition<DdType, ValueType> const& partition;
std::set<storm::expressions::Variable> const& rowVariables; std::set<storm::expressions::Variable> const& rowVariables;
std::set<storm::expressions::Variable> const& columnVariables; storm::dd::Bdd<DdType> rowVariablesCube;
storm::dd::Bdd<DdType> columnVariablesCube; storm::dd::Bdd<DdType> partitionBdd;
}; };
template<typename ValueType> template <>
class InternalRepresentativeComputer<storm::dd::DdType::CUDD, ValueType> : public InternalRepresentativeComputerBase<storm::dd::DdType::CUDD, ValueType> { class InternalRepresentativeComputer<storm::dd::DdType::CUDD> : public InternalRepresentativeComputerBase<storm::dd::DdType::CUDD> {
public: public:
InternalRepresentativeComputer(Partition<storm::dd::DdType::CUDD, ValueType> const& partition, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables) : InternalRepresentativeComputerBase<storm::dd::DdType::CUDD, ValueType>(partition, rowVariables, columnVariables) { InternalRepresentativeComputer(storm::dd::Bdd<storm::dd::DdType::CUDD> const& partitionBdd, std::set<storm::expressions::Variable> const& rowVariables) : InternalRepresentativeComputerBase<storm::dd::DdType::CUDD>(partitionBdd, rowVariables) {
this->ddman = this->internalDdManager->getCuddManager().getManager(); this->ddman = this->internalDdManager->getCuddManager().getManager();
} }
storm::dd::Bdd<storm::dd::DdType::CUDD> getRepresentatives() { storm::dd::Bdd<storm::dd::DdType::CUDD> getRepresentatives() {
return storm::dd::Bdd<storm::dd::DdType::CUDD>(*this->ddManager, storm::dd::InternalBdd<storm::dd::DdType::CUDD>(this->internalDdManager, cudd::BDD(this->internalDdManager->getCuddManager(), this->getRepresentativesRec(this->partition.asAdd().getInternalAdd().getCuddDdNode(), this->columnVariablesCube.getInternalBdd().getCuddDdNode()))), this->rowVariables); return storm::dd::Bdd<storm::dd::DdType::CUDD>(*this->ddManager, storm::dd::InternalBdd<storm::dd::DdType::CUDD>(this->internalDdManager, cudd::BDD(this->internalDdManager->getCuddManager(), this->getRepresentativesRec(this->partitionBdd.getInternalBdd().getCuddDdNode(), this->rowVariablesCube.getInternalBdd().getCuddDdNode()))), this->rowVariables);
} }
private: private:
DdNodePtr getRepresentativesRec(DdNodePtr partitionNode, DdNodePtr stateVariablesCube) { DdNodePtr getRepresentativesRec(DdNodePtr partitionNode, DdNodePtr stateVariablesCube) {
if (partitionNode == Cudd_ReadZero(ddman)) { if (partitionNode == Cudd_ReadLogicZero(ddman)) {
return Cudd_ReadLogicZero(ddman); return partitionNode;
} }
// If we visited the node before, there is no block that we still need to cover. // If we visited the node before, there is no block that we still need to cover.
@ -98,6 +94,11 @@ namespace storm {
if (Cudd_NodeReadIndex(partitionNode) == Cudd_NodeReadIndex(stateVariablesCube)) { if (Cudd_NodeReadIndex(partitionNode) == Cudd_NodeReadIndex(stateVariablesCube)) {
elsePartitionNode = Cudd_E(partitionNode); elsePartitionNode = Cudd_E(partitionNode);
thenPartitionNode = Cudd_T(partitionNode); thenPartitionNode = Cudd_T(partitionNode);
if (Cudd_IsComplement(partitionNode)) {
elsePartitionNode = Cudd_Not(elsePartitionNode);
thenPartitionNode = Cudd_Not(thenPartitionNode);
}
} else { } else {
elsePartitionNode = thenPartitionNode = partitionNode; elsePartitionNode = thenPartitionNode = partitionNode;
skipped = true; skipped = true;
@ -122,7 +123,7 @@ namespace storm {
return elseResult; return elseResult;
} else { } else {
bool complement = Cudd_IsComplement(thenResult); bool complement = Cudd_IsComplement(thenResult);
auto result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(stateVariablesCube) - 1, Cudd_Regular(thenResult), complement ? Cudd_Not(elseResult) : elseResult); auto result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(stateVariablesCube), Cudd_Regular(thenResult), complement ? Cudd_Not(elseResult) : elseResult);
Cudd_Deref(elseResult); Cudd_Deref(elseResult);
Cudd_Deref(thenResult); Cudd_Deref(thenResult);
return complement ? Cudd_Not(result) : result; return complement ? Cudd_Not(result) : result;
@ -132,7 +133,7 @@ namespace storm {
if (elseResult == Cudd_ReadLogicZero(ddman)) { if (elseResult == Cudd_ReadLogicZero(ddman)) {
result = elseResult; result = elseResult;
} else { } else {
result = Cudd_Not(cuddUniqueInter(ddman, Cudd_NodeReadIndex(stateVariablesCube) - 1, Cudd_ReadOne(ddman), Cudd_Not(elseResult))); result = Cudd_Not(cuddUniqueInter(ddman, Cudd_NodeReadIndex(stateVariablesCube), Cudd_ReadOne(ddman), Cudd_Not(elseResult)));
} }
Cudd_Deref(elseResult); Cudd_Deref(elseResult);
return result; return result;
@ -144,15 +145,15 @@ namespace storm {
spp::sparse_hash_map<DdNode const*, bool> visitedNodes; spp::sparse_hash_map<DdNode const*, bool> visitedNodes;
}; };
template<typename ValueType> template<>
class InternalRepresentativeComputer<storm::dd::DdType::Sylvan, ValueType> : public InternalRepresentativeComputerBase<storm::dd::DdType::Sylvan, ValueType> { class InternalRepresentativeComputer<storm::dd::DdType::Sylvan> : public InternalRepresentativeComputerBase<storm::dd::DdType::Sylvan> {
public: public:
InternalRepresentativeComputer(Partition<storm::dd::DdType::Sylvan, ValueType> const& partition, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables) : InternalRepresentativeComputerBase<storm::dd::DdType::Sylvan, ValueType>(partition, rowVariables, columnVariables) { InternalRepresentativeComputer(storm::dd::Bdd<storm::dd::DdType::Sylvan> const& partitionBdd, std::set<storm::expressions::Variable> const& rowVariables) : InternalRepresentativeComputerBase<storm::dd::DdType::Sylvan>(partitionBdd, rowVariables) {
// Intentionally left empty. // Intentionally left empty.
} }
storm::dd::Bdd<storm::dd::DdType::Sylvan> getRepresentatives() { storm::dd::Bdd<storm::dd::DdType::Sylvan> getRepresentatives() {
return storm::dd::Bdd<storm::dd::DdType::Sylvan>(*this->ddManager, storm::dd::InternalBdd<storm::dd::DdType::Sylvan>(this->internalDdManager, sylvan::Bdd(this->getRepresentativesRec(this->partition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), this->columnVariablesCube.getInternalBdd().getSylvanBdd().GetBDD()))), this->rowVariables); return storm::dd::Bdd<storm::dd::DdType::Sylvan>(*this->ddManager, storm::dd::InternalBdd<storm::dd::DdType::Sylvan>(this->internalDdManager, sylvan::Bdd(this->getRepresentativesRec(this->partitionBdd.getInternalBdd().getSylvanBdd().GetBDD(), this->rowVariablesCube.getInternalBdd().getSylvanBdd().GetBDD()))), this->rowVariables);
} }
private: private:
@ -199,7 +200,7 @@ namespace storm {
mtbdd_refs_pop(2); mtbdd_refs_pop(2);
return elseResult; return elseResult;
} else { } else {
auto result = sylvan_makenode(sylvan_var(stateVariablesCube) - 1, elseResult, thenResult); auto result = sylvan_makenode(sylvan_var(stateVariablesCube), elseResult, thenResult);
mtbdd_refs_pop(2); mtbdd_refs_pop(2);
return result; return result;
} }
@ -208,7 +209,7 @@ namespace storm {
if (elseResult == sylvan_false) { if (elseResult == sylvan_false) {
result = elseResult; result = elseResult;
} else { } else {
result = sylvan_makenode(sylvan_var(stateVariablesCube) - 1, elseResult, sylvan_false); result = sylvan_makenode(sylvan_var(stateVariablesCube), elseResult, sylvan_false);
} }
mtbdd_refs_pop(1); mtbdd_refs_pop(1);
return result; return result;
@ -718,8 +719,8 @@ namespace storm {
partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
auto start = std::chrono::high_resolution_clock::now(); auto start = std::chrono::high_resolution_clock::now();
// FIXME: Use partition as BDD in representative computation. auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
auto representatives = InternalRepresentativeComputer<DdType, ValueType>(partition, model.getRowVariables(), model.getColumnVariables()).getRepresentatives(); representatives.template toAdd<ValueType>().exportToDot("repr.dot");
STORM_LOG_ASSERT(representatives.getNonZeroCount() == partition.getNumberOfBlocks(), "Representatives size does not match that of the partition: " << representatives.getNonZeroCount() << " vs. " << partition.getNumberOfBlocks() << "."); STORM_LOG_ASSERT(representatives.getNonZeroCount() == partition.getNumberOfBlocks(), "Representatives size does not match that of the partition: " << representatives.getNonZeroCount() << " vs. " << partition.getNumberOfBlocks() << ".");
STORM_LOG_ASSERT((representatives && partitionAsBdd).existsAbstract(model.getRowVariables()) == partitionAsBdd.existsAbstract(model.getRowVariables()), "Representatives do not cover all blocks."); STORM_LOG_ASSERT((representatives && partitionAsBdd).existsAbstract(model.getRowVariables()) == partitionAsBdd.existsAbstract(model.getRowVariables()), "Representatives do not cover all blocks.");
InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model, partition, representatives); InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model, partition, representatives);
@ -795,13 +796,13 @@ namespace storm {
} }
auto start = std::chrono::high_resolution_clock::now(); auto start = std::chrono::high_resolution_clock::now();
storm::dd::Bdd<DdType> partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables()); storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables());
storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables()); storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables());
std::map<std::string, storm::dd::Bdd<DdType>> preservedLabelBdds; std::map<std::string, storm::dd::Bdd<DdType>> preservedLabelBdds;
for (auto const& label : preservationInformation.getLabels()) { for (auto const& label : preservationInformation.getLabels()) {
preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBdd).existsAbstract(model.getRowVariables()));
} }
for (auto const& expression : preservationInformation.getExpressions()) { for (auto const& expression : preservationInformation.getExpressions()) {
std::stringstream stream; std::stringstream stream;
@ -812,18 +813,18 @@ namespace storm {
if (it != preservedLabelBdds.end()) { if (it != preservedLabelBdds.end()) {
STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition."); STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition.");
} else { } else {
preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBdd).existsAbstract(model.getRowVariables()));
} }
} }
auto end = std::chrono::high_resolution_clock::now(); auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms."); STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
start = std::chrono::high_resolution_clock::now(); start = std::chrono::high_resolution_clock::now();
storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables()); storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet).renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables());
// Pick a representative from each block. // Pick a representative from each block.
auto representatives = InternalRepresentativeComputer<DdType, ValueType>(partition, model.getRowVariables(), model.getColumnVariables()).getRepresentatives(); auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
partitionAsBdd = representatives && partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); partitionAsBdd &= representatives;
storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>(); storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()); quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables());

Write Preview
|||||||
100:0
Loading…
Cancel
Save