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

more work on refiners that deal with nondeterminism variables

tempestpy_adaptions
dehnert 8 years ago
parent
d0840f783a
commit
472eaffabc
2 changed files with 153 additions and 136 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. 287
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp
  2. 2
      src/storm/storage/dd/bisimulation/SignatureRefiner.h

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

@ -10,6 +10,7 @@
#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"
@ -79,7 +80,7 @@ namespace storm {
template<typename ValueType>
class InternalSignatureRefiner<storm::dd::DdType::CUDD, ValueType> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) {
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::CUDD> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::CUDD> const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), nextFreeBlockIndex(0), numberOfRefinements(0), lastNumberOfVisitedNodes(10000), signatureCache(lastNumberOfVisitedNodes), reuseBlocksCache(lastNumberOfVisitedNodes) {
// Intentionally left empty.
}
@ -97,18 +98,22 @@ namespace storm {
signatureCache.clear();
reuseBlocksCache.clear();
nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
internalDdManager.debugCheck();
// Perform the actual recursive refinement step.
DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode());
DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
// Construct resulting ADD from the obtained node and the meta information.
storm::dd::InternalAdd<storm::dd::DdType::CUDD, ValueType> internalNewPartitionAdd(&internalDdManager, cudd::ADD(internalDdManager.getCuddManager(), result));
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> newPartitionAdd(oldPartition.asAdd().getDdManager(), internalNewPartitionAdd, oldPartition.asAdd().getContainedMetaVariables());
internalDdManager.debugCheck();
return newPartitionAdd;
}
DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode) {
DdNodePtr refine(DdNode* partitionNode, DdNode* signatureNode, DdNode* nondeterminismVariablesNode, DdNode* nonBlockVariablesNode) {
::DdManager* ddman = internalDdManager.getCuddManager().getManager();
// If we arrived at the constant zero node, then this was an illegal state encoding (we require
@ -118,45 +123,66 @@ namespace storm {
}
// Check the cache whether we have seen the same node before.
std::unique_ptr<DdNode*>& sigCacheEntrySmartPtr = signatureCache[std::make_pair(signatureNode, partitionNode)];
if (sigCacheEntrySmartPtr) {
auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = signatureCache.find(nodePair);
if (it != signatureCache.end()) {
// If so, we return the corresponding result.
return *sigCacheEntrySmartPtr;
return it->second;
}
DdNode** newEntryPtr = new DdNode*;
sigCacheEntrySmartPtr.reset(newEntryPtr);
// Determine the levels in the DDs.
uint64_t partitionVariable = Cudd_NodeReadIndex(partitionNode) - 1;
uint64_t signatureVariable = Cudd_NodeReadIndex(signatureNode);
uint64_t partitionLevel = Cudd_ReadPerm(ddman, partitionVariable);
uint64_t signatureLevel = Cudd_ReadPerm(ddman, signatureVariable);
uint64_t topLevel = std::min(partitionLevel, signatureLevel);
uint64_t topVariable = topLevel == partitionLevel ? partitionVariable : signatureVariable;
// Check whether the top variable is still within the state encoding.
if (topLevel <= lastStateLevel) {
// Determine subresults by recursive descent.
DdNodePtr thenResult;
DdNodePtr elseResult;
if (partitionLevel < signatureLevel) {
thenResult = refine(Cudd_T(partitionNode), signatureNode);
Cudd_Ref(thenResult);
elseResult = refine(Cudd_E(partitionNode), signatureNode);
Cudd_Ref(elseResult);
} else if (partitionLevel > signatureLevel) {
thenResult = refine(partitionNode, Cudd_T(signatureNode));
Cudd_Ref(thenResult);
elseResult = refine(partitionNode, Cudd_E(signatureNode));
Cudd_Ref(elseResult);
// If there are no more non-block variables, we hit the signature.
if (Cudd_IsConstant(nonBlockVariablesNode)) {
// 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();
signatureCache[nodePair] = partitionNode;
return partitionNode;
} else {
thenResult = refine(Cudd_T(partitionNode), Cudd_T(signatureNode));
Cudd_Ref(thenResult);
elseResult = refine(Cudd_E(partitionNode), Cudd_E(signatureNode));
Cudd_Ref(elseResult);
DdNode* result;
{
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex, false).template toAdd<ValueType>();
++nextFreeBlockIndex;
result = blockEncoding.getInternalAdd().getCuddDdNode();
Cudd_Ref(result);
}
signatureCache[nodePair] = result;
Cudd_Deref(result);
return result;
}
} else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
short offset = 1;
if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
offset = 0;
}
DdNode* partitionThen;
DdNode* partitionElse;
if (Cudd_NodeReadIndex(partitionNode) - offset == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
partitionThen = Cudd_T(partitionNode);
partitionElse = Cudd_E(partitionNode);
} else {
partitionThen = partitionElse = partitionNode;
}
DdNode* signatureThen;
DdNode* signatureElse;
if (Cudd_NodeReadIndex(signatureNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
signatureThen = Cudd_T(signatureNode);
signatureElse = Cudd_E(signatureNode);
} else {
signatureThen = signatureElse = signatureNode;
}
DdNode* thenResult = refine(partitionThen, signatureThen, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(thenResult);
DdNode* elseResult = refine(partitionElse, signatureElse, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
Cudd_Ref(elseResult);
DdNode* result;
if (thenResult == elseResult) {
Cudd_Deref(thenResult);
@ -164,7 +190,7 @@ namespace storm {
result = thenResult;
} else {
// Get the node to connect the subresults.
DdNode* var = Cudd_addIthVar(ddman, topVariable + 1);
DdNode* var = Cudd_addIthVar(ddman, Cudd_NodeReadIndex(nonBlockVariablesNode) + offset);
Cudd_Ref(var);
result = Cudd_addIte(ddman, var, thenResult, elseResult);
Cudd_Ref(result);
@ -174,33 +200,10 @@ namespace storm {
}
// Store the result in the cache.
*newEntryPtr = result;
signatureCache[nodePair] = result;
Cudd_Deref(result);
return result;
} else {
// If we are not within the state encoding any more, we hit the signature itself.
// 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();
*newEntryPtr = partitionNode;
return partitionNode;
} else {
DdNode* result;
{
storm::dd::Add<storm::dd::DdType::CUDD, ValueType> blockEncoding = manager.getEncoding(blockVariable, nextFreeBlockIndex, false).template toAdd<ValueType>();
++nextFreeBlockIndex;
result = blockEncoding.getInternalAdd().getCuddDdNode();
Cudd_Ref(result);
}
*newEntryPtr = result;
Cudd_Deref(result);
return result;
}
}
}
@ -208,8 +211,9 @@ namespace storm {
storm::dd::InternalDdManager<storm::dd::DdType::CUDD> const& internalDdManager;
storm::expressions::Variable const& blockVariable;
// The last level that belongs to the state encoding in the DDs.
uint64_t lastStateLevel;
// The cubes representing all non-block and all nondeterminism variables, respectively.
storm::dd::Bdd<storm::dd::DdType::CUDD> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::CUDD> nonBlockVariables;
// The current number of blocks of the new partition.
uint64_t nextFreeBlockIndex;
@ -221,7 +225,7 @@ namespace storm {
uint64_t lastNumberOfVisitedNodes;
// The cache used to identify states with identical signature.
spp::sparse_hash_map<std::pair<DdNode const*, DdNode const*>, std::unique_ptr<DdNode*>, CuddPointerPairHash> signatureCache;
spp::sparse_hash_map<std::pair<DdNode const*, DdNode const*>, DdNode*, CuddPointerPairHash> signatureCache;
// The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<DdNode const*, ReuseWrapper> reuseBlocksCache;
@ -230,7 +234,7 @@ namespace storm {
template<typename ValueType>
class InternalSignatureRefiner<storm::dd::DdType::Sylvan, ValueType> {
public:
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, uint64_t lastStateLevel) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), numberOfBlockVariables(manager.getMetaVariable(blockVariable).getNumberOfDdVariables()), blockCube(manager.getMetaVariable(blockVariable).getCube()), lastStateLevel(lastStateLevel), nextFreeBlockIndex(0), numberOfRefinements(0), signatureCache() {
InternalSignatureRefiner(storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager, storm::expressions::Variable const& blockVariable, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nondeterminismVariables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& nonBlockVariables) : manager(manager), internalDdManager(manager.getInternalDdManager()), blockVariable(blockVariable), nondeterminismVariables(nondeterminismVariables), nonBlockVariables(nonBlockVariables), 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();
@ -270,7 +274,7 @@ namespace storm {
// totalMakeNodeTime = std::chrono::high_resolution_clock::duration(0);
// Perform the actual recursive refinement step.
BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD());
BDD result = refine(oldPartition.asBdd().getInternalBdd().getSylvanBdd().GetBDD(), signatureAdd.getInternalAdd().getSylvanMtbdd().GetMTBDD(), nondeterminismVariables.getInternalBdd().getSylvanBdd().GetBDD(), nonBlockVariables.getInternalBdd().getSylvanBdd().GetBDD());
// Construct resulting BDD from the obtained node and the meta information.
storm::dd::InternalBdd<storm::dd::DdType::Sylvan> internalNewPartitionBdd(&internalDdManager, sylvan::Bdd(result));
@ -300,7 +304,7 @@ namespace storm {
return sylvan_cube(blockCube.getInternalBdd().getSylvanBdd().GetBDD(), e.data());
}
BDD refine(BDD partitionNode, MTBDD signatureNode) {
BDD refine(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
@ -331,93 +335,98 @@ namespace storm {
sigCacheEntrySmartPtr.reset(newEntryPtr);
sylvan_gc_test();
// Determine levels in the DDs.
// start = std::chrono::high_resolution_clock::now();
BDDVAR signatureVariable = sylvan_isconst(signatureNode) ? 0xffffffff : sylvan_var(signatureNode);
BDDVAR partitionVariable = sylvan_var(partitionNode) - 1;
BDDVAR topVariable = std::min(signatureVariable, partitionVariable);
// end = std::chrono::high_resolution_clock::now();
// totalLevelLookupTime += end - start;
// Check whether the top variable is still within the state encoding.
if (topVariable <= lastStateLevel) {
// Determine subresults by recursive descent.
BDD thenResult;
BDD elseResult;
if (partitionVariable < signatureVariable) {
elseResult = refine(sylvan_low(partitionNode), signatureNode);
thenResult = refine(sylvan_high(partitionNode), signatureNode);
} else if (partitionVariable > signatureVariable) {
elseResult = refine(partitionNode, sylvan_low(signatureNode));
thenResult = refine(partitionNode, sylvan_high(signatureNode));
} else {
elseResult = refine(sylvan_low(partitionNode), sylvan_low(signatureNode));
thenResult = refine(sylvan_high(partitionNode), sylvan_high(signatureNode));
}
BDD result;
if (thenResult == elseResult) {
result = thenResult;
} else {
// Get the node to connect the subresults.
// start = std::chrono::high_resolution_clock::now();
result = sylvan_makenode(topVariable + 1, elseResult, thenResult);
// end = std::chrono::high_resolution_clock::now();
// totalMakeNodeTime += end - start;
}
// Store the result in the cache.
// start = std::chrono::high_resolution_clock::now();
*newEntryPtr = result;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
return result;
} else {
// If we are not within the state encoding any more, we hit the signature itself.
// If there are no more non-block variables, we hit the signature.
if (sylvan_isconst(nonBlockVariablesNode)) {
// 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.
// start = std::chrono::high_resolution_clock::now();
// start = std::chrono::high_resolution_clock::now();
auto& reuseBlockEntry = reuseBlocksCache[partitionNode];
// end = std::chrono::high_resolution_clock::now();
// totalReuseBlocksLookupTime += end - start;
// end = std::chrono::high_resolution_clock::now();
// totalReuseBlocksLookupTime += end - start;
if (!reuseBlockEntry.isReused()) {
reuseBlockEntry.setReused();
reuseBlocksCache.emplace(partitionNode, true);
// start = std::chrono::high_resolution_clock::now();
// start = std::chrono::high_resolution_clock::now();
*newEntryPtr = partitionNode;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
return partitionNode;
} else {
// start = std::chrono::high_resolution_clock::now();
// start = std::chrono::high_resolution_clock::now();
BDD result = encodeBlock(nextFreeBlockIndex++);
// end = std::chrono::high_resolution_clock::now();
// totalBlockEncodingTime += end - start;
// end = std::chrono::high_resolution_clock::now();
// totalBlockEncodingTime += end - start;
// start = std::chrono::high_resolution_clock::now();
// start = std::chrono::high_resolution_clock::now();
*newEntryPtr = result;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
return result;
}
} else {
// If there are more variables that belong to the non-block part of the encoding, we need to recursively descend.
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
short offset = 1;
if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) {
offset = 0;
}
BDD partitionThen;
BDD partitionElse;
if (sylvan_var(partitionNode) - offset == sylvan_var(nonBlockVariablesNode)) {
partitionThen = sylvan_high(partitionNode);
partitionElse = sylvan_low(partitionNode);
} else {
partitionThen = partitionElse = partitionNode;
}
MTBDD signatureThen;
MTBDD signatureElse;
if (sylvan_var(signatureNode) == sylvan_var(nonBlockVariablesNode)) {
signatureThen = sylvan_high(signatureNode);
signatureElse = sylvan_low(signatureNode);
} else {
signatureThen = signatureElse = signatureNode;
}
BDD thenResult = refine(partitionThen, signatureThen, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD elseResult = refine(partitionElse, signatureElse, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
BDD result;
if (thenResult == elseResult) {
result = thenResult;
} else {
// Get the node to connect the subresults.
// start = std::chrono::high_resolution_clock::now();
result = sylvan_makenode(sylvan_var(nonBlockVariablesNode) + offset, elseResult, thenResult);
// end = std::chrono::high_resolution_clock::now();
// totalMakeNodeTime += end - start;
}
// Store the result in the cache.
// start = std::chrono::high_resolution_clock::now();
*newEntryPtr = result;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
return result;
}
}
storm::dd::DdManager<storm::dd::DdType::Sylvan> const& manager;
storm::dd::InternalDdManager<storm::dd::DdType::Sylvan> const& internalDdManager;
storm::expressions::Variable const& blockVariable;
storm::dd::Bdd<storm::dd::DdType::Sylvan> nondeterminismVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> nonBlockVariables;
uint64_t numberOfBlockVariables;
storm::dd::Bdd<storm::dd::DdType::Sylvan> blockCube;
// The last level that belongs to the state encoding in the DDs.
uint64_t lastStateLevel;
// The current number of blocks of the new partition.
uint64_t nextFreeBlockIndex;
@ -444,13 +453,21 @@ namespace storm {
};
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& stateVariables) : manager(&manager), stateVariables(stateVariables) {
uint64_t lastStateLevel = 0;
for (auto const& stateVariable : stateVariables) {
lastStateLevel = std::max(lastStateLevel, manager.getMetaVariable(stateVariable).getHighestLevel());
SignatureRefiner<DdType, ValueType>::SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, std::set<storm::expressions::Variable> const& nondeterminismVariables) : manager(&manager), stateVariables(stateVariables) {
storm::dd::Bdd<DdType> nonBlockVariablesCube = manager.getBddOne();
storm::dd::Bdd<DdType> nondeterminismVariablesCube = manager.getBddOne();
for (auto const& var : nondeterminismVariables) {
auto cube = manager.getMetaVariable(var).getCube();
nonBlockVariablesCube &= cube;
nondeterminismVariablesCube &= cube;
}
for (auto const& var : stateVariables) {
auto cube = manager.getMetaVariable(var).getCube();
nonBlockVariablesCube &= cube;
}
internalRefiner = std::make_unique<InternalSignatureRefiner<DdType, ValueType>>(manager, blockVariable, lastStateLevel);
internalRefiner = std::make_unique<InternalSignatureRefiner<DdType, ValueType>>(manager, blockVariable, nondeterminismVariablesCube, nonBlockVariablesCube);
}
template<storm::dd::DdType DdType, typename ValueType>

2
src/storm/storage/dd/bisimulation/SignatureRefiner.h
View File

@ -18,7 +18,7 @@ namespace storm {
class SignatureRefiner {
public:
SignatureRefiner() = default;
SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables);
SignatureRefiner(storm::dd::DdManager<DdType> const& manager, storm::expressions::Variable const& blockVariable, std::set<storm::expressions::Variable> const& stateVariables, std::set<storm::expressions::Variable> const& nondeterminismVariables = std::set<storm::expressions::Variable>());
~SignatureRefiner();

Write Preview
Loading…
Cancel
Save