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

Improved product of model and memory structure: We can now enforce that certain states are considered reachable.

tempestpy_adaptions
TimQu 7 years ago
parent
9bccae9c5c
commit
43642fef84
2 changed files with 56 additions and 36 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. 69
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  2. 23
      src/storm/storage/memorystructure/SparseModelMemoryProduct.h

69
src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
View File

@ -19,9 +19,21 @@ namespace storm {
template <typename ValueType>
SparseModelMemoryProduct<ValueType>::SparseModelMemoryProduct(storm::models::sparse::Model<ValueType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) {
// intentionally left empty
reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memory.getNumberOfStates(), false);
}
template <typename ValueType>
void SparseModelMemoryProduct<ValueType>::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) {
reachableStates.set(modelState * memory.getNumberOfStates() + memoryState, true);
}
template <typename ValueType>
void SparseModelMemoryProduct<ValueType>::setBuildFullProduct() {
reachableStates.clear();
reachableStates.complement();
}
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> SparseModelMemoryProduct<ValueType>::build() {
uint64_t modelStateCount = model.getNumberOfStates();
@ -38,7 +50,7 @@ namespace storm {
}
STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states.");
storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates);
computeReachableStates(memorySuccessors, initialStates);
// Compute the mapping to the states of the result
uint64_t reachableStateCount = 0;
@ -50,8 +62,8 @@ namespace storm {
// Build the model components
storm::storage::SparseMatrix<ValueType> transitionMatrix = model.getTransitionMatrix().hasTrivialRowGrouping() ?
buildDeterministicTransitionMatrix(reachableStates, memorySuccessors) :
buildNondeterministicTransitionMatrix(reachableStates, memorySuccessors);
buildDeterministicTransitionMatrix(memorySuccessors) :
buildNondeterministicTransitionMatrix(memorySuccessors);
storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix);
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors);
@ -88,37 +100,38 @@ namespace storm {
}
template <typename ValueType>
storm::storage::BitVector SparseModelMemoryProduct<ValueType>::computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const {
void SparseModelMemoryProduct<ValueType>::computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) {
uint64_t memoryStateCount = memory.getNumberOfStates();
// Explore the reachable states via DFS.
// A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm::storage::BitVector reachableStates = initialStates;
std::vector<uint64_t> stack(reachableStates.begin(), reachableStates.end());
while (!stack.empty()) {
uint64_t stateIndex = stack.back();
stack.pop_back();
uint64_t modelState = stateIndex / memoryStateCount;
uint64_t memoryState = stateIndex % memoryStateCount;
auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState);
for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) {
if (!storm::utility::isZero(modelTransitionIt->getValue())) {
uint64_t successorModelState = modelTransitionIt->getColumn();
uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin();
uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState];
uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState;
if (!reachableStates.get(successorStateIndex)) {
reachableStates.set(successorStateIndex, true);
stack.push_back(successorStateIndex);
reachableStates |= initialStates;
if (!reachableStates.full()) {
std::vector<uint64_t> stack(reachableStates.begin(), reachableStates.end());
while (!stack.empty()) {
uint64_t stateIndex = stack.back();
stack.pop_back();
uint64_t modelState = stateIndex / memoryStateCount;
uint64_t memoryState = stateIndex % memoryStateCount;
auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState);
for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) {
if (!storm::utility::isZero(modelTransitionIt->getValue())) {
uint64_t successorModelState = modelTransitionIt->getColumn();
uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin();
uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState];
uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState;
if (!reachableStates.get(successorStateIndex)) {
reachableStates.set(successorStateIndex, true);
stack.push_back(successorStateIndex);
}
}
}
}
}
return reachableStates;
}
template <typename ValueType>
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const {
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildDeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const {
uint64_t memoryStateCount = memory.getNumberOfStates();
uint64_t numResStates = reachableStates.getNumberOfSetBits();
uint64_t numResTransitions = 0;
@ -144,7 +157,7 @@ namespace storm {
}
template <typename ValueType>
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const {
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildNondeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const {
uint64_t memoryStateCount = memory.getNumberOfStates();
uint64_t numResStates = reachableStates.getNumberOfSetBits();
uint64_t numResChoices = 0;

23
src/storm/storage/memorystructure/SparseModelMemoryProduct.h
View File

@ -14,9 +14,7 @@ namespace storm {
/*!
* This class builds the product of the given sparse model and the given memory structure.
* This is similar to the well-known product of a model with a deterministic rabin automaton.
* Note: we already do one memory-structure-step for the initial state, i.e., if s is an initial state of
* the given model and s satisfies memoryStructure.getTransitionMatrix[0][n], then (s,n) will be the corresponding
* initial state of the resulting model.
* The product contains only the reachable states of the product
*
* The states of the resulting sparse model will have the original state labels plus the labels of this
* memory structure.
@ -28,11 +26,18 @@ namespace storm {
SparseModelMemoryProduct(storm::models::sparse::Model<ValueType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure);
// Enforces that the given model and memory state as well as the successor(s) are considered reachable -- even if they are not reachable from an initial state.
void addReachableState(uint64_t const& modelState, uint64_t const& memoryState);
// Enforces that every state is considered reachable. If this is set, the result has size #modelStates * #memoryStates
void setBuildFullProduct();
// Invokes the building of the product
std::shared_ptr<storm::models::sparse::Model<ValueType>> build();
// Retrieves the state of the resulting model that represents the given memory and model state.
// An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable).
// Should only be called AFTER calling build();
// An invalid index is returned, if the specifyied state does not exist (i.e., if it is not part of product).
uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState) const;
private:
@ -42,13 +47,13 @@ namespace storm {
std::vector<uint64_t> computeMemorySuccessors() const;
// Computes the reachable states of the resulting model
storm::storage::BitVector computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const;
void computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates);
// Methods that build the model components
// Matrix for deterministic models
storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const;
storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const;
// Matrix for nondeterministic models
storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const;
storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const;
// State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES
storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const;
// Reward models
@ -61,7 +66,9 @@ namespace storm {
// Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState)
std::vector<uint64_t> toResultStateMapping;
// Indicates which states are considered reachable. (s, m) is reachable if this BitVector is true at (s * memoryStateCount) + m
storm::storage::BitVector reachableStates;
storm::models::sparse::Model<ValueType> const& model;
storm::storage::MemoryStructure const& memory;

Write Preview
Loading…
Cancel
Save