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

toward multi-threaded dd bisimulation

main
dehnert 7 years ago
parent
edec805e37
commit
d2d129a836
9 changed files with 276 additions and 102 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. 17
      src/storm/settings/modules/BisimulationSettings.cpp
  2. 8
      src/storm/settings/modules/BisimulationSettings.h
  3. 22
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  4. 270
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
  5. 7
      src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
  6. 10
      src/storm/storage/dd/sylvan/InternalSylvanAdd.h
  7. 4
      src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp
  8. 10
      src/storm/storage/dd/sylvan/InternalSylvanBdd.h
  9. 30
      src/storm/utility/sylvan.h

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

@ -20,6 +20,7 @@ namespace storm {
const std::string BisimulationSettings::reuseOptionName = "reuse";
const std::string BisimulationSettings::initialPartitionOptionName = "init";
const std::string BisimulationSettings::refinementModeOptionName = "refine";
const std::string BisimulationSettings::parallelismModeOptionName = "parallel";
BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) {
std::vector<std::string> types = { "strong", "weak" };
@ -50,6 +51,12 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(refinementModes))
.setDefaultValueString("full").build())
.build());
std::vector<std::string> parallelismModes = {"on", "off"};
this->addOption(storm::settings::OptionBuilder(moduleName, parallelismModeOptionName, true, "Sets whether to use parallelism mode or not.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(parallelismModes))
.setDefaultValueString("on").build())
.build());
}
bool BisimulationSettings::isStrongBisimulationSet() const {
@ -118,6 +125,16 @@ namespace storm {
return RefinementMode::Full;
}
BisimulationSettings::ParallelismMode BisimulationSettings::getParallelismMode() const {
std::string parallelismModeAsString = this->getOption(parallelismModeOptionName).getArgumentByName("mode").getValueAsString();
if (parallelismModeAsString == "on") {
return ParallelismMode::Parallel;
} else if (parallelismModeAsString == "off") {
return ParallelismMode::Sequential;
}
return ParallelismMode::Parallel;
}
bool BisimulationSettings::check() const {
bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet();
STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");

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

@ -25,6 +25,8 @@ namespace storm {
enum class RefinementMode { Full, ChangedStates };
enum class ParallelismMode { Parallel, Sequential };
/*!
* Creates a new set of bisimulation settings.
*/
@ -76,6 +78,11 @@ namespace storm {
*/
RefinementMode getRefinementMode() const;
/*!
* Retrieves whether parallel is set.
*/
ParallelismMode getParallelismMode() const;
virtual bool check() const override;
// The name of the module.
@ -90,6 +97,7 @@ namespace storm {
static const std::string reuseOptionName;
static const std::string initialPartitionOptionName;
static const std::string refinementModeOptionName;
static const std::string parallelismModeOptionName;
};
} // namespace modules
} // namespace settings

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

@ -175,7 +175,7 @@ namespace storm {
bool skipped = false;
BDD elsePartitionNode;
BDD thenPartitionNode;
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(partitionNode, sylvan_var(stateVariablesCube))) {
if (sylvan_bdd_matches_variable_index(partitionNode, sylvan_var(stateVariablesCube))) {
elsePartitionNode = sylvan_low(partitionNode);
thenPartitionNode = sylvan_high(partitionNode);
} else {
@ -647,7 +647,7 @@ namespace storm {
} else {
MTBDD vectorT;
MTBDD vectorE;
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(vector, sylvan_var(variables))) {
if (sylvan_mtbdd_matches_variable_index(vector, sylvan_var(variables))) {
vectorT = sylvan_high(vector);
vectorE = sylvan_low(vector);
} else {
@ -656,7 +656,7 @@ namespace storm {
BDD representativesT;
BDD representativesE;
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(representativesNode, sylvan_var(variables))) {
if (sylvan_bdd_matches_variable_index(representativesNode, sylvan_var(variables))) {
representativesT = sylvan_high(representativesNode);
representativesE = sylvan_low(representativesNode);
} else {
@ -687,7 +687,7 @@ namespace storm {
STORM_LOG_ASSERT(!odd.isTerminalNode(), "Expected non-terminal node.");
BDD partitionT;
BDD partitionE;
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(partitionNode, sylvan_var(variables))) {
if (sylvan_bdd_matches_variable_index(partitionNode, sylvan_var(variables))) {
partitionT = sylvan_high(partitionNode);
partitionE = sylvan_low(partitionNode);
} else {
@ -696,7 +696,7 @@ namespace storm {
BDD representativesT;
BDD representativesE;
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(representativesNode, sylvan_var(variables))) {
if (sylvan_bdd_matches_variable_index(representativesNode, sylvan_var(variables))) {
representativesT = sylvan_high(representativesNode);
representativesE = sylvan_low(representativesNode);
} else {
@ -732,7 +732,7 @@ namespace storm {
MTBDD e;
// Determine whether the variable was skipped in the matrix.
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) {
if (sylvan_mtbdd_matches_variable_index(transitionMatrixNode, sylvan_var(variables))) {
t = sylvan_high(transitionMatrixNode);
e = sylvan_low(transitionMatrixNode);
} else {
@ -749,7 +749,7 @@ namespace storm {
MTBDD e;
MTBDD et;
MTBDD ee;
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(transitionMatrixNode, sylvan_var(variables))) {
if (sylvan_mtbdd_matches_variable_index(transitionMatrixNode, sylvan_var(variables))) {
// Source node was not skipped in transition matrix.
t = sylvan_high(transitionMatrixNode);
e = sylvan_low(transitionMatrixNode);
@ -757,7 +757,7 @@ namespace storm {
t = e = transitionMatrixNode;
}
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(t, sylvan_var(variables) + 1)) {
if (sylvan_mtbdd_matches_variable_index(t, sylvan_var(variables) + 1)) {
// Target node was not skipped in transition matrix.
tt = sylvan_high(t);
te = sylvan_low(t);
@ -766,7 +766,7 @@ namespace storm {
tt = te = t;
}
if (t != e) {
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(e, sylvan_var(variables) + 1)) {
if (sylvan_mtbdd_matches_variable_index(e, sylvan_var(variables) + 1)) {
// Target node was not skipped in transition matrix.
et = sylvan_high(e);
ee = sylvan_low(e);
@ -781,7 +781,7 @@ namespace storm {
BDD targetT;
BDD targetE;
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(targetPartitionNode, sylvan_var(variables))) {
if (sylvan_bdd_matches_variable_index(targetPartitionNode, sylvan_var(variables))) {
// Node was not skipped in target partition.
targetT = sylvan_high(targetPartitionNode);
targetE = sylvan_low(targetPartitionNode);
@ -792,7 +792,7 @@ namespace storm {
BDD representativesT;
BDD representativesE;
if (storm::dd::InternalBdd<storm::dd::DdType::Sylvan>::matchesVariableIndex(representativesNode, sylvan_var(variables))) {
if (sylvan_bdd_matches_variable_index(representativesNode, sylvan_var(variables))) {
// Node was not skipped in representatives.
representativesT = sylvan_high(representativesNode);
representativesE = sylvan_low(representativesNode);

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

@ -1,6 +1,7 @@
#include "storm/storage/dd/bisimulation/SignatureRefiner.h"
#include <cstdio>
#include <mutex>
#include <unordered_map>
#include <boost/container/flat_map.hpp>
@ -41,7 +42,7 @@ namespace storm {
// Intentionally left empty.
}
InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true) {
InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true), parallel(false) {
auto const& bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode();
@ -49,11 +50,15 @@ namespace storm {
storm::settings::modules::BisimulationSettings::RefinementMode refinementMode = bisimulationSettings.getRefinementMode();
this->createChangedStates = refinementMode == storm::settings::modules::BisimulationSettings::RefinementMode::ChangedStates;
storm::settings::modules::BisimulationSettings::ParallelismMode parallelismMode = bisimulationSettings.getParallelismMode();
this->parallel = parallelismMode == storm::settings::modules::BisimulationSettings::ParallelismMode::Parallel;
}
bool shiftStateVariables;
bool reuseBlockNumbers;
bool createChangedStates;
bool parallel;
};
class ReuseWrapper {
@ -461,24 +466,79 @@ namespace storm {
spp::sparse_hash_map<DdNode const*, ReuseWrapper> reuseBlocksCache;
};
template<typename ValueType>
class InternalSignatureRefiner<storm::dd::DdType::Sylvan, ValueType> {
TASK_DECL_5(BDD, refine_double, BDD, MTBDD, BDD, BDD, void*);
template<storm::dd::DdType DdType>
class InternalSignatureRefinerBase;
template<>
class InternalSignatureRefinerBase<storm::dd::DdType::Sylvan> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() {
InternalSignatureRefinerBase(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() {
// Perform garbage collection to clean up stuff not needed anymore.
LACE_ME;
sylvan_gc();
}
BDD encodeBlock(uint64_t blockIndex) {
std::vector<uint8_t> e(numberOfBlockVariables);
for (uint64_t i = 0; i < numberOfBlockVariables; ++i) {
e[i] = blockIndex & 1 ? 1 : 0;
blockIndex >>= 1;
}
return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data());
}
storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager;
storm::dd::InternalDdManager<storm::dd::DdType::Sylvan> const& internalDdManager;
storm::expressions::Variable blockVariable;
std::set<storm::expressions::Variable> stateVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> nonBlockVariables;
// The provided options.
InternalSignatureRefinerOptions options;
uint64_t numberOfBlockVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> blockCube;
// The current number of blocks of the new partition.
uint64_t nextFreeBlockIndex;
// The number of completed refinements.
uint64_t numberOfRefinements;
// The cache used to identify states with identical signature.
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, std::pair<BDD, BDD>, SylvanMTBDDPairHash> signatureCache;
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, BDD, SylvanMTBDDPairHash> signatureCacheSingle;
// The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<MTBDD, ReuseWrapper> reuseBlocksCache;
// A mutex that can be used to synchronize concurrent accesses to the members.
std::mutex mutex;
};
template<typename ValueType>
class InternalSignatureRefiner<storm::dd::DdType::Sylvan, ValueType> : public InternalSignatureRefinerBase<storm::dd::DdType::Sylvan> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : InternalSignatureRefinerBase<storm::dd::DdType::Sylvan>(manager, blockVariable, stateVariables, nondeterminismVariables, nonBlockVariables, options) {
// Intentionally left empty.
}
Partition<storm::dd::DdType::Sylvan, ValueType> refine(Partition<storm::dd::DdType::Sylvan, ValueType> const& oldPartition, Signature<storm::dd::DdType::Sylvan, ValueType> const& signature) {
std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, boost::optional<storm::dd::Bdd<storm::dd::DdType::Sylvan>>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd());
++numberOfRefinements;
return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second);
}
private:
void clearCaches() {
signatureCache.clear();
signatureCacheSingle.clear();
reuseBlocksCache.clear();
}
@ -488,14 +548,21 @@ namespace storm {
nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0;
// Perform the actual recursive refinement step.
std::pair<BDD, BDD> result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
std::pair<BDD, BDD> result;
if (options.parallel) {
STORM_LOG_TRACE("Using parallel refine.");
result = refineParallel(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
} else {
STORM_LOG_TRACE("Using sequential refine.");
result = refineSequential(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.
storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result.first));
storm::dd::Bdd<storm::dd::DdType::Sylvan> newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables());
boost::optional<storm::dd::Bdd<storm::dd::DdType::Sylvan>> optionalChangedBdd;
if (options.createChangedStates) {
if (options.createChangedStates && result.second != 0) {
storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalChangedBdd(&internalDdManager, sylvan::Bdd(result.second));
storm::dd::Bdd<storm::dd::DdType::Sylvan> changedBdd(oldPartition.asBdd().getDdManager(), internalChangedBdd, stateVariables);
optionalChangedBdd = changedBdd;
@ -504,15 +571,6 @@ namespace storm {
clearCaches();
return std::make_pair(newPartitionBdd, optionalChangedBdd);
}
BDD encodeBlock(uint64_t blockIndex) {
std::vector<uint8_t> e(numberOfBlockVariables);
for (uint64_t i = 0; i < numberOfBlockVariables; ++i) {
e[i] = blockIndex & 1 ? 1 : 0;
blockIndex >>= 1;
}
return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data());
}
std::pair<BDD, BDD> reuseOrRelabel(BDD partitionNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
LACE_ME;
@ -580,7 +638,7 @@ namespace storm {
isNondeterminismVariable = true;
}
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) {
if (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) {
partitionThen = sylvan_high(partitionNode);
partitionElse = sylvan_low(partitionNode);
skipped = false;
@ -649,7 +707,12 @@ namespace storm {
}
}
std::pair<BDD, BDD> refine(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
std::pair<BDD, BDD> refineParallel(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) {
LACE_ME;
return std::make_pair(CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0);
}
std::pair<BDD, BDD> refineSequential(BDD partitionNode, 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
@ -675,9 +738,9 @@ namespace storm {
// 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)) {
if (options.reuseBlockNumbers) {
@ -709,7 +772,7 @@ namespace storm {
return result;
} else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
bool skippedBoth = true;
BDD partitionThen;
BDD partitionElse;
@ -725,22 +788,22 @@ namespace storm {
isNondeterminismVariable = true;
}
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) {
if (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) {
partitionThen = sylvan_high(partitionNode);
partitionElse = sylvan_low(partitionNode);
skippedBoth = false;
} else {
partitionThen = partitionElse = partitionNode;
}
if (storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::matchesVariableIndex(signatureNode, sylvan_var(nonBlockVariablesNode))) {
if (sylvan_mtbdd_matches_variable_index(signatureNode, sylvan_var(nonBlockVariablesNode))) {
signatureThen = sylvan_high(signatureNode);
signatureElse = sylvan_low(signatureNode);
skippedBoth = false;
} else {
signatureThen = signatureElse = signatureNode;
}
// If both (signature and partition) skipped the next variable, we fast-forward.
if (skippedBoth) {
// If the current variable is a nondeterminism variable, we need to advance both variable sets otherwise just the non-block variables.
@ -750,20 +813,20 @@ namespace storm {
}
}
}
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (sylvan_isconst(nonBlockVariablesNode)) {
return refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
return refineSequential(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
std::pair<BDD, BDD> combinedThenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
std::pair<BDD, BDD> combinedThenResult = refineSequential(partitionThen, signatureThen, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD thenResult = combinedThenResult.first;
bdd_refs_push(thenResult);
BDD changedThenResult = combinedThenResult.second;
if (options.createChangedStates) {
bdd_refs_push(changedThenResult);
}
std::pair<BDD, BDD> combinedElseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
std::pair<BDD, BDD> combinedElseResult = refineSequential(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD elseResult = combinedElseResult.first;
bdd_refs_push(elseResult);
BDD changedElseResult = combinedElseResult.second;
@ -798,49 +861,134 @@ namespace storm {
// Store the result in the cache.
signatureCache[nodePair] = result;
return result;
}
}
storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager;
storm::dd::InternalDdManager<storm::dd::DdType::Sylvan> const& internalDdManager;
storm::expressions::Variable blockVariable;
std::set<storm::expressions::Variable> stateVariables;
};
TASK_IMPL_5(BDD, refine_double, BDD, partitionNode, MTBDD, signatureNode, BDD, nondeterminismVariablesNode, BDD, nonBlockVariablesNode, void*, refinerPtr)
{
auto& refiner = *static_cast<InternalSignatureRefinerBase<storm::dd::DdType::Sylvan>*>(refinerPtr);
std::unique_lock<std::mutex> lock(refiner.mutex, std::defer_lock);
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
// all states to be non-deadlock).
if (partitionNode == sylvan_false) {
return sylvan_false;
}
storm::dd::Bdd<storm::dd::DdType::Sylvan> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> nonBlockVariables;
STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node.");
// The provided options.
InternalSignatureRefinerOptions options;
BDD result;
uint64_t numberOfBlockVariables;
if (sylvan_isconst(nonBlockVariablesNode)) {
// Get the lock so we can modify the signature cache.
lock.lock();
// Check the signature cache whether we have seen this signature before.
auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = refiner.signatureCacheSingle.find(nodePair);
if (it != refiner.signatureCacheSingle.end()) {
return it->second;
}
if (refiner.options.reuseBlockNumbers) {
// 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.
auto& reuseBlockEntry = refiner.reuseBlocksCache[partitionNode];
if (!reuseBlockEntry.isReused()) {
reuseBlockEntry.setReused();
refiner.reuseBlocksCache.emplace(partitionNode, true);
refiner.signatureCacheSingle[nodePair] = partitionNode;
return partitionNode;
}
}
// Encode new block and give up lock before
result = refiner.encodeBlock(refiner.nextFreeBlockIndex++);
refiner.signatureCacheSingle[nodePair] = result;
lock.unlock();
return result;
}
storm::dd::Bdd<storm::dd::DdType::Sylvan> blockCube;
// Check the cache whether we have seen the same node before.
if (cache_get(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), &result)) {
return result;
}
// The current number of blocks of the new partition.
uint64_t nextFreeBlockIndex;
sylvan_gc_test();
// The number of completed refinements.
uint64_t numberOfRefinements;
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
// The cache used to identify states with identical signature.
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, std::pair<BDD, BDD>, SylvanMTBDDPairHash> signatureCache;
bool skippedBoth = true;
BDD partitionThen;
BDD partitionElse;
MTBDD signatureThen;
MTBDD signatureElse;
short offset;
bool isNondeterminismVariable = false;
while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = refiner.options.shiftStateVariables ? 1 : 0;
if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) {
offset = 0;
isNondeterminismVariable = true;
}
if (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) {
partitionThen = sylvan_high(partitionNode);
partitionElse = sylvan_low(partitionNode);
skippedBoth = false;
} else {
partitionThen = partitionElse = partitionNode;
}
if (sylvan_mtbdd_matches_variable_index(signatureNode, sylvan_var(nonBlockVariablesNode))) {
signatureThen = sylvan_high(signatureNode);
signatureElse = sylvan_low(signatureNode);
skippedBoth = false;
} else {
signatureThen = signatureElse = signatureNode;
}
// If both (signature and partition) skipped the next variable, we fast-forward.
if (skippedBoth) {
// 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);
}
}
}
// The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<MTBDD, ReuseWrapper> reuseBlocksCache;
// If there are no more non-block variables remaining, make a recursive call to enter the base case.
if (sylvan_isconst(nonBlockVariablesNode)) {
return CALL(refine_double, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, refinerPtr);
}
// Performance counters.
// uint64_t signatureCacheLookups;
// uint64_t signatureCacheHits;
// uint64_t numberOfVisitedNodes;
// std::chrono::high_resolution_clock::duration totalSignatureCacheLookupTime;
// std::chrono::high_resolution_clock::duration totalSignatureCacheStoreTime;
// std::chrono::high_resolution_clock::duration totalReuseBlocksLookupTime;
// std::chrono::high_resolution_clock::duration totalLevelLookupTime;
// std::chrono::high_resolution_clock::duration totalBlockEncodingTime;
// std::chrono::high_resolution_clock::duration totalMakeNodeTime;
};
BDD nextNondeterminismVariables = isNondeterminismVariable ? sylvan_set_next(nondeterminismVariablesNode) : nondeterminismVariablesNode;
BDD nextNonBlockVariables = sylvan_set_next(nonBlockVariablesNode);
bdd_refs_spawn(SPAWN(refine_double, partitionThen, signatureThen, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr));
BDD elseResult = bdd_refs_push(CALL(refine_double, partitionElse, signatureElse, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr));
BDD thenResult = bdd_refs_sync(SYNC(refine_double));
bdd_refs_pop(1);
if (thenResult == elseResult) {
result = thenResult;
} else {
// Get the node to connect the subresults.
result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult);
}
// Store the result in the cache.
cache_put(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), result);
return result;
}
template<storm::dd::DdType DdType, typename ValueType>
SignatureRefiner<DdType, ValueType>::SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateRowVariables, std::set<storm::expressions::Variable> const& stateColumnVariables, bool shiftStateVariables, std::set<storm::expressions::Variable> const& nondeterminismVariables) : manager(&manager) {

7
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -79,12 +79,7 @@ namespace storm {
return negated ? -(*rationalFunction) : (*rationalFunction);
}
#endif
template<typename ValueType>
bool InternalAdd<DdType::Sylvan, ValueType>::matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset) {
return !mtbdd_isleaf(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
}
template<typename ValueType>
bool InternalAdd<DdType::Sylvan, ValueType>::operator==(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
return this->sylvanMtbdd == other.sylvanMtbdd;

10
src/storm/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -618,16 +618,6 @@ namespace storm {
* @return The value of the leaf.
*/
static ValueType getValue(MTBDD const& node);
/*!
* Retrieves whether the topmost variable in the MTBDD is the one with the given index.
*
* @param The top node of the MTBDD.
* @param variableIndex The variable index.
* @param offset An offset that is applied to the index of the top variable in the MTBDD.
* @return True iff the MTBDD's top variable has the given index.
*/
static bool matchesVariableIndex(MTBDD const& node, uint64_t variableIndex, int64_t offset = 0);
private:
/*!

4
src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp
View File

@ -527,10 +527,6 @@ namespace storm {
return newNodeVariable;
}
bool InternalBdd<DdType::Sylvan>::matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset) {
return !sylvan_isconst(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
}
template InternalAdd<DdType::Sylvan, double> InternalBdd<DdType::Sylvan>::toAdd() const;
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalBdd<DdType::Sylvan>::toAdd() const;
template InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalBdd<DdType::Sylvan>::toAdd() const;

10
src/storm/storage/dd/sylvan/InternalSylvanBdd.h
View File

@ -373,16 +373,6 @@ namespace storm {
* @param targetValues The vector to which to write the selected values.
*/
void filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const;
/*!
* Retrieves whether the topmost variable in the BDD is the one with the given index.
*
* @param The top node of the BDD.
* @param variableIndex The variable index.
* @param offset An offset that is applied to the index of the top variable in the BDD.
* @return True iff the BDD's top variable has the given index.
*/
static bool matchesVariableIndex(BDD const& node, uint64_t variableIndex, int64_t offset = 0);
friend struct std::hash<storm::dd::InternalBdd<storm::dd::DdType::Sylvan>>;

30
src/storm/utility/sylvan.h
View File

@ -17,5 +17,35 @@
#include "sylvan_storm_rational_number.h"
#include "sylvan_storm_rational_function.h"
namespace storm {
namespace dd {
/*!
* Retrieves whether the topmost variable in the BDD is the one with the given index.
*
* @param node The top node of the BDD.
* @param variableIndex The variable index.
* @param offset An offset that is applied to the index of the top variable in the BDD.
* @return True iff the BDD's top variable has the given index.
*/
bool sylvan_bdd_matches_variable_index(BDD node, uint64_t variableIndex, int64_t offset = 0) {
return !sylvan_isconst(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
}
/*!
* Retrieves whether the topmost variable in the MTBDD is the one with the given index.
*
* @param node The top node of the BDD.
* @param variableIndex The variable index.
* @param offset An offset that is applied to the index of the top variable in the BDD.
* @return True iff the BDD's top variable has the given index.
*/
bool sylvan_mtbdd_matches_variable_index(MTBDD node, uint64_t variableIndex, int64_t offset = 0) {
return !mtbdd_isleaf(node) && static_cast<uint64_t>(sylvan_var(node) + offset) == variableIndex;
}
}
}
#pragma GCC diagnostic pop
#pragma clang diagnostic pop
Write Preview
Loading…
Cancel
Save