diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp index e831df563..85083da5d 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -10,6 +10,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StochasticTwoPlayerGame.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/modelchecker/CheckTask.h" #include "storm/modelchecker/results/CheckResult.h" diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp index 8feab2495..b41ddaca5 100644 --- a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp @@ -3,6 +3,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StochasticTwoPlayerGame.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/abstraction/SymbolicStateSet.h" diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index 26423bb87..1f63fcd64 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -3,6 +3,7 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StochasticTwoPlayerGame.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" diff --git a/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.cpp new file mode 100644 index 000000000..08a1585e7 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.cpp @@ -0,0 +1,367 @@ +#include "storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h" + +#include "storm/storage/dd/DdManager.h" + +#include "storm/storage/dd/bisimulation/Partition.h" +#include "storm/storage/dd/bisimulation/Signature.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + InternalSignatureRefiner::InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), ddman(manager.getInternalDdManager().getCuddManager().getManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache(), reuseBlocksCache() { + + // 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(static_cast(manager.getInternalDdManager().getCuddManager().ReadSize()), static_cast(2)); + } + + template + Partition InternalSignatureRefiner::refine(Partition const& oldPartition, Signature const& signature) { + std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd());; + ++numberOfRefinements; + return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); + } + + template + void InternalSignatureRefiner::clearCaches() { + signatureCache.clear(); + reuseBlocksCache.clear(); + } + + template + std::pair, boost::optional>> InternalSignatureRefiner::refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); + + nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; + + // Perform the actual recursive refinement step. + std::pair 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. + storm::dd::InternalAdd internalNewPartitionAdd(&manager.getInternalDdManager(), cudd::ADD(manager.getInternalDdManager().getCuddManager(), result.first)); + storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); + + boost::optional> optionalChangedAdd; + if (result.second) { + storm::dd::InternalAdd internalChangedAdd(&manager.getInternalDdManager(), cudd::ADD(manager.getInternalDdManager().getCuddManager(), result.second)); + storm::dd::Add changedAdd(oldPartition.asAdd().getDdManager(), internalChangedAdd, stateVariables); + optionalChangedAdd = changedAdd; + } + + clearCaches(); + return std::make_pair(newPartitionAdd, optionalChangedAdd); + } + + template + DdNodePtr InternalSignatureRefiner::encodeBlock(uint64_t blockIndex) { + for (auto const& blockDdVariableIndex : blockDdVariableIndices) { + blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0; + blockIndex >>= 1; + } + 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; + } + + template + std::pair InternalSignatureRefiner::reuseOrRelabel(DdNode* partitionNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { + // If we arrived at the constant zero node, then this was an illegal state encoding. + if (partitionNode == Cudd_ReadZero(ddman)) { + if (options.createChangedStates) { + return std::make_pair(partitionNode, Cudd_ReadZero(ddman)); + } else { + return std::make_pair(partitionNode, nullptr); + } + } + + // Check the cache whether we have seen the same node before. + auto nodePair = std::make_pair(nullptr, partitionNode); + + auto it = signatureCache.find(nodePair); + if (it != signatureCache.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)) { + if (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& reuseEntry = reuseBlocksCache[partitionNode]; + if (!reuseEntry.isReused()) { + reuseEntry.setReused(); + std::pair result = std::make_pair(partitionNode, options.createChangedStates ? Cudd_ReadZero(ddman) : nullptr); + signatureCache[nodePair] = result; + return result; + } + } + + std::pair result = std::make_pair(encodeBlock(nextFreeBlockIndex++), options.createChangedStates ? Cudd_ReadOne(ddman) : nullptr); + signatureCache[nodePair] = 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* partitionThen; + DdNode* partitionElse; + 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(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + partitionThen = Cudd_T(partitionNode); + partitionElse = Cudd_E(partitionNode); + skipped = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + // 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 reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + std::pair combinedThenResult = reuseOrRelabel(partitionThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNodePtr thenResult = combinedThenResult.first; + DdNodePtr changedThenResult = combinedThenResult.second; + Cudd_Ref(thenResult); + if (options.createChangedStates) { + Cudd_Ref(changedThenResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); + } + std::pair combinedElseResult = reuseOrRelabel(partitionElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNodePtr elseResult = combinedElseResult.first; + DdNodePtr changedElseResult = combinedElseResult.second; + Cudd_Ref(elseResult); + if (options.createChangedStates) { + Cudd_Ref(changedElseResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); + } + + DdNodePtr 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); + } + + DdNodePtr changedResult = nullptr; + if (options.createChangedStates) { + if (changedThenResult == changedElseResult) { + Cudd_Deref(changedThenResult); + Cudd_Deref(changedElseResult); + changedResult = changedThenResult; + } else { + // Get the node to connect the subresults. + bool complemented = Cudd_IsComplement(changedThenResult); + changedResult = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(changedThenResult), complemented ? Cudd_Not(changedElseResult) : changedElseResult); + if (complemented) { + changedResult = Cudd_Not(changedResult); + } + Cudd_Deref(changedThenResult); + Cudd_Deref(changedElseResult); + } + } + + // Store the result in the cache. + auto pairResult = std::make_pair(result, changedResult); + signatureCache[nodePair] = pairResult; + return pairResult; + } + } + + template + std::pair InternalSignatureRefiner::refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { + // If we arrived at the constant zero node, then this was an illegal state encoding. + if (partitionNode == Cudd_ReadZero(ddman)) { + if (options.createChangedStates) { + return std::make_pair(partitionNode, Cudd_ReadZero(ddman)); + } else { + return std::make_pair(partitionNode, nullptr); + } + } else if (signatureNode == Cudd_ReadZero(ddman)) { + std::pair result = reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + return result; + } + + // Check the cache whether we have seen the same node before. + auto nodePair = std::make_pair(signatureNode, partitionNode); + + auto it = signatureCache.find(nodePair); + if (it != signatureCache.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)) { + if (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& reuseEntry = reuseBlocksCache[partitionNode]; + if (!reuseEntry.isReused()) { + reuseEntry.setReused(); + std::pair result = std::make_pair(partitionNode, options.createChangedStates ? Cudd_ReadZero(ddman) : nullptr); + signatureCache[nodePair] = result; + return result; + } + } + + std::pair result = std::make_pair(encodeBlock(nextFreeBlockIndex++), options.createChangedStates ? Cudd_ReadOne(ddman) : nullptr); + signatureCache[nodePair] = 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 skippedBoth = true; + DdNode* partitionThen; + DdNode* partitionElse; + DdNode* signatureThen; + DdNode* signatureElse; + short offset; + bool isNondeterminismVariable = false; + while (skippedBoth && !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(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + partitionThen = Cudd_T(partitionNode); + partitionElse = Cudd_E(partitionNode); + skippedBoth = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { + signatureThen = Cudd_T(signatureNode); + signatureElse = Cudd_E(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 = 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 refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + std::pair combinedThenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNodePtr thenResult = combinedThenResult.first; + DdNodePtr changedThenResult = combinedThenResult.second; + Cudd_Ref(thenResult); + if (options.createChangedStates) { + Cudd_Ref(changedThenResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); + } + std::pair combinedElseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); + DdNodePtr elseResult = combinedElseResult.first; + DdNodePtr changedElseResult = combinedElseResult.second; + Cudd_Ref(elseResult); + if (options.createChangedStates) { + Cudd_Ref(changedElseResult); + } else { + STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); + } + + DdNodePtr 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); + } + + DdNodePtr changedResult = nullptr; + if (options.createChangedStates) { + if (changedThenResult == changedElseResult) { + Cudd_Deref(changedThenResult); + Cudd_Deref(changedElseResult); + changedResult = changedThenResult; + } else { + // Get the node to connect the subresults. + bool complemented = Cudd_IsComplement(changedThenResult); + changedResult = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(changedThenResult), complemented ? Cudd_Not(changedElseResult) : changedElseResult); + if (complemented) { + changedResult = Cudd_Not(changedResult); + } + Cudd_Deref(changedThenResult); + Cudd_Deref(changedElseResult); + } + } + + // Store the result in the cache. + auto pairResult = std::make_pair(result, changedResult); + signatureCache[nodePair] = pairResult; + return pairResult; + } + } + + template class InternalSignatureRefiner; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h new file mode 100644 index 000000000..3e8be9964 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h @@ -0,0 +1,84 @@ +#pragma once + +#include +#include + +#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" + +#include "storm/storage/dd/Bdd.h" + +#include "storm/storage/expressions/Variable.h" + +#include "storm/storage/dd/cudd/utility.h" + +#include + +namespace storm { + namespace dd { + + template + class DdManager; + + template + class Add; + + namespace bisimulation { + + template + class Partition; + + template + class Signature; + + template + class InternalSignatureRefiner { + public: + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options = InternalSignatureRefinerOptions()); + + Partition refine(Partition const& oldPartition, Signature const& signature); + + private: + void clearCaches(); + + std::pair, boost::optional>> refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd); + + DdNodePtr encodeBlock(uint64_t blockIndex); + + std::pair reuseOrRelabel(DdNode* partitionNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode); + + std::pair refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode); + + storm::dd::DdManager const& manager; + ::DdManager* ddman; + storm::expressions::Variable blockVariable; + std::set stateVariables; + + // The cubes representing all non-block and all nondeterminism variables, respectively. + storm::dd::Bdd nondeterminismVariables; + storm::dd::Bdd nonBlockVariables; + + // The provided options. + InternalSignatureRefinerOptions options; + + // The indices of the DD variables associated with the block variable. + std::vector blockDdVariableIndices; + + // A vector used for encoding block indices. + std::vector blockEncoding; + + // 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, CuddPointerPairHash> signatureCache; + + // The cache used to identify which old block numbers have already been reused. + spp::sparse_hash_map reuseBlocksCache; + }; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.cpp new file mode 100644 index 000000000..90aebf216 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.cpp @@ -0,0 +1,45 @@ +#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/BisimulationSettings.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + InternalSignatureRefinerOptions::InternalSignatureRefinerOptions() : InternalSignatureRefinerOptions(true) { + // Intentionally left empty. + } + + InternalSignatureRefinerOptions::InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true), parallel(false) { + auto const& bisimulationSettings = storm::settings::getModule(); + + storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); + this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers; + + 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; + } + + ReuseWrapper::ReuseWrapper() : ReuseWrapper(false) { + // Intentionally left empty. + } + + ReuseWrapper::ReuseWrapper(bool value) : value(value) { + // Intentionally left empty. + } + + bool ReuseWrapper::isReused() const { + return value; + } + + void ReuseWrapper::setReused() { + value = true; + } + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h new file mode 100644 index 000000000..0b3f3309a --- /dev/null +++ b/src/storm/storage/dd/bisimulation/InternalSignatureRefiner.h @@ -0,0 +1,36 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + class InternalSignatureRefiner; + + struct InternalSignatureRefinerOptions { + InternalSignatureRefinerOptions(); + InternalSignatureRefinerOptions(bool shiftStateVariables); + + bool shiftStateVariables; + bool reuseBlockNumbers; + bool createChangedStates; + bool parallel; + }; + + class ReuseWrapper { + public: + ReuseWrapper(); + ReuseWrapper(bool value); + + bool isReused() const; + void setReused(); + + private: + bool value; + }; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp new file mode 100644 index 000000000..f41b9edaa --- /dev/null +++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.cpp @@ -0,0 +1,632 @@ +#include "storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h" + +#include "storm/storage/dd/DdManager.h" + +#include "storm/storage/dd/bisimulation/Partition.h" +#include "storm/storage/dd/bisimulation/Signature.h" + +#include "sylvan_cache.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + InternalSylvanSignatureRefinerBase::InternalSylvanSignatureRefinerBase(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : manager(manager), 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(), resize(0) { + + // Perform garbage collection to clean up stuff not needed anymore. + LACE_ME; + sylvan_gc(); + + table.resize(3 * 8 * (1ull << 14)); + } + + BDD InternalSylvanSignatureRefinerBase::encodeBlock(uint64_t blockIndex) { + std::vector 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()); + } + + + template + InternalSignatureRefiner::InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : storm::dd::bisimulation::InternalSylvanSignatureRefinerBase(manager, blockVariable, stateVariables, nondeterminismVariables, nonBlockVariables, options) { + + // Intentionally left empty. + } + + template + Partition InternalSignatureRefiner::refine(Partition const& oldPartition, Signature const& signature) { + std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd()); + ++numberOfRefinements; + return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); + } + + template + void InternalSignatureRefiner::clearCaches() { + signatureCache.clear(); + reuseBlocksCache.clear(); + this->table = std::vector(table.size()); + this->signatures = std::vector(signatures.size()); + } + + template + std::pair, boost::optional>> InternalSignatureRefiner::refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { + STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); + + nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; + signatures.resize(nextFreeBlockIndex); + + // Perform the actual recursive refinement step. + std::pair 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 internalNewPartitionBdd(&manager.getInternalDdManager(), sylvan::Bdd(result.first)); + storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); + + boost::optional> optionalChangedBdd; + if (options.createChangedStates && result.second != 0) { + storm::dd::InternalBdd internalChangedBdd(&manager.getInternalDdManager(), sylvan::Bdd(result.second)); + storm::dd::Bdd changedBdd(oldPartition.asBdd().getDdManager(), internalChangedBdd, stateVariables); + optionalChangedBdd = changedBdd; + } + + clearCaches(); + return std::make_pair(newPartitionBdd, optionalChangedBdd); + } + + template + std::pair InternalSignatureRefiner::reuseOrRelabel(BDD partitionNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + LACE_ME; + + if (partitionNode == sylvan_false) { + if (options.createChangedStates) { + return std::make_pair(sylvan_false, sylvan_false); + } else { + return std::make_pair(sylvan_false, 0); + } + } + + // Check the cache whether we have seen the same node before. + auto nodePair = std::make_pair(0, partitionNode); + auto it = signatureCache.find(nodePair); + if (it != signatureCache.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)) { + if (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 = reuseBlocksCache[partitionNode]; + if (!reuseBlockEntry.isReused()) { + reuseBlockEntry.setReused(); + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(partitionNode, sylvan_false); + } else { + result = std::make_pair(partitionNode, 0); + } + signatureCache[nodePair] = result; + return result; + } + } + + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), sylvan_true); + } else { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), 0); + } + signatureCache[nodePair] = 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; + BDD partitionThen; + BDD partitionElse; + 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 (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { + partitionThen = sylvan_high(partitionNode); + partitionElse = sylvan_low(partitionNode); + skipped = false; + } else { + partitionThen = partitionElse = partitionNode; + } + + // 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 reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + std::pair combinedThenResult = reuseOrRelabel(partitionThen, 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 combinedElseResult = reuseOrRelabel(partitionElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD elseResult = combinedElseResult.first; + bdd_refs_push(elseResult); + BDD changedElseResult = combinedElseResult.second; + if (options.createChangedStates) { + bdd_refs_push(changedElseResult); + } + + std::pair result; + if (thenResult == elseResult) { + result.first = thenResult; + } else { + // Get the node to connect the subresults. + result.first = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); + } + + result.second = 0; + if (options.createChangedStates) { + if (changedThenResult == changedElseResult) { + result.second = changedThenResult; + } else { + // Get the node to connect the subresults. + result.second = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, changedElseResult, changedThenResult); + } + } + + // Dispose of the intermediate results. + if (options.createChangedStates) { + bdd_refs_pop(4); + } else { + bdd_refs_pop(2); + } + + // Store the result in the cache. + signatureCache[nodePair] = result; + return result; + } + } + + template + std::pair InternalSignatureRefiner::refineParallel(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { + LACE_ME; + // return std::make_pair(CALL(refine_parallel, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0); + return std::make_pair(CALL(sylvan_refine_partition, signatureNode, nonBlockVariablesNode, partitionNode, this), 0); + } + + template + std::pair InternalSignatureRefiner::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 + // all states to be non-deadlock). + if (partitionNode == sylvan_false) { + if (options.createChangedStates) { + return std::make_pair(sylvan_false, sylvan_false); + } else { + return std::make_pair(sylvan_false, 0); + } + } else if (mtbdd_iszero(signatureNode)) { + std::pair result = reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); + signatureCache[std::make_pair(signatureNode, partitionNode)] = result; + return result; + } + + STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node."); + + // Check the cache whether we have seen the same node before. + auto nodePair = std::make_pair(signatureNode, partitionNode); + auto it = signatureCache.find(nodePair); + if (it != signatureCache.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)) { + if (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 = reuseBlocksCache[partitionNode]; + if (!reuseBlockEntry.isReused()) { + reuseBlockEntry.setReused(); + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(partitionNode, sylvan_false); + } else { + result = std::make_pair(partitionNode, 0); + } + signatureCache[nodePair] = result; + return result; + } + } + + std::pair result; + if (options.createChangedStates) { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), sylvan_true); + } else { + result = std::make_pair(encodeBlock(nextFreeBlockIndex++), 0); + } + signatureCache[nodePair] = 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 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 = 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); + } + } + } + + // If there are no more non-block variables remaining, make a recursive call to enter the base case. + if (sylvan_isconst(nonBlockVariablesNode)) { + return refineSequential(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); + } + + std::pair 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 combinedElseResult = refineSequential(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); + BDD elseResult = combinedElseResult.first; + bdd_refs_push(elseResult); + BDD changedElseResult = combinedElseResult.second; + if (options.createChangedStates) { + bdd_refs_push(changedElseResult); + } + + std::pair result; + if (thenResult == elseResult) { + result.first = thenResult; + } else { + // Get the node to connect the subresults. + result.first = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); + } + + result.second = 0; + if (options.createChangedStates) { + if (changedThenResult == changedElseResult) { + result.second = changedThenResult; + } else { + // Get the node to connect the subresults. + result.second = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, changedElseResult, changedThenResult); + } + } + + // Dispose of the intermediate results. + if (options.createChangedStates) { + bdd_refs_pop(4); + } else { + bdd_refs_pop(2); + } + + // Store the result in the cache. + signatureCache[nodePair] = result; + + return result; + } + } + +#define cas(ptr, old, new) (__sync_bool_compare_and_swap((ptr),(old),(new))) +#define ATOMIC_READ(x) (*(volatile decltype(x) *)&(x)) + + /* Rotating 64-bit FNV-1a hash */ + static uint64_t + sylvan_hash(uint64_t a, uint64_t b) + { + const uint64_t prime = 1099511628211; + uint64_t hash = 14695981039346656037LLU; + hash = (hash ^ (a>>32)); + hash = (hash ^ a) * prime; + hash = (hash ^ b) * prime; + return hash ^ (hash>>32); + } + + VOID_TASK_3(sylvan_rehash, size_t, first, size_t, count, void*, refinerPtr) + { + auto& refiner = *static_cast(refinerPtr); + + if (count > 128) { + SPAWN(sylvan_rehash, first, count/2, refinerPtr); + CALL(sylvan_rehash, first+count/2, count-count/2, refinerPtr); + SYNC(sylvan_rehash); + return; + } + + while (count--) { + uint64_t *old_ptr = refiner.oldTable.data() + first*3; + uint64_t a = old_ptr[0]; + uint64_t b = old_ptr[1]; + uint64_t c = old_ptr[2]; + + uint64_t hash = sylvan_hash(a, b); + uint64_t pos = hash % (refiner.table.size() / 3); + + volatile uint64_t *ptr = 0; + for (;;) { + ptr = refiner.table.data() + pos*3; + if (*ptr == 0) { + if (cas(ptr, 0, a)) { + ptr[1] = b; + ptr[2] = c; + break; + } + } + pos++; + if (pos >= (refiner.table.size() / 3)) pos = 0; + } + + first++; + } + } + + VOID_TASK_1(sylvan_grow_it, void*, refinerPtr) + { + auto& refiner = *static_cast(refinerPtr); + + refiner.oldTable = std::move(refiner.table); + + refiner.table = std::vector(refiner.oldTable.size() << 1); + + CALL(sylvan_rehash, 0, refiner.oldTable.size() / 3, refinerPtr); + + refiner.oldTable.clear(); + } + + VOID_TASK_1(sylvan_grow, void*, refinerPtr) + { + auto& refiner = *static_cast(refinerPtr); + + if (cas(&refiner.resize, 0, 1)) { + NEWFRAME(sylvan_grow_it, refinerPtr); + refiner.resize = 0; + } else { + /* wait for new frame to appear */ + while (ATOMIC_READ(lace_newframe.t) == 0) {} + lace_yield(__lace_worker, __lace_dq_head); + } + } + + static uint64_t + sylvan_search_or_insert(uint64_t sig, uint64_t previous_block, void* refinerPtr) + { + auto& refiner = *static_cast(refinerPtr); + + uint64_t hash = sylvan_hash(sig, previous_block); + uint64_t pos = hash % (refiner.table.size() / 3); + + volatile uint64_t *ptr = 0; + uint64_t a, b, c; + int count = 0; + for (;;) { + ptr = refiner.table.data() + pos*3; + a = *ptr; + if (a == sig) { + while ((b=ptr[1]) == 0) continue; + if (b == previous_block) { + while ((c=ptr[2]) == 0) continue; + return c; + } + } else if (a == 0) { + if (cas(ptr, 0, sig)) { + c = ptr[2] = __sync_fetch_and_add(&refiner.nextFreeBlockIndex, 1); + ptr[1] = previous_block; + return c; + } else { + continue; + } + } + pos++; + if (pos >= (refiner.table.size() / 3)) pos = 0; + if (++count >= 128) return 0; + } + } + + TASK_1(uint64_t, sylvan_decode_block, BDD, block) + { + uint64_t result = 0; + uint64_t mask = 1; + while (block != sylvan_true) { + BDD b_low = sylvan_low(block); + if (b_low == sylvan_false) { + result |= mask; + block = sylvan_high(block); + } else { + block = b_low; + } + mask <<= 1; + } + return result; + } + + TASK_3(BDD, sylvan_assign_block, BDD, sig, BDD, previous_block, void*, refinerPtr) + { + assert(previous_block != mtbdd_false); // if so, incorrect call! + + auto& refiner = *static_cast(refinerPtr); + + // maybe do garbage collection + sylvan_gc_test(); + + if (sig == sylvan_false) { + // slightly different handling because sylvan_false == 0 + sig = (uint64_t)-1; + } + + // try to claim previous block number + const uint64_t p_b = CALL(sylvan_decode_block, previous_block); + assert(p_b != 0); + + for (;;) { + BDD cur = *(volatile BDD*)&refiner.signatures[p_b]; + if (cur == sig) return previous_block; + if (cur != 0) break; + if (cas(&refiner.signatures[p_b], 0, sig)) return previous_block; + } + + // no previous block number, search or insert + uint64_t c; + while ((c = sylvan_search_or_insert(sig, previous_block, refinerPtr)) == 0) CALL(sylvan_grow, refinerPtr); + + // if (c >= refiner.signatures.size()) { + // fprintf(stderr, "Out of cheese exception, no more blocks available\n"); + // exit(1); + // } + + // return CALL(refiner.encodeBlock(c)); + return refiner.encodeBlock(c); + } + + TASK_4(BDD, sylvan_refine_partition, BDD, dd, BDD, vars, BDD, previous_partition, void*, refinerPtr) + { + auto& refiner = *static_cast(refinerPtr); + + /* expecting dd as in s,a,B */ + /* expecting vars to be conjunction of variables in s */ + /* expecting previous_partition as in t,B */ + + if (previous_partition == sylvan_false) { + /* it had no block in the previous iteration, therefore also not now */ + return sylvan_false; + } + + if (sylvan_set_isempty(vars)) { + BDD result; + if (cache_get(dd|(256LL<<42), vars, previous_partition|(refiner.numberOfRefinements<<40), &result)) return result; + result = CALL(sylvan_assign_block, dd, previous_partition, refinerPtr); + cache_put(dd|(256LL<<42), vars, previous_partition|(refiner.numberOfRefinements<<40), result); + return result; + } + + sylvan_gc_test(); + + /* vars != sylvan_false */ + /* dd cannot be sylvan_true - if vars != sylvan_true, then dd is in a,B */ + + BDDVAR dd_var = sylvan_isconst(dd) ? 0xffffffff : sylvan_var(dd); + BDDVAR pp_var = sylvan_var(previous_partition); + BDDVAR vars_var = sylvan_var(vars); + + while (vars_var < dd_var && vars_var+1 < pp_var) { + vars = sylvan_set_next(vars); + if (sylvan_set_isempty(vars)) return CALL(sylvan_refine_partition, dd, vars, previous_partition, refinerPtr); + vars_var = sylvan_var(vars); + } + + /* Consult cache */ + BDD result; + if (cache_get(dd|(256LL<<42), vars, previous_partition|(refiner.numberOfRefinements<<40), &result)) { + return result; + } + + /* Compute cofactors */ + BDD dd_low, dd_high; + if (vars_var == dd_var) { + dd_low = sylvan_low(dd); + dd_high = sylvan_high(dd); + } else { + dd_low = dd_high = dd; + } + + BDD pp_low, pp_high; + if (vars_var+1 == pp_var) { + pp_low = sylvan_low(previous_partition); + pp_high = sylvan_high(previous_partition); + } else { + pp_low = pp_high = previous_partition; + } + + /* Recursive steps */ + BDD next_vars = sylvan_set_next(vars); + bdd_refs_spawn(SPAWN(sylvan_refine_partition, dd_low, next_vars, pp_low, refinerPtr)); + BDD high = bdd_refs_push(CALL(sylvan_refine_partition, dd_high, next_vars, pp_high, refinerPtr)); + BDD low = bdd_refs_sync(SYNC(sylvan_refine_partition)); + bdd_refs_pop(1); + + /* rename from s to t */ + result = sylvan_makenode(vars_var+1, low, high); + + /* Write to cache */ + cache_put(dd|(256LL<<42), vars, previous_partition|(refiner.numberOfRefinements<<40), result); + return result; + } + + template class InternalSignatureRefiner; + template class InternalSignatureRefiner; + template class InternalSignatureRefiner; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h new file mode 100644 index 000000000..7105a5bff --- /dev/null +++ b/src/storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h @@ -0,0 +1,85 @@ +#pragma once + +#include "storm/storage/dd/bisimulation/InternalSignatureRefiner.h" + +#include "storm/storage/dd/Bdd.h" + +#include "storm/storage/expressions/Variable.h" + +#include "storm/storage/dd/sylvan/utility.h" + +#include + +namespace storm { + namespace dd { + template + class DdManager; + + namespace bisimulation { + + template + class Partition; + + template + class Signature; + + class InternalSylvanSignatureRefinerBase { + public: + InternalSylvanSignatureRefinerBase(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options); + + BDD encodeBlock(uint64_t blockIndex); + + storm::dd::DdManager const& manager; + storm::expressions::Variable blockVariable; + std::set stateVariables; + + storm::dd::Bdd nondeterminismVariables; + storm::dd::Bdd nonBlockVariables; + + // The provided options. + InternalSignatureRefinerOptions options; + + uint64_t numberOfBlockVariables; + + storm::dd::Bdd 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, SylvanMTBDDPairHash> signatureCache; + + // The cache used to identify which old block numbers have already been reused. + spp::sparse_hash_map reuseBlocksCache; + + // Data used by sylvan implementation. + std::vector signatures; + std::vector table; + std::vector oldTable; + uint64_t resize; + }; + + template + class InternalSignatureRefiner : public InternalSylvanSignatureRefinerBase { + public: + InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options); + + Partition refine(Partition const& oldPartition, Signature const& signature); + + private: + void clearCaches(); + + std::pair, boost::optional>> refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd); + + std::pair reuseOrRelabel(BDD partitionNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode); + std::pair refineParallel(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode); + std::pair refineSequential(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode); + + }; + + } + } +} diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index d3708c6a5..9f441be1b 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -135,7 +135,7 @@ namespace storm { storm::dd::Bdd partitionBdd = manager.getBddZero(); storm::dd::Bdd transitionMatrixBdd = model.getTransitionMatrix().notZero().existsAbstract(model.getNondeterminismVariables()); storm::dd::Bdd coveredStates = manager.getBddZero(); - uint64_t blockCount = 0; + uint64_t blockCount = 1; // Backward BFS. storm::dd::Bdd backwardFrontier = targetStates; @@ -244,7 +244,7 @@ namespace storm { template uint64_t Partition::getNumberOfBlocks() const { - return numberOfBlocks; + return numberOfBlocks - 1; } template @@ -311,7 +311,7 @@ namespace storm { template std::pair, uint64_t> Partition::createPartitionBdd(storm::dd::DdManager const& manager, storm::models::symbolic::Model const& model, std::vector> const& stateSets, storm::expressions::Variable const& blockVariable) { - uint64_t blockCount = 0; + uint64_t blockCount = 1; storm::dd::Bdd partitionBdd = manager.getBddZero(); // Enumerate all realizable blocks. diff --git a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp index e5c11b3d3..a17eb9912 100644 --- a/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureRefiner.cpp @@ -1,1023 +1,14 @@ #include "storm/storage/dd/bisimulation/SignatureRefiner.h" -#include -#include - -#include -#include - #include "storm/storage/dd/DdManager.h" -#include "storm/storage/dd/cudd/InternalCuddDdManager.h" - -#include "storm/storage/dd/cudd/utility.h" -#include "storm/storage/dd/sylvan/utility.h" - -#include "storm/utility/macros.h" -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/InvalidArgumentException.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/BisimulationSettings.h" - -#include - -#include "sylvan_cache.h" -#include "sylvan_table.h" -#include "sylvan_int.h" - -#ifdef STORM_HAVE_INTELTBB -#include "tbb/tbb.h" -#else -#error "Need TBB at this point." -#endif +#include "storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h" +#include "storm/storage/dd/bisimulation/InternalSylvanSignatureRefiner.h" namespace storm { namespace dd { namespace bisimulation { - template - class InternalSignatureRefiner; - - struct InternalSignatureRefinerOptions { - InternalSignatureRefinerOptions() : InternalSignatureRefinerOptions(true) { - // Intentionally left empty. - } - - InternalSignatureRefinerOptions(bool shiftStateVariables) : shiftStateVariables(shiftStateVariables), createChangedStates(true), parallel(false) { - auto const& bisimulationSettings = storm::settings::getModule(); - - storm::settings::modules::BisimulationSettings::ReuseMode reuseMode = bisimulationSettings.getReuseMode(); - this->reuseBlockNumbers = reuseMode == storm::settings::modules::BisimulationSettings::ReuseMode::BlockNumbers; - - 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 { - public: - ReuseWrapper() : ReuseWrapper(false) { - // Intentionally left empty. - } - - ReuseWrapper(bool value) : value(value) { - // Intentionally left empty. - } - - bool isReused() const { - return value; - } - - void setReused() { - value = true; - } - - private: - bool value; - }; - - template - class InternalSignatureRefiner { - public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options = InternalSignatureRefinerOptions()) : manager(manager), internalDdManager(manager.getInternalDdManager()), ddman(internalDdManager.getCuddManager().getManager()), blockVariable(blockVariable), stateVariables(stateVariables), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), options(options), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) { - - // 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(static_cast(internalDdManager.getCuddManager().ReadSize()), static_cast(2)); - } - - Partition refine(Partition const& oldPartition, Signature const& signature) { - std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd());; - ++numberOfRefinements; - return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); - } - - private: - void clearCaches() { - signatureCache.clear(); - reuseBlocksCache.clear(); - } - - std::pair, boost::optional>> refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { - STORM_LOG_ASSERT(oldPartition.storedAsAdd(), "Expecting partition to be stored as ADD for CUDD."); - - nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; - - // Perform the actual recursive refinement step. - std::pair 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. - storm::dd::InternalAdd internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result.first)); - storm::dd::Add newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables()); - - boost::optional> optionalChangedAdd; - if (result.second) { - storm::dd::InternalAdd internalChangedAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result.second)); - storm::dd::Add changedAdd(oldPartition.asAdd().getDdManager(), internalChangedAdd, stateVariables); - optionalChangedAdd = changedAdd; - } - - clearCaches(); - return std::make_pair(newPartitionAdd, optionalChangedAdd); - } - - DdNodePtr encodeBlock(uint64_t blockIndex) { - for (auto const& blockDdVariableIndex : blockDdVariableIndices) { - blockEncoding[blockDdVariableIndex] = blockIndex & 1 ? 1 : 0; - blockIndex >>= 1; - } - 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; - } - - std::pair reuseOrRelabel(DdNode* partitionNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { - // If we arrived at the constant zero node, then this was an illegal state encoding. - if (partitionNode == Cudd_ReadZero(ddman)) { - if (options.createChangedStates) { - return std::make_pair(partitionNode, Cudd_ReadZero(ddman)); - } else { - return std::make_pair(partitionNode, nullptr); - } - } - - // Check the cache whether we have seen the same node before. - auto nodePair = std::make_pair(nullptr, partitionNode); - - auto it = signatureCache.find(nodePair); - if (it != signatureCache.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)) { - if (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& reuseEntry = reuseBlocksCache[partitionNode]; - if (!reuseEntry.isReused()) { - reuseEntry.setReused(); - std::pair result = std::make_pair(partitionNode, options.createChangedStates ? Cudd_ReadZero(ddman) : nullptr); - signatureCache[nodePair] = result; - return result; - } - } - - std::pair result = std::make_pair(encodeBlock(nextFreeBlockIndex++), options.createChangedStates ? Cudd_ReadOne(ddman) : nullptr); - signatureCache[nodePair] = 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* partitionThen; - DdNode* partitionElse; - 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(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - partitionThen = Cudd_T(partitionNode); - partitionElse = Cudd_E(partitionNode); - skipped = false; - } else { - partitionThen = partitionElse = partitionNode; - } - - // 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 reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); - } - - std::pair combinedThenResult = reuseOrRelabel(partitionThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); - DdNodePtr thenResult = combinedThenResult.first; - DdNodePtr changedThenResult = combinedThenResult.second; - Cudd_Ref(thenResult); - if (options.createChangedStates) { - Cudd_Ref(changedThenResult); - } else { - STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); - } - std::pair combinedElseResult = reuseOrRelabel(partitionElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); - DdNodePtr elseResult = combinedElseResult.first; - DdNodePtr changedElseResult = combinedElseResult.second; - Cudd_Ref(elseResult); - if (options.createChangedStates) { - Cudd_Ref(changedElseResult); - } else { - STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); - } - - DdNodePtr 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); - } - - DdNodePtr changedResult = nullptr; - if (options.createChangedStates) { - if (changedThenResult == changedElseResult) { - Cudd_Deref(changedThenResult); - Cudd_Deref(changedElseResult); - changedResult = changedThenResult; - } else { - // Get the node to connect the subresults. - bool complemented = Cudd_IsComplement(changedThenResult); - changedResult = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(changedThenResult), complemented ? Cudd_Not(changedElseResult) : changedElseResult); - if (complemented) { - changedResult = Cudd_Not(changedResult); - } - Cudd_Deref(changedThenResult); - Cudd_Deref(changedElseResult); - } - } - - // Store the result in the cache. - auto pairResult = std::make_pair(result, changedResult); - signatureCache[nodePair] = pairResult; - return pairResult; - } - } - - std::pair refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) { - // If we arrived at the constant zero node, then this was an illegal state encoding. - if (partitionNode == Cudd_ReadZero(ddman)) { - if (options.createChangedStates) { - return std::make_pair(partitionNode, Cudd_ReadZero(ddman)); - } else { - return std::make_pair(partitionNode, nullptr); - } - } else if (signatureNode == Cudd_ReadZero(ddman)) { - std::pair result = reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); - signatureCache[std::make_pair(signatureNode, partitionNode)] = result; - return result; - } - - // Check the cache whether we have seen the same node before. - auto nodePair = std::make_pair(signatureNode, partitionNode); - - auto it = signatureCache.find(nodePair); - if (it != signatureCache.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)) { - if (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& reuseEntry = reuseBlocksCache[partitionNode]; - if (!reuseEntry.isReused()) { - reuseEntry.setReused(); - std::pair result = std::make_pair(partitionNode, options.createChangedStates ? Cudd_ReadZero(ddman) : nullptr); - signatureCache[nodePair] = result; - return result; - } - } - - std::pair result = std::make_pair(encodeBlock(nextFreeBlockIndex++), options.createChangedStates ? Cudd_ReadOne(ddman) : nullptr); - signatureCache[nodePair] = 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 skippedBoth = true; - DdNode* partitionThen; - DdNode* partitionElse; - DdNode* signatureThen; - DdNode* signatureElse; - short offset; - bool isNondeterminismVariable = false; - while (skippedBoth && !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(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - partitionThen = Cudd_T(partitionNode); - partitionElse = Cudd_E(partitionNode); - skippedBoth = false; - } else { - partitionThen = partitionElse = partitionNode; - } - - if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) { - signatureThen = Cudd_T(signatureNode); - signatureElse = Cudd_E(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 = 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 refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); - } - - std::pair combinedThenResult = refine(partitionThen, signatureThen, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); - DdNodePtr thenResult = combinedThenResult.first; - DdNodePtr changedThenResult = combinedThenResult.second; - Cudd_Ref(thenResult); - if (options.createChangedStates) { - Cudd_Ref(changedThenResult); - } else { - STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); - } - std::pair combinedElseResult = refine(partitionElse, signatureElse, isNondeterminismVariable ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode)); - DdNodePtr elseResult = combinedElseResult.first; - DdNodePtr changedElseResult = combinedElseResult.second; - Cudd_Ref(elseResult); - if (options.createChangedStates) { - Cudd_Ref(changedElseResult); - } else { - STORM_LOG_ASSERT(!changedThenResult, "Expected not changed state DD."); - } - - DdNodePtr 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); - } - - DdNodePtr changedResult = nullptr; - if (options.createChangedStates) { - if (changedThenResult == changedElseResult) { - Cudd_Deref(changedThenResult); - Cudd_Deref(changedElseResult); - changedResult = changedThenResult; - } else { - // Get the node to connect the subresults. - bool complemented = Cudd_IsComplement(changedThenResult); - changedResult = cuddUniqueInter(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset, Cudd_Regular(changedThenResult), complemented ? Cudd_Not(changedElseResult) : changedElseResult); - if (complemented) { - changedResult = Cudd_Not(changedResult); - } - Cudd_Deref(changedThenResult); - Cudd_Deref(changedElseResult); - } - } - - // Store the result in the cache. - auto pairResult = std::make_pair(result, changedResult); - signatureCache[nodePair] = pairResult; - return pairResult; - } - } - - storm::dd::DdManager const& manager; - storm::dd::InternalDdManager const& internalDdManager; - ::DdManager* ddman; - storm::expressions::Variable blockVariable; - std::set stateVariables; - - // The cubes representing all non-block and all nondeterminism variables, respectively. - storm::dd::Bdd nondeterminismVariables; - storm::dd::Bdd nonBlockVariables; - - // The provided options. - InternalSignatureRefinerOptions options; - - // The indices of the DD variables associated with the block variable. - std::vector blockDdVariableIndices; - - // A vector used for encoding block indices. - std::vector blockEncoding; - - // The current number of blocks of the new partition. - uint64_t nextFreeBlockIndex; - - // The number of completed refinements. - uint64_t numberOfRefinements; - - // The number of nodes visited in the last refinement operation. - uint64_t lastNumberOfVisitedNodes; - - // The cache used to identify states with identical signature. - spp::sparse_hash_map, std::pair, CuddPointerPairHash> signatureCache; - - // The cache used to identify which old block numbers have already been reused. - spp::sparse_hash_map reuseBlocksCache; - }; - - TASK_DECL_5(BDD, refine_parallel, BDD, MTBDD, BDD, BDD, void*); - - template - class InternalSignatureRefinerBase; - - struct MutexWrapper { - MutexWrapper() : mutex() { - // Intentionally left empty. - } - - MutexWrapper(MutexWrapper const& other) { - // Intentionally left empty to create new mutex when copying. - } - - MutexWrapper& operator=(MutexWrapper const& other) { - // Intentionally left empty to create new mutex when copying. - return *this; - } - - std::mutex mutex; - }; - - template<> - class InternalSignatureRefinerBase { - public: - InternalSignatureRefinerBase(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd 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 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 const& manager; - storm::dd::InternalDdManager const& internalDdManager; - storm::expressions::Variable blockVariable; - std::set stateVariables; - - storm::dd::Bdd nondeterminismVariables; - storm::dd::Bdd nonBlockVariables; - - // The provided options. - InternalSignatureRefinerOptions options; - - uint64_t numberOfBlockVariables; - - storm::dd::Bdd 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, SylvanMTBDDPairHash> signatureCache; -// spp::sparse_hash_map, std::pair, SylvanMTBDDPairHash> signatureCacheParallel; - tbb::concurrent_unordered_map, std::pair>, SylvanMTBDDPairHash> signatureCacheParallel; - - // The cache used to identify which old block numbers have already been reused. - spp::sparse_hash_map reuseBlocksCache; - tbb::concurrent_unordered_map reuseBlocksCacheParallel; - - // A mutex that can be used to synchronize concurrent accesses to the members. - std::mutex mutex; - }; - - template - class InternalSignatureRefiner : public InternalSignatureRefinerBase { - public: - InternalSignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateVariables, storm::dd::Bdd const& nondeterminismVariables, storm::dd::Bdd const& nonBlockVariables, InternalSignatureRefinerOptions const& options) : InternalSignatureRefinerBase(manager, blockVariable, stateVariables, nondeterminismVariables, nonBlockVariables, options) { - - // Intentionally left empty. - } - - Partition refine(Partition const& oldPartition, Signature const& signature) { - std::pair, boost::optional>> newPartitionDds = refine(oldPartition, signature.getSignatureAdd()); - ++numberOfRefinements; - return oldPartition.replacePartition(newPartitionDds.first, nextFreeBlockIndex, nextFreeBlockIndex, newPartitionDds.second); - } - - void clearCaches() { - signatureCache.clear(); - signatureCacheParallel.clear(); - reuseBlocksCache.clear(); - reuseBlocksCacheParallel.clear(); - } - - std::pair, boost::optional>> refine(Partition const& oldPartition, storm::dd::Add const& signatureAdd) { - STORM_LOG_ASSERT(oldPartition.storedAsBdd(), "Expecting partition to be stored as BDD for Sylvan."); - - nextFreeBlockIndex = options.reuseBlockNumbers ? oldPartition.getNextFreeBlockIndex() : 0; - - // Perform the actual recursive refinement step. - std::pair 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 internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result.first)); - storm::dd::Bdd newPartitionBdd(oldPartition.asBdd().getDdManager(), internalNewPartitionBdd, oldPartition.asBdd().getContainedMetaVariables()); - - boost::optional> optionalChangedBdd; - if (options.createChangedStates && result.second != 0) { - storm::dd::InternalBdd internalChangedBdd(&internalDdManager, sylvan::Bdd(result.second)); - storm::dd::Bdd changedBdd(oldPartition.asBdd().getDdManager(), internalChangedBdd, stateVariables); - optionalChangedBdd = changedBdd; - } - - clearCaches(); - return std::make_pair(newPartitionBdd, optionalChangedBdd); - } - - std::pair reuseOrRelabel(BDD partitionNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { - LACE_ME; - - if (partitionNode == sylvan_false) { - if (options.createChangedStates) { - return std::make_pair(sylvan_false, sylvan_false); - } else { - return std::make_pair(sylvan_false, 0); - } - } - - // Check the cache whether we have seen the same node before. - auto nodePair = std::make_pair(0, partitionNode); - auto it = signatureCache.find(nodePair); - if (it != signatureCache.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)) { - if (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 = reuseBlocksCache[partitionNode]; - if (!reuseBlockEntry.isReused()) { - reuseBlockEntry.setReused(); - std::pair result; - if (options.createChangedStates) { - result = std::make_pair(partitionNode, sylvan_false); - } else { - result = std::make_pair(partitionNode, 0); - } - signatureCache[nodePair] = result; - return result; - } - } - - std::pair result; - if (options.createChangedStates) { - result = std::make_pair(encodeBlock(nextFreeBlockIndex++), sylvan_true); - } else { - result = std::make_pair(encodeBlock(nextFreeBlockIndex++), 0); - } - signatureCache[nodePair] = 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; - BDD partitionThen; - BDD partitionElse; - 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 (sylvan_mtbdd_matches_variable_index(partitionNode, sylvan_var(nonBlockVariablesNode), -offset)) { - partitionThen = sylvan_high(partitionNode); - partitionElse = sylvan_low(partitionNode); - skipped = false; - } else { - partitionThen = partitionElse = partitionNode; - } - - // 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 reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); - } - - std::pair combinedThenResult = reuseOrRelabel(partitionThen, 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 combinedElseResult = reuseOrRelabel(partitionElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); - BDD elseResult = combinedElseResult.first; - bdd_refs_push(elseResult); - BDD changedElseResult = combinedElseResult.second; - if (options.createChangedStates) { - bdd_refs_push(changedElseResult); - } - - std::pair result; - if (thenResult == elseResult) { - result.first = thenResult; - } else { - // Get the node to connect the subresults. - result.first = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); - } - - result.second = 0; - if (options.createChangedStates) { - if (changedThenResult == changedElseResult) { - result.second = changedThenResult; - } else { - // Get the node to connect the subresults. - result.second = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, changedElseResult, changedThenResult); - } - } - - // Dispose of the intermediate results. - if (options.createChangedStates) { - bdd_refs_pop(4); - } else { - bdd_refs_pop(2); - } - - // Store the result in the cache. - signatureCache[nodePair] = result; - return result; - } - } - - std::pair refineParallel(BDD partitionNode, MTBDD signatureNode, BDD nondeterminismVariablesNode, BDD nonBlockVariablesNode) { - LACE_ME; - return std::make_pair(CALL(refine_parallel, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, this), 0); - } - - std::pair 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 - // all states to be non-deadlock). - if (partitionNode == sylvan_false) { - if (options.createChangedStates) { - return std::make_pair(sylvan_false, sylvan_false); - } else { - return std::make_pair(sylvan_false, 0); - } - } else if (mtbdd_iszero(signatureNode)) { - std::pair result = reuseOrRelabel(partitionNode, nondeterminismVariablesNode, nonBlockVariablesNode); - signatureCache[std::make_pair(signatureNode, partitionNode)] = result; - return result; - } - - STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node."); - - // Check the cache whether we have seen the same node before. - auto nodePair = std::make_pair(signatureNode, partitionNode); - auto it = signatureCache.find(nodePair); - if (it != signatureCache.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)) { - if (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 = reuseBlocksCache[partitionNode]; - if (!reuseBlockEntry.isReused()) { - reuseBlockEntry.setReused(); - std::pair result; - if (options.createChangedStates) { - result = std::make_pair(partitionNode, sylvan_false); - } else { - result = std::make_pair(partitionNode, 0); - } - signatureCache[nodePair] = result; - return result; - } - } - - std::pair result; - if (options.createChangedStates) { - result = std::make_pair(encodeBlock(nextFreeBlockIndex++), sylvan_true); - } else { - result = std::make_pair(encodeBlock(nextFreeBlockIndex++), 0); - } - signatureCache[nodePair] = 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 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 = 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); - } - } - } - - // If there are no more non-block variables remaining, make a recursive call to enter the base case. - if (sylvan_isconst(nonBlockVariablesNode)) { - return refineSequential(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode); - } - - std::pair 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 combinedElseResult = refineSequential(partitionElse, signatureElse, isNondeterminismVariable ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode)); - BDD elseResult = combinedElseResult.first; - bdd_refs_push(elseResult); - BDD changedElseResult = combinedElseResult.second; - if (options.createChangedStates) { - bdd_refs_push(changedElseResult); - } - - std::pair result; - if (thenResult == elseResult) { - result.first = thenResult; - } else { - // Get the node to connect the subresults. - result.first = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult); - } - - result.second = 0; - if (options.createChangedStates) { - if (changedThenResult == changedElseResult) { - result.second = changedThenResult; - } else { - // Get the node to connect the subresults. - result.second = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, changedElseResult, changedThenResult); - } - } - - // Dispose of the intermediate results. - if (options.createChangedStates) { - bdd_refs_pop(4); - } else { - bdd_refs_pop(2); - } - - // Store the result in the cache. - signatureCache[nodePair] = result; - - return result; - } - } - - }; - - TASK_IMPL_5(BDD, refine_parallel, BDD, partitionNode, MTBDD, signatureNode, BDD, nondeterminismVariablesNode, BDD, nonBlockVariablesNode, void*, refinerPtr) - { - auto& refiner = *static_cast*>(refinerPtr); - std::unique_lock 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_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node."); - - // Check the cache whether we have seen the same node before. - BDD result; - if (cache_get(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), &result)) { - return result; - } - - if (sylvan_isconst(nonBlockVariablesNode)) { - auto nodePair = std::make_pair(signatureNode, partitionNode); - - lock.lock(); - auto& signatureCacheEntry = refiner.signatureCacheParallel[nodePair]; - - // If the mutex already exists, it means that some other thread has created it and this thread is - // supposed to yield the right answer. We can therefore wait for this lock and then return the result. - if (signatureCacheEntry.second) { - std::unique_lock blockLock(*signatureCacheEntry.second); - return signatureCacheEntry.first; - } else { - signatureCacheEntry.second = std::make_unique(); - } - std::unique_lock blockLock(*signatureCacheEntry.second); - lock.unlock(); - - 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.reuseBlocksCacheParallel[partitionNode]; - if (!reuseBlockEntry.isReused()) { - reuseBlockEntry.setReused(); - signatureCacheEntry.first = partitionNode; - return partitionNode; - } - } - - result = refiner.encodeBlock(refiner.nextFreeBlockIndex++); - signatureCacheEntry.first = result; - blockLock.unlock(); - - // Store the result in the cache. - cache_put(signatureNode|(256LL<<42), nonBlockVariablesNode, partitionNode|(refiner.numberOfRefinements<<40), result); - - return result; - } - - sylvan_gc_test(); - - // 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; - 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); - } - } - } - - // 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_parallel, partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode, refinerPtr); - } - - BDD nextNondeterminismVariables = isNondeterminismVariable ? sylvan_set_next(nondeterminismVariablesNode) : nondeterminismVariablesNode; - BDD nextNonBlockVariables = sylvan_set_next(nonBlockVariablesNode); - bdd_refs_spawn(SPAWN(refine_parallel, partitionElse, signatureElse, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); - - BDD thenResult = bdd_refs_push(CALL(refine_parallel, partitionThen, signatureThen, nextNondeterminismVariables, nextNonBlockVariables, refinerPtr)); - BDD elseResult = bdd_refs_sync(SYNC(refine_parallel)); - 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 SignatureRefiner::SignatureRefiner(storm::dd::DdManager const& manager, storm::expressions::Variable const& blockVariable, std::set const& stateRowVariables, std::set const& stateColumnVariables, bool shiftStateVariables, std::set const& nondeterminismVariables) : manager(&manager) {