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

only supporting reuse of nothing or of block numbers

tempestpy_adaptions
dehnert 7 years ago
parent
a19c2fe59b
commit
669940ccd3
3 changed files with 63 additions and 333 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/settings/modules/BisimulationSettings.cpp
  2. 2
      src/storm/settings/modules/BisimulationSettings.h
  3. 350
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

10
src/storm/settings/modules/BisimulationSettings.cpp
View File

@ -31,7 +31,7 @@ namespace storm {
std::vector<std::string> signatureModes = { "eager", "lazy" }; std::vector<std::string> signatureModes = { "eager", "lazy" };
this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
std::vector<std::string> reuseModes = {"all", "none", "blocks", "sig"};
std::vector<std::string> reuseModes = {"none", "blocks"};
this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.") this->addOption(storm::settings::OptionBuilder(moduleName, reuseOptionName, true, "Sets whether to reuse all results.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes)) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes))
.setDefaultValueString("blocks").build()) .setDefaultValueString("blocks").build())
@ -76,16 +76,12 @@ namespace storm {
BisimulationSettings::ReuseMode BisimulationSettings::getReuseMode() const { BisimulationSettings::ReuseMode BisimulationSettings::getReuseMode() const {
std::string reuseModeAsString = this->getOption(reuseOptionName).getArgumentByName("mode").getValueAsString(); std::string reuseModeAsString = this->getOption(reuseOptionName).getArgumentByName("mode").getValueAsString();
if (reuseModeAsString == "all") {
return ReuseMode::All;
} else if (reuseModeAsString == "none") {
if (reuseModeAsString == "none") {
return ReuseMode::None; return ReuseMode::None;
} else if (reuseModeAsString == "blocks") { } else if (reuseModeAsString == "blocks") {
return ReuseMode::BlockNumbers; return ReuseMode::BlockNumbers;
} else if (reuseModeAsString == "sig") {
return ReuseMode::SignatureResults;
} }
return ReuseMode::All;
return ReuseMode::BlockNumbers;
} }
bool BisimulationSettings::check() const { bool BisimulationSettings::check() const {

2
src/storm/settings/modules/BisimulationSettings.h
View File

@ -19,7 +19,7 @@ namespace storm {
enum class QuotientFormat { Sparse, Dd }; enum class QuotientFormat { Sparse, Dd };
enum class ReuseMode { All, None, BlockNumbers, SignatureResults };
enum class ReuseMode { None, BlockNumbers };
/*! /*!
* Creates a new set of bisimulation settings. * Creates a new set of bisimulation settings.

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

@ -45,13 +45,11 @@ namespace storm {
auto const& bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>(); auto const& bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode();
this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers;
this->reuseSignatureResult = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::All || reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::SignatureResults;
this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers;
} }
bool shiftStateVariables; bool shiftStateVariables;
bool reuseBlockNumbers; bool reuseBlockNumbers;
bool reuseSignatureResult;
}; };
class ReuseWrapper { class ReuseWrapper {
@ -90,39 +88,24 @@ namespace storm {
} }
Partition<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, Signature<storm::dd::DdType::CUDD, ValueType> const& signature) { Partition<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, Signature<storm::dd::DdType::CUDD, ValueType> const& signature) {
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd;
if (options.reuseBlockNumbers && !options.reuseSignatureResult) {
newPartitionAdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd());
} else {
newPartitionAdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd());
}
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd = refine(oldPartition, signature.getSignatureAdd());;
++numberOfRefinements; ++numberOfRefinements;
uint64_t numberOfBlocks = nextFreeBlockIndex;
if (options.reuseSignatureResult) {
std::set<storm::expressions::Variable> blockVariableSet = {blockVariable};
std::set<storm::expressions::Variable> nonBlockExpressionVariables;
std::set_difference(oldPartition.asAdd().getContainedMetaVariables().begin(), oldPartition.asAdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin()));
numberOfBlocks = newPartitionAdd.notZero().existsAbstract(nonBlockExpressionVariables).getNonZeroCount();
}
return oldPartition.replacePartition(newPartitionAdd, numberOfBlocks, nextFreeBlockIndex);
return oldPartition.replacePartition(newPartitionAdd, nextFreeBlockIndex, nextFreeBlockIndex);
} }
private: private:
void clearCaches() { void clearCaches() {
signatureCache.clear(); signatureCache.clear();
signatureCache2.clear();
reuseBlocksCache.clear(); reuseBlocksCache.clear();
} }
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> refineReuseBlockNumber(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& signatureAdd) {
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> refine(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD.");
nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0;
// Perform the actual recursive refinement step. // Perform the actual recursive refinement step.
DdNodePtr result = refineReuseBlockNumber(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
// Construct resulting ADD from the obtained node and the meta information. // Construct resulting ADD from the obtained node and the meta information.
storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result)); storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result));
@ -132,25 +115,6 @@ namespace storm {
return newPartitionAdd; return newPartitionAdd;
} }
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> refineReuseSignatureResults(Partition<storm::dd::DdType::CUDD, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::CUDD, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD.");
nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0;
// Perform the actual recursive refinement step.
DdNodePtr result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
// Construct resulting ADD from the obtained node and the meta information.
storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result));
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables());
if (options.reuseSignatureResult) {
oldSignatureCache = signatureCache;
}
clearCaches();
return newPartitionAdd;
}
DdNodePtr encodeBlock(uint64_t blockIndex) { DdNodePtr encodeBlock(uint64_t blockIndex) {
for (auto const& blockDdVariableIndex : blockDdVariableIndices) { for (auto const& blockDdVariableIndex : blockDdVariableIndices) {
blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0; blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0;
@ -165,102 +129,7 @@ namespace storm {
return result; return result;
} }
DdNodePtr refineReuseSignatureResults(DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock).
if (signatureNode == Cudd_ReadZero(ddman)) {
return signatureNode;
}
// Check the cache whether we have seen the same node before.
auto it = signatureCache.find(signatureNode);
if (it != signatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
// If we are to reuse signature results, check the old cache.
if (options.reuseSignatureResult) {
it = oldSignatureCache.find(signatureNode);
if (it != oldSignatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
}
// If there are no more non-block variables, we hit the signature.
if (Cudd_IsConstant(nonBlockVariablesNode)) {
DdNode* result = encodeBlock(nextFreeBlockIndex++);
signatureCache[signatureNode] = result;
return result;
} else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
bool skipped = true;
DdNode* signatureThen;
DdNode* signatureElse;
short offset;
bool isNondeterminismVariable = false;
while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = options.shiftStateVariables ? 1 : 0;
if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
}
if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
signatureThen = Cudd_T(signatureNode);
signatureElse = Cudd_E(signatureNode);
skipped = false;
} else {
signatureThen = signatureElse = signatureNode;
}
// If we skipped the next variable, we fast-forward.
if (skipped) {
// If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables.
nonBlockVariablesNode = Cudd_T(nonBlockVariablesNode);
if (isNondeterminismVariable) {
nondeterminismVariablesNode = Cudd_T(nondeterminismVariablesNode);
}
}
}
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (Cudd_IsConstant(nonBlockVariablesNode)) {
return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
DdNode* thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(thenResult);
DdNode* elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(elseResult);
DdNode* result;
if (thenResult == elseResult) {
Cudd_Deref(thenResult);
Cudd_Deref(elseResult);
result = thenResult;
} else {
// Get the node to connect the subresults.
bool complemented = Cudd_IsComplement(thenResult);
result = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult);
if (complemented) {
result = Cudd_Not(result);
}
Cudd_Deref(thenResult);
Cudd_Deref(elseResult);
}
// Store the result in the cache.
signatureCache[signatureNode] = result;
return result;
}
}
DdNodePtr refineReuseBlockNumber(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
// If we arrived at the constant zero node, then this was an illegal state encoding (we require // If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock). // all states to be non-deadlock).
if (partitionNode == Cudd_ReadZero(ddman)) { if (partitionNode == Cudd_ReadZero(ddman)) {
@ -269,26 +138,30 @@ namespace storm {
// Check the cache whether we have seen the same node before. // Check the cache whether we have seen the same node before.
auto nodePair = std::make_pair(signatureNode, partitionNode); auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = signatureCache2.find(nodePair);
if (it != signatureCache2.end()) {
auto it = signatureCache.find(nodePair);
if (it != signatureCache.end()) {
// If so, we return the corresponding result. // If so, we return the corresponding result.
return it->second; return it->second;
} }
// If there are no more non-block variables, we hit the signature. // If there are no more non-block variables, we hit the signature.
if (Cudd_IsConstant(nonBlockVariablesNode)) { if (Cudd_IsConstant(nonBlockVariablesNode)) {
if (options.reuseBlockNumbers) {
// If this is the first time (in this traversal) that we encounter this signature, we check // If this is the first time (in this traversal) that we encounter this signature, we check
// whether we can assign the old block number to it. // whether we can assign the old block number to it.
auto& reuseEntry = reuseBlocksCache[partitionNode]; auto& reuseEntry = reuseBlocksCache[partitionNode];
if (!reuseEntry.isReused()) { if (!reuseEntry.isReused()) {
reuseEntry.setReused(); reuseEntry.setReused();
signatureCache2[nodePair] = partitionNode;
signatureCache[nodePair] = partitionNode;
return partitionNode; return partitionNode;
} else {
}
}
DdNode* result = encodeBlock(nextFreeBlockIndex++); DdNode* result = encodeBlock(nextFreeBlockIndex++);
signatureCache2[nodePair] = result;
signatureCache[nodePair] = result;
return result; return result;
}
} else { } else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
@ -335,12 +208,12 @@ namespace storm {
// If there are no more non-block variables remaining, make a recursive call to enter the base case. // If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (Cudd_IsConstant(nonBlockVariablesNode)) { if (Cudd_IsConstant(nonBlockVariablesNode)) {
return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
} }
DdNode* thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
DdNode* thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(thenResult); Cudd_Ref(thenResult);
DdNode* elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
DdNode* elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(elseResult); Cudd_Ref(elseResult);
DdNode* result; DdNode* result;
@ -360,8 +233,7 @@ namespace storm {
} }
// Store the result in the cache. // Store the result in the cache.
signatureCache2[nodePair] = result;
signatureCache[nodePair] = result;
return result; return result;
} }
} }
@ -394,9 +266,7 @@ namespace storm {
uint64_t lastNumberOfVisitedNodes; uint64_t lastNumberOfVisitedNodes;
// The cache used to identify states with identical signature. // The cache used to identify states with identical signature.
spp::sparse_hash_map<DdNode const*, DdNode*> oldSignatureCache;
spp::sparse_hash_map<DdNode const*, DdNode*> signatureCache;
spp::sparse_hash_map<std::pair<DdNode const*, DdNode const*>, DdNode*, CuddPointerPairHash> signatureCache2;
spp::sparse_hash_map<std::pair<DdNode const*, DdNode const*>, DdNode*, CuddPointerPairHash> signatureCache;
// The cache used to identify which old block numbers have already been reused. // The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<DdNode const*, ReuseWrapper> reuseBlocksCache; spp::sparse_hash_map<DdNode const*, ReuseWrapper> reuseBlocksCache;
@ -412,44 +282,24 @@ namespace storm {
} }
Partition<storm::dd::DdType::Sylvan, ValueType> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, Signature<storm::dd::DdType::Sylvan, ValueType> const& signature) { Partition<storm::dd::DdType::Sylvan, ValueType> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, Signature<storm::dd::DdType::Sylvan, ValueType> const& signature) {
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd;
if (options.reuseBlockNumbers && !options.reuseSignatureResult) {
newPartitionBdd = refineReuseBlockNumber(oldPartition, signature.getSignatureAdd());
} else {
newPartitionBdd = refineReuseSignatureResults(oldPartition, signature.getSignatureAdd());
}
auto start = std::chrono::high_resolution_clock::now();
uint64_t numberOfBlocks = nextFreeBlockIndex;
if (options.reuseSignatureResult) {
std::set<storm::expressions::Variable> blockVariableSet = {blockVariable};
std::set<storm::expressions::Variable> nonBlockExpressionVariables;
std::set_difference(oldPartition.asBdd().getContainedMetaVariables().begin(), oldPartition.asBdd().getContainedMetaVariables().end(), blockVariableSet.begin(), blockVariableSet.end(), std::inserter(nonBlockExpressionVariables, nonBlockExpressionVariables.begin()));
numberOfBlocks = newPartitionBdd.existsAbstract(nonBlockExpressionVariables).getNonZeroCount();
}
auto end = std::chrono::high_resolution_clock::now();
std::cout << "took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << std::endl;
return oldPartition.replacePartition(newPartitionBdd, numberOfBlocks, nextFreeBlockIndex);
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd = refine(oldPartition, signature.getSignatureAdd());
++numberOfRefinements;
return oldPartition.replacePartition(newPartitionBdd, nextFreeBlockIndex, nextFreeBlockIndex);
} }
private: private:
void clearCaches() { void clearCaches() {
signatureCache.clear(); signatureCache.clear();
signatureCache2.clear();
reuseBlocksCache.clear(); reuseBlocksCache.clear();
} }
storm::dd::Bdd<storm::dd::DdType::Sylvan> refineReuseBlockNumber(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& signatureAdd) {
storm::dd::Bdd<storm::dd::DdType::Sylvan> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan.");
// Set up next refinement.
++numberOfRefinements;
nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0;
// Perform the actual recursive refinement step. // Perform the actual recursive refinement step.
BDD result = refineReuseBlockNumber(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
// Construct resulting BDD from the obtained node and the meta information. // Construct resulting BDD from the obtained node and the meta information.
storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result)); storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result));
@ -459,28 +309,6 @@ namespace storm {
return newPartitionBdd; return newPartitionBdd;
} }
storm::dd::Bdd<storm::dd::DdType::Sylvan> refineReuseSignatureResults(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& signatureAdd) {
STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan.");
// Set up next refinement.
++numberOfRefinements;
nextFreeBlockIndex = options.reuseSignatureResult ? oldPartition.getNextFreeBlockIndex() : 0;
// Perform the actual recursive refinement step.
BDD result = refineReuseSignatureResults(signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
// Construct resulting BDD from the obtained node and the meta information.
storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result));
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables());
if (options.reuseSignatureResult) {
oldSignatureCache = signatureCache;
}
clearCaches();
return newPartitionBdd;
}
BDD encodeBlock(uint64_t blockIndex) { BDD encodeBlock(uint64_t blockIndex) {
std::vector<uint8_t> e(numberOfBlockVariables); std::vector<uint8_t> e(numberOfBlockVariables);
for (uint64_t i = 0; i < numberOfBlockVariables; ++i) { for (uint64_t i = 0; i < numberOfBlockVariables; ++i) {
@ -490,101 +318,7 @@ namespace storm {
return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data()); return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data());
} }
BDD refineReuseSignatureResults(MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
LACE_ME;
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock).
if (mtbdd_iszero(signatureNode)) {
return sylvan_false;
}
// Check the cache whether we have seen the same node before.
auto it = signatureCache.find(signatureNode);
if (it != signatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
// If we are to reuse signature results, check the old cache.
if (options.reuseSignatureResult) {
it = oldSignatureCache.find(signatureNode);
if (it != oldSignatureCache.end()) {
// If so, we return the corresponding result.
return it->second;
}
}
sylvan_gc_test();
// If there are no more non-block variables, we hit the signature.
if (sylvan_isconst(nonBlockVariablesNode)) {
BDD result = encodeBlock(nextFreeBlockIndex++);
signatureCache[signatureNode] = result;
return result;
} else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
bool skipped = true;
MTBDD signatureThen;
MTBDD signatureElse;
short offset;
bool isNondeterminismVariable = false;
while (skipped && !sylvan_isconst(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = options.shiftStateVariables ? 1 : 0;
if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
}
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) {
signatureThen = sylvan_high(signatureNode);
signatureElse = sylvan_low(signatureNode);
skipped = false;
} else {
signatureThen = signatureElse = signatureNode;
}
// If we skipped the next variable, we fast-forward.
if (skipped) {
// If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables.
nonBlockVariablesNode = sylvan_high(nonBlockVariablesNode);
if (isNondeterminismVariable) {
nondeterminismVariablesNode = sylvan_high(nondeterminismVariablesNode);
}
}
}
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (sylvan_isconst(nonBlockVariablesNode)) {
return refineReuseSignatureResults(signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
BDD thenResult = refineReuseSignatureResults(signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(thenResult);
BDD elseResult = refineReuseSignatureResults(signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(elseResult);
BDD result;
if (thenResult == elseResult) {
result = thenResult;
} else {
// Get the node to connect the subresults.
result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult);
}
// Dispose of the intermediate results.
bdd_refs_pop(2);
// Store the result in the cache.
signatureCache[signatureNode] = result;
return result;
}
}
BDD refineReuseBlockNumber(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
BDD refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
LACE_ME; LACE_ME;
// If we arrived at the constant zero node, then this was an illegal state encoding (we require // If we arrived at the constant zero node, then this was an illegal state encoding (we require
@ -597,8 +331,8 @@ namespace storm {
// Check the cache whether we have seen the same node before. // Check the cache whether we have seen the same node before.
auto nodePair = std::make_pair(signatureNode, partitionNode); auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = signatureCache2.find(nodePair);
if (it != signatureCache2.end()) {
auto it = signatureCache.find(nodePair);
if (it != signatureCache.end()) {
// If so, we return the corresponding result. // If so, we return the corresponding result.
return it->second; return it->second;
} }
@ -607,6 +341,7 @@ namespace storm {
// If there are no more non-block variables, we hit the signature. // If there are no more non-block variables, we hit the signature.
if (sylvan_isconst(nonBlockVariablesNode)) { if (sylvan_isconst(nonBlockVariablesNode)) {
if (options.reuseBlockNumbers) {
// If this is the first time (in this traversal) that we encounter this signature, we check // If this is the first time (in this traversal) that we encounter this signature, we check
// whether we can assign the old block number to it. // whether we can assign the old block number to it.
@ -614,13 +349,14 @@ namespace storm {
if (!reuseBlockEntry.isReused()) { if (!reuseBlockEntry.isReused()) {
reuseBlockEntry.setReused(); reuseBlockEntry.setReused();
reuseBlocksCache.emplace(partitionNode, true); reuseBlocksCache.emplace(partitionNode, true);
signatureCache2[nodePair] = partitionNode;
signatureCache[nodePair] = partitionNode;
return partitionNode; return partitionNode;
} else {
}
}
BDD result = encodeBlock(nextFreeBlockIndex++); BDD result = encodeBlock(nextFreeBlockIndex++);
signatureCache2[nodePair] = result;
signatureCache[nodePair] = result;
return result; return result;
}
} else { } else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend. // If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
@ -667,12 +403,12 @@ namespace storm {
// If there are no more non-block variables remaining, make a recursive call to enter the base case. // If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (sylvan_isconst(nonBlockVariablesNode)) { if (sylvan_isconst(nonBlockVariablesNode)) {
return refineReuseBlockNumber(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
} }
BDD thenResult = refineReuseBlockNumber(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD thenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(thenResult); bdd_refs_push(thenResult);
BDD elseResult = refineReuseBlockNumber(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD elseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
bdd_refs_push(elseResult); bdd_refs_push(elseResult);
BDD result; BDD result;
@ -687,7 +423,7 @@ namespace storm {
bdd_refs_pop(2); bdd_refs_pop(2);
// Store the result in the cache. // Store the result in the cache.
signatureCache2[nodePair] = result;
signatureCache[nodePair] = result;
return result; return result;
} }
@ -714,9 +450,7 @@ namespace storm {
uint64_t numberOfRefinements; uint64_t numberOfRefinements;
// The cache used to identify states with identical signature. // The cache used to identify states with identical signature.
spp::sparse_hash_map<MTBDD, MTBDD> oldSignatureCache;
spp::sparse_hash_map<MTBDD, MTBDD> signatureCache;
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, MTBDD, SylvanMTBDDPairHash> signatureCache2;
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, MTBDD, SylvanMTBDDPairHash> signatureCache;
// The cache used to identify which old block numbers have already been reused. // The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<MTBDD, ReuseWrapper> reuseBlocksCache; spp::sparse_hash_map<MTBDD, ReuseWrapper> reuseBlocksCache;

Write Preview
Loading…
Cancel
Save