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

faster block encoding for CUDD; optimizations in sparse quotient extraction

tempestpy_adaptions
dehnert 7 years ago
parent
75ec21b1d6
commit
7e723b2b8f
4 changed files with 119 additions and 29 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 32
      src/storm/storage/dd/DdMetaVariable.cpp
  2. 19
      src/storm/storage/dd/DdMetaVariable.h
  3. 57
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  4. 40
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

32
src/storm/storage/dd/DdMetaVariable.cpp
View File

@ -5,12 +5,13 @@
namespace storm {
namespace dd {
template<DdType LibraryType>
DdMetaVariable<LibraryType>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables) {
DdMetaVariable<LibraryType>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), lowestIndex(0) {
this->createCube();
this->precomputeLowestIndex();
}
template<DdType LibraryType>
DdMetaVariable<LibraryType>::DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(type), low(0), ddVariables(ddVariables) {
DdMetaVariable<LibraryType>::DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(type), low(0), ddVariables(ddVariables), lowestIndex(0) {
STORM_LOG_ASSERT(type == MetaVariableType::Bool || type == MetaVariableType::BitVector, "Cannot create this type of meta variable in this constructor.");
if (ddVariables.size() < 63) {
this->high = (1ull << ddVariables.size()) - 1;
@ -21,6 +22,7 @@ namespace storm {
this->type = MetaVariableType::Bool;
}
this->createCube();
this->precomputeLowestIndex();
}
template<DdType LibraryType>
@ -54,7 +56,7 @@ namespace storm {
if (result && high) {
return value <= this->high;
}
return false;
return result;
}
template<DdType LibraryType>
@ -73,9 +75,11 @@ namespace storm {
}
template<DdType LibraryType>
std::vector<uint64_t> DdMetaVariable<LibraryType>::getIndices() const {
std::vector<uint64_t> DdMetaVariable<LibraryType>::getIndices(bool sortedByLevel) const {
std::vector<std::pair<uint64_t, uint64_t>> indicesAndLevels = this->getIndicesAndLevels();
std::sort(indicesAndLevels.begin(), indicesAndLevels.end(), [] (std::pair<uint64_t, uint64_t> const& a, std::pair<uint64_t, uint64_t> const& b) { return a.second < b.second; });
if (sortedByLevel) {
std::sort(indicesAndLevels.begin(), indicesAndLevels.end(), [] (std::pair<uint64_t, uint64_t> const& a, std::pair<uint64_t, uint64_t> const& b) { return a.second < b.second; });
}
std::vector<uint64_t> indices;
for (auto const& e : indicesAndLevels) {
@ -110,6 +114,11 @@ namespace storm {
return result;
}
template<DdType LibraryType>
uint64_t DdMetaVariable<LibraryType>::getLowestIndex() const {
return lowestIndex;
}
template<DdType LibraryType>
void DdMetaVariable<LibraryType>::createCube() {
STORM_LOG_ASSERT(!this->ddVariables.empty(), "The DD variables must not be empty.");
@ -121,6 +130,19 @@ namespace storm {
}
}
template<DdType LibraryType>
void DdMetaVariable<LibraryType>::precomputeLowestIndex() {
bool first = true;
for (auto const& var : this->ddVariables) {
if (first) {
first = false;
this->lowestIndex = var.getIndex();
} else {
this->lowestIndex = std::min(lowestIndex, var.getIndex());
}
}
}
template class DdMetaVariable<DdType::CUDD>;
template class DdMetaVariable<DdType::Sylvan>;
}

19
src/storm/storage/dd/DdMetaVariable.h
View File

@ -88,15 +88,22 @@ namespace storm {
*/
Bdd<LibraryType> const& getCube() const;
/*!
* Retrieves the highest index of all DD variables belonging to this meta variable.
*/
uint64_t getLowestIndex() const;
/*!
* Retrieves the highest level of all DD variables belonging to this meta variable.
*/
uint64_t getHighestLevel() const;
/*!
* Retrieves the indices of the DD variables associated with this meta variable sorted by level.
* Retrieves the indices of the DD variables associated with this meta variable.
*
* @param sortedByLevel If true, the indices are sorted by their level.
*/
std::vector<uint64_t> getIndices() const;
std::vector<uint64_t> getIndices(bool sortedByLevel = true) const;
/*!
* Retrieves the indices and levels of the DD variables associated with this meta variable.
@ -124,6 +131,11 @@ namespace storm {
*/
DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables);
/*!
* Precomputes the lowest index of any DD variable associated with this meta variable.
*/
void precomputeLowestIndex();
/*!
* Retrieves the variables used to encode the meta variable.
*
@ -153,6 +165,9 @@ namespace storm {
// The cube consisting of all variables that encode the meta variable.
Bdd<LibraryType> cube;
// The lowest index of any DD variable of this meta variable.
uint64_t lowestIndex;
};
}
}

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

@ -197,6 +197,9 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> extractTransitionMatrix(storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& transitionMatrix, Partition<storm::dd::DdType::CUDD, ValueType> const& partition) {
STORM_LOG_ASSERT(partition.storedAsAdd(), "Expected partition stored as ADD.");
transitionMatrix.exportToDot("trans.dot");
partition.asAdd().exportToDot("part.dot");
// Create the number of rows necessary for the matrix.
this->reserveMatrixEntries(partition.getNumberOfBlocks());
STORM_LOG_TRACE("Partition has " << partition.getNumberOfStates() << " states in " << partition.getNumberOfBlocks() << " blocks.");
@ -291,7 +294,7 @@ namespace storm {
}
}
void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t sourceStateEncodingIndex, storm::storage::BitVector& sourceStateEncoding, storm::storage::BitVector const& nondeterminismEncoding, ValueType factor = 1) {
void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t sourceStateEncodingIndex, storm::storage::BitVector& sourceStateEncoding, storm::storage::BitVector const& nondeterminismEncoding, ValueType const& factor = 1) {
// 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 (transitionMatrixNode == Cudd_ReadZero(ddman)) {
@ -322,6 +325,9 @@ namespace storm {
uint64_t targetPartitionVariable = Cudd_NodeReadIndex(targetPartitionNode) - 1;
// Move through transition matrix.
bool skippedSourceInMatrix = false;
bool skippedTargetTInMatrix = false;
bool skippedTargetEInMatrix = false;
DdNode* tt = transitionMatrixNode;
DdNode* te = transitionMatrixNode;
DdNode* et = transitionMatrixNode;
@ -335,6 +341,7 @@ namespace storm {
te = Cudd_E(t);
} else {
tt = te = t;
skippedTargetTInMatrix = true;
}
DdNode* e = Cudd_E(transitionMatrixNode);
@ -344,13 +351,16 @@ namespace storm {
ee = Cudd_E(e);
} else {
et = ee = e;
skippedTargetEInMatrix = true;
}
} else {
skippedSourceInMatrix = true;
if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[sourceStateEncodingIndex].first + 1) {
tt = et = Cudd_T(transitionMatrixNode);
te = ee = Cudd_E(transitionMatrixNode);
} else {
tt = te = et = ee = transitionMatrixNode;
skippedTargetTInMatrix = skippedTargetEInMatrix = true;
}
}
@ -383,8 +393,10 @@ namespace storm {
// If we skipped the variable in the source partition, we only have to choose one of the two representatives.
if (!skippedInSourcePartition) {
sourceStateEncoding.set(sourceStateEncodingIndex, true);
extractTransitionMatrixRec(tt, sourceT, targetT, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor);
extractTransitionMatrixRec(te, sourceT, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor);
if (!skippedInTargetPartition) {
extractTransitionMatrixRec(tt, sourceT, targetT, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor);
}
extractTransitionMatrixRec(te, sourceT, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedTargetTInMatrix && skippedInTargetPartition ? 2 * factor : factor);
}
sourceStateEncoding.set(sourceStateEncodingIndex, false);
@ -392,7 +404,7 @@ namespace storm {
if (!skippedInTargetPartition) {
extractTransitionMatrixRec(et, sourceE, targetT, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor);
}
extractTransitionMatrixRec(ee, sourceE, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedInTargetPartition ? 2 * factor : factor);
extractTransitionMatrixRec(ee, sourceE, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedTargetEInMatrix && skippedInTargetPartition ? 2 * factor : factor);
}
}
@ -497,7 +509,7 @@ namespace storm {
}
}
void extractTransitionMatrixRec(MTBDD transitionMatrixNode, BDD sourcePartitionNode, BDD targetPartitionNode, uint64_t currentIndex, storm::storage::BitVector& sourceState, storm::storage::BitVector const& nondeterminismEncoding) {
void extractTransitionMatrixRec(MTBDD transitionMatrixNode, BDD sourcePartitionNode, BDD targetPartitionNode, uint64_t currentIndex, storm::storage::BitVector& sourceState, storm::storage::BitVector const& nondeterminismEncoding, ValueType const& factor = storm::utility::one<ValueType>()) {
// 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)) {
@ -518,10 +530,9 @@ namespace storm {
// Otherwise, we record the new representative.
sourceRepresentative.reset(new storm::storage::BitVector(sourceState));
// Decode the target block.
// Decode the target block and add matrix entry.
uint64_t targetBlockIndex = decodeBlockIndex(targetPartitionNode);
this->addMatrixEntry(nondeterminismEncoding, sourceBlockIndex, targetBlockIndex, storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(transitionMatrixNode));
this->addMatrixEntry(nondeterminismEncoding, sourceBlockIndex, targetBlockIndex, factor * storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(transitionMatrixNode));
} else {
// Determine the levels in the DDs.
uint64_t transitionMatrixVariable = sylvan_isconst(transitionMatrixNode) ? 0xffffffff : sylvan_var(transitionMatrixNode);
@ -529,6 +540,9 @@ namespace storm {
uint64_t targetPartitionVariable = sylvan_var(targetPartitionNode) - 1;
// Move through transition matrix.
bool skippedSourceInMatrix = false;
bool skippedTargetTInMatrix = false;
bool skippedTargetEInMatrix = false;
MTBDD tt = transitionMatrixNode;
MTBDD te = transitionMatrixNode;
MTBDD et = transitionMatrixNode;
@ -543,6 +557,7 @@ namespace storm {
te = sylvan_low(t);
} else {
tt = te = t;
skippedTargetTInMatrix = true;
}
uint64_t eVariable = sylvan_isconst(e) ? 0xffffffff : sylvan_var(e);
@ -551,17 +566,21 @@ namespace storm {
ee = sylvan_low(e);
} else {
et = ee = e;
skippedTargetEInMatrix = true;
}
} else {
skippedSourceInMatrix = true;
if (transitionMatrixVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first + 1) {
tt = et = sylvan_high(transitionMatrixNode);
te = ee = sylvan_low(transitionMatrixNode);
} else {
tt = te = et = ee = transitionMatrixNode;
skippedTargetTInMatrix = skippedTargetEInMatrix = true;
}
}
// Move through partition (for source state).
bool skippedInSourcePartition = false;
MTBDD sourceT;
MTBDD sourceE;
if (sourcePartitionVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) {
@ -569,9 +588,11 @@ namespace storm {
sourceE = sylvan_low(sourcePartitionNode);
} else {
sourceT = sourceE = sourcePartitionNode;
skippedInSourcePartition = true;
}
// Move through partition (for target state).
bool skippedInTargetPartition = false;
MTBDD targetT;
MTBDD targetE;
if (targetPartitionVariable == this->sourceVariablesIndicesAndLevels[currentIndex].first) {
@ -579,15 +600,25 @@ namespace storm {
targetE = sylvan_low(targetPartitionNode);
} else {
targetT = targetE = targetPartitionNode;
skippedInTargetPartition = true;
}
sourceState.set(currentIndex, true);
extractTransitionMatrixRec(tt, sourceT, targetT, currentIndex + 1, sourceState, nondeterminismEncoding);
extractTransitionMatrixRec(te, sourceT, targetE, currentIndex + 1, sourceState, nondeterminismEncoding);
// If we skipped the variable in the source partition, we only have to choose one of the two representatives.
if (!skippedInSourcePartition) {
sourceState.set(currentIndex, true);
// If we skipped the variable in the target partition, just count the one representative twice.
if (!skippedInTargetPartition) {
extractTransitionMatrixRec(tt, sourceT, targetT, currentIndex + 1, sourceState, nondeterminismEncoding, factor);
}
extractTransitionMatrixRec(te, sourceT, targetE, currentIndex + 1, sourceState, nondeterminismEncoding, skippedTargetTInMatrix && skippedInTargetPartition ? 2 * factor : factor);
}
sourceState.set(currentIndex, false);
extractTransitionMatrixRec(et, sourceE, targetT, currentIndex + 1, sourceState, nondeterminismEncoding);
extractTransitionMatrixRec(ee, sourceE, targetE, currentIndex + 1, sourceState, nondeterminismEncoding);
// If we skipped the variable in the target partition, just count the one representative twice.
if (!skippedInTargetPartition) {
extractTransitionMatrixRec(et, sourceE, targetT, currentIndex + 1, sourceState, nondeterminismEncoding, factor);
}
extractTransitionMatrixRec(ee, sourceE, targetE, currentIndex + 1, sourceState, nondeterminismEncoding, skippedTargetEInMatrix && skippedInTargetPartition ? 2 * factor : factor);
}
}

40
src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
View File

@ -1,5 +1,7 @@
#include "storm/storage/dd/bisimulation/SignatureRefiner.h"
#include <cstdio>
#include <unordered_map>
#include <boost/container/flat_map.hpp>
@ -57,7 +59,13 @@ namespace storm {
class InternalSignatureRefiner<storm::dd::DdType::CUDD, ValueType> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) {
// Intentionally left empty.
// Initialize precomputed data.
auto const& ddMetaVariable = manager.getMetaVariable(blockVariable);
blockDdVariableIndices = ddMetaVariable.getIndices();
// Create initialized block encoding where all variables are "don't care".
blockEncoding = std::vector<int>(static_cast<uint64_t>(internalDdManager.getCuddManager().ReadSize()), static_cast<int>(2));
}
Partition<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, Signature<storm::dd::DdType::CUDD, ValueType> const& signature) {
@ -85,6 +93,21 @@ namespace storm {
return newPartitionAdd;
}
DdNodePtr encodeBlock(uint64_t blockIndex) {
for (auto const& blockDdVariableIndex : blockDdVariableIndices) {
blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0;
blockIndex >>= 1;
}
::DdManager* ddMan = internalDdManager.getCuddManager().getManager();
DdNodePtr bddEncoding = Cudd_CubeArrayToBdd(ddMan, blockEncoding.data());
Cudd_Ref(bddEncoding);
DdNodePtr result = Cudd_BddToAdd(ddMan, bddEncoding);
Cudd_Ref(result);
Cudd_RecursiveDeref(ddMan, bddEncoding);
Cudd_Deref(result);
return result;
}
DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
::DdManager* ddman = internalDdManager.getCuddManager().getManager();
@ -112,15 +135,8 @@ namespace storm {
signatureCache[nodePair] = partitionNode;
return partitionNode;
} else {
DdNode* result;
{
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex, false).template toAdd<ValueType>();
++nextFreeBlockIndex;
result = blockEncoding.getInternalAdd().getCuddDdNode();
Cudd_Ref(result);
}
DdNode* result = encodeBlock(nextFreeBlockIndex++);
signatureCache[nodePair] = result;
Cudd_Deref(result);
return result;
}
} else {
@ -207,6 +223,12 @@ namespace storm {
storm::dd::Bdd<storm::dd::DdType::CUDD> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::CUDD> nonBlockVariables;
// The indices of the DD variables associated with the block variable.
std::vector<uint64_t> blockDdVariableIndices;
// A vector used for encoding block indices.
std::vector<int> blockEncoding;
// The current number of blocks of the new partition.
uint64_t nextFreeBlockIndex;

Write Preview
Loading…
Cancel
Save