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

more work on MDP bisimulation

tempestpy_adaptions
dehnert 8 years ago
parent
472eaffabc
commit
2b0911d627
7 changed files with 112 additions and 105 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. 13
      src/storm/models/symbolic/Model.cpp
  2. 15
      src/storm/models/symbolic/Model.h
  3. 14
      src/storm/models/symbolic/NondeterministicModel.cpp
  4. 5
      src/storm/models/symbolic/NondeterministicModel.h
  5. 6
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  6. 2
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  7. 162
      src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

13
src/storm/models/symbolic/Model.cpp
View File

@ -174,12 +174,21 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
std::set<storm::expressions::Variable> Model<Type, ValueType>::getRowAndNondeterminismVariables() const {
return rowVariables;
std::set<storm::expressions::Variable> result;
std::set_union(this->getRowVariables().begin(), this->getRowVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
return result;
}
template<storm::dd::DdType Type, typename ValueType>
std::set<storm::expressions::Variable> Model<Type, ValueType>::getColumnAndNondeterminismVariables() const {
return columnVariables;
std::set<storm::expressions::Variable> result;
std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
return result;
}
template<storm::dd::DdType Type, typename ValueType>
std::set<storm::expressions::Variable> const& Model<Type, ValueType>::getNondeterminismVariables() const {
return emptyVariableSet;
}
template<storm::dd::DdType Type, typename ValueType>

15
src/storm/models/symbolic/Model.h
View File

@ -226,14 +226,21 @@ namespace storm {
*
* @return All meta variables used to encode rows and nondetermism.
*/
virtual std::set<storm::expressions::Variable> getRowAndNondeterminismVariables() const;
std::set<storm::expressions::Variable> getRowAndNondeterminismVariables() const;
/*!
* Retrieves all meta variables used to encode columns and nondetermism.
*
* @return All meta variables used to encode columns and nondetermism.
*/
virtual std::set<storm::expressions::Variable> getColumnAndNondeterminismVariables() const;
std::set<storm::expressions::Variable> getColumnAndNondeterminismVariables() const;
/*!
* Retrieves all meta variables used to encode the nondeterminism.
*
* @return All meta variables used to encode the nondeterminism.
*/
virtual std::set<storm::expressions::Variable> const& getNondeterminismVariables() const;
/*!
* Retrieves the pairs of row and column meta variables.
@ -311,7 +318,6 @@ namespace storm {
std::set<storm::RationalFunctionVariable> const& getParameters() const;
protected:
/*!
* Sets the transition matrix of the model.
*
@ -389,6 +395,9 @@ namespace storm {
// The parameters. Only meaningful for models over rational functions.
std::set<storm::RationalFunctionVariable> parameters;
// An empty variable set that can be used when references to non-existing sets need to be returned.
std::set<storm::expressions::Variable> emptyVariableSet;
};
} // namespace symbolic

14
src/storm/models/symbolic/NondeterministicModel.cpp
View File

@ -62,20 +62,6 @@ namespace storm {
return nondeterminismVariables;
}
template<storm::dd::DdType Type, typename ValueType>
std::set<storm::expressions::Variable> NondeterministicModel<Type, ValueType>::getRowAndNondeterminismVariables() const {
std::set<storm::expressions::Variable> result;
std::set_union(this->getRowVariables().begin(), this->getRowVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
return result;
}
template<storm::dd::DdType Type, typename ValueType>
std::set<storm::expressions::Variable> NondeterministicModel<Type, ValueType>::getColumnAndNondeterminismVariables() const {
std::set<storm::expressions::Variable> result;
std::set_union(this->getColumnVariables().begin(), this->getColumnVariables().end(), this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), std::inserter(result, result.begin()));
return result;
}
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> const& NondeterministicModel<Type, ValueType>::getIllegalMask() const {
return illegalMask;

5
src/storm/models/symbolic/NondeterministicModel.h
View File

@ -97,10 +97,7 @@ namespace storm {
*
* @return The meta variables used to encode the nondeterminism in the model.
*/
std::set<storm::expressions::Variable> const& getNondeterminismVariables() const;
virtual std::set<storm::expressions::Variable> getRowAndNondeterminismVariables() const override;
virtual std::set<storm::expressions::Variable> getColumnAndNondeterminismVariables() const override;
virtual std::set<storm::expressions::Variable> const& getNondeterminismVariables() const override;
/*!
* Retrieves a BDD characterizing all illegal nondeterminism encodings in the model.

6
src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
View File

@ -5,7 +5,7 @@ namespace storm {
namespace bisimulation {
template <storm::dd::DdType DdType, typename ValueType>
PartitionRefiner<DdType, ValueType>::PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables()) {
PartitionRefiner<DdType, ValueType>::PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getNondeterminismVariables()) {
// Intentionally left empty.
}
@ -44,7 +44,7 @@ namespace storm {
totalSignatureTime += (signatureEnd - signatureStart);
STORM_LOG_DEBUG("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
signature.getSignatureAdd().exportToDot("sig" + std::to_string(refinements) + ".dot");
// signature.getSignatureAdd().exportToDot("sig" + std::to_string(refinements) + ".dot");
// if (refinements == 1) {
// exit(-1);
// }
@ -54,7 +54,7 @@ namespace storm {
auto refinementEnd = std::chrono::high_resolution_clock::now();
totalRefinementTime += (refinementEnd - refinementStart);
newPartition.asAdd().exportToDot("newpart" + std::to_string(refinements) + ".dot");
// newPartition.asAdd().exportToDot("newpart" + std::to_string(refinements) + ".dot");
signatureTime += std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();

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

@ -592,7 +592,7 @@ namespace storm {
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {}));
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot exctract quotient for this model type.");
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
}
}

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

@ -99,8 +99,6 @@ namespace storm {
reuseBlocksCache.clear();
nextFreeBlockIndex = oldPartition.getNextFreeBlockIndex();
internalDdManager.debugCheck();
// Perform the actual recursive refinement step.
DdNodePtr result = refine(oldPartition.asAdd().getInternalAdd().getCuddDdNode(), signatureAdd.getInternalAdd().getCuddDdNode(), nondeterminismVariables.getInternalBdd().getCuddDdNode(), nonBlockVariables.getInternalBdd().getCuddDdNode());
@ -108,8 +106,6 @@ namespace storm {
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;
}
@ -154,28 +150,48 @@ namespace storm {
} 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;
}
bool skippedBoth = true;
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;
short offset = 1;
while (skippedBoth && !Cudd_IsConstant(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = 1;
if (!Cudd_IsConstant(nondeterminismVariablesNode) && Cudd_NodeReadIndex(nondeterminismVariablesNode) == Cudd_NodeReadIndex(nonBlockVariablesNode)) {
offset = 0;
}
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 (offset == 0) {
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);
}
DdNode* thenResult = refine(partitionThen, signatureThen, offset == 0 ? Cudd_T(nondeterminismVariablesNode) : nondeterminismVariablesNode, Cudd_T(nonBlockVariablesNode));
@ -315,24 +331,13 @@ namespace storm {
STORM_LOG_ASSERT(partitionNode != mtbdd_false, "Expected non-false node.");
// ++numberOfVisitedNodes;
// Check the cache whether we have seen the same node before.
// ++signatureCacheLookups;
// auto start = std::chrono::high_resolution_clock::now();
std::unique_ptr<MTBDD>& sigCacheEntrySmartPtr = signatureCache[std::make_pair(signatureNode, partitionNode)];
if (sigCacheEntrySmartPtr) {
// ++signatureCacheHits;
auto nodePair = std::make_pair(signatureNode, partitionNode);
auto it = signatureCache.find(nodePair);
if (it != signatureCache.end()) {
// If so, we return the corresponding result.
// auto end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheLookupTime += end - start;
return *sigCacheEntrySmartPtr;
return it->second;
}
// auto end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheLookupTime += end - start;
MTBDD* newEntryPtr = new MTBDD;
sigCacheEntrySmartPtr.reset(newEntryPtr);
sylvan_gc_test();
@ -341,55 +346,62 @@ namespace storm {
// 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();
auto& reuseBlockEntry = reuseBlocksCache[partitionNode];
// 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();
*newEntryPtr = partitionNode;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
signatureCache[nodePair] = partitionNode;
return partitionNode;
} else {
// start = std::chrono::high_resolution_clock::now();
BDD result = encodeBlock(nextFreeBlockIndex++);
// end = std::chrono::high_resolution_clock::now();
// totalBlockEncodingTime += end - start;
// start = std::chrono::high_resolution_clock::now();
*newEntryPtr = result;
// end = std::chrono::high_resolution_clock::now();
// totalSignatureCacheStoreTime += end - start;
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.
// 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;
}
bool skippedBoth = true;
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;
short offset = 1;
while (skippedBoth && !sylvan_isconst(nonBlockVariablesNode)) {
// Remember an offset that indicates whether the top variable is a nondeterminism variable or not.
offset = 1;
if (!sylvan_isconst(nondeterminismVariablesNode) && sylvan_var(nondeterminismVariablesNode) == sylvan_var(nonBlockVariablesNode)) {
offset = 0;
}
if (sylvan_var(partitionNode) - offset == sylvan_var(nonBlockVariablesNode)) {
partitionThen = sylvan_high(partitionNode);
partitionElse = sylvan_low(partitionNode);
skippedBoth = false;
} else {
partitionThen = partitionElse = partitionNode;
}
if (sylvan_var(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 (offset == 0) {
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 refine(partitionNode, signatureNode, nondeterminismVariablesNode, nonBlockVariablesNode);
}
BDD thenResult = refine(partitionThen, signatureThen, offset == 0 ? sylvan_high(nondeterminismVariablesNode) : nondeterminismVariablesNode, sylvan_high(nonBlockVariablesNode));
@ -400,17 +412,11 @@ namespace storm {
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;
signatureCache[nodePair] = result;
return result;
}
@ -434,7 +440,7 @@ namespace storm {
uint64_t numberOfRefinements;
// The cache used to identify states with identical signature.
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, std::unique_ptr<MTBDD>, SylvanMTBDDPairHash> signatureCache;
spp::sparse_hash_map<std::pair<MTBDD, MTBDD>, MTBDD, SylvanMTBDDPairHash> signatureCache;
// The cache used to identify which old block numbers have already been reused.
spp::sparse_hash_map<MTBDD, ReuseWrapper> reuseBlocksCache;

Write Preview
Loading…
Cancel
Save