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

The model memory product can now retrieve the reachable states without actually building the product

main
TimQu 8 years ago
parent
11a4f8d016
commit
999fd0752c
4 changed files with 132 additions and 102 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  2. 19
      src/storm/models/sparse/NondeterministicModel.cpp
  3. 166
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  4. 45
      src/storm/storage/memorystructure/SparseModelMemoryProduct.h

4
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
View File

@ -484,8 +484,8 @@ namespace storm {
productToMemoryStateMap.resize(numProductStates, std::numeric_limits<uint64_t>::max());
for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) {
for (uint64_t memoryState = 0; memoryState < numMemoryStates; ++memoryState) {
uint64_t productState = productBuilder.getResultState(modelState, memoryState);
if (productState < numProductStates) {
if (productBuilder.isStateReachable(modelState, memoryState)) {
uint64_t productState = productBuilder.getResultState(modelState, memoryState);
modelMemoryToProductStateMap[modelState * numMemoryStates + memoryState] = productState;
productToModelStateMap[productState] = modelState;
productToMemoryStateMap[productState] = memoryState;

19
src/storm/models/sparse/NondeterministicModel.cpp
View File

@ -51,22 +51,11 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> NondeterministicModel<ValueType, RewardModelType>::applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) {
if (scheduler.isMemorylessScheduler()) {
auto memStruct = storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(*this);
auto memoryProduct = memStruct.product(*this);
if (!dropUnreachableStates) {
memoryProduct.setBuildFullProduct();
}
return memoryProduct.build(scheduler);
} else {
boost::optional<storm::storage::MemoryStructure> const& memStruct = scheduler.getMemoryStructure();
STORM_LOG_ASSERT(memStruct, "Memoryless scheduler without memory structure.");
auto memoryProduct = memStruct->product(*this);
if (!dropUnreachableStates) {
memoryProduct.setBuildFullProduct();
}
return memoryProduct.build(scheduler);
storm::storage::SparseModelMemoryProduct<ValueType, RewardModelType> memoryProduct(*this, scheduler);
if (!dropUnreachableStates) {
memoryProduct.setBuildFullProduct();
}
return memoryProduct.build();
}
template<typename ValueType, typename RewardModelType>

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

@ -9,6 +9,7 @@
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/utility/constants.h"
#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
#include "storm/utility/macros.h"
#include "storm/utility/builder.h"
@ -18,91 +19,113 @@ namespace storm {
namespace storage {
template <typename ValueType, typename RewardModelType>
SparseModelMemoryProduct<ValueType, RewardModelType>::SparseModelMemoryProduct(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : memoryStateCount(memoryStructure.getNumberOfStates()), model(sparseModel), memory(memoryStructure) {
SparseModelMemoryProduct<ValueType, RewardModelType>::SparseModelMemoryProduct(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : isInitialized(false), memoryStateCount(memoryStructure.getNumberOfStates()), model(sparseModel), memory(memoryStructure), scheduler(boost::none) {
reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memoryStateCount, false);
}
template <typename ValueType, typename RewardModelType>
SparseModelMemoryProduct<ValueType, RewardModelType>::SparseModelMemoryProduct(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel, storm::storage::Scheduler<ValueType> const& scheduler) : isInitialized(false), memoryStateCount(scheduler.getNumberOfMemoryStates()), model(sparseModel), localMemory(scheduler.getMemoryStructure() ? boost::optional<MemoryStructure>() : boost::optional<MemoryStructure>(storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(model))), memory(scheduler.getMemoryStructure() ? scheduler.getMemoryStructure().get() : localMemory.get()), scheduler(scheduler) {
reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memoryStateCount, false);
}
template <typename ValueType, typename RewardModelType>
void SparseModelMemoryProduct<ValueType, RewardModelType>::initialize() {
if (!isInitialized) {
uint64_t modelStateCount = model.getNumberOfStates();
computeMemorySuccessors();
// Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false);
auto memoryInitIt = memory.getInitialMemoryStates().begin();
for (auto const& modelInit : model.getInitialStates()) {
initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true);
++memoryInitIt;
}
STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states.");
computeReachableStates(initialStates);
// Compute the mapping to the states of the result
uint64_t reachableStateCount = 0;
toResultStateMapping = std::vector<uint64_t> (model.getNumberOfStates() * memoryStateCount, std::numeric_limits<uint64_t>::max());
for (auto const& reachableState : reachableStates) {
toResultStateMapping[reachableState] = reachableStateCount;
++reachableStateCount;
}
isInitialized = true;
}
}
template <typename ValueType, typename RewardModelType>
void SparseModelMemoryProduct<ValueType, RewardModelType>::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) {
isInitialized = false;
reachableStates.set(modelState * memoryStateCount + memoryState, true);
}
template <typename ValueType, typename RewardModelType>
void SparseModelMemoryProduct<ValueType, RewardModelType>::setBuildFullProduct() {
isInitialized = false;
reachableStates.fill();
}
template <typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> SparseModelMemoryProduct<ValueType, RewardModelType>::build(boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) {
uint64_t modelStateCount = model.getNumberOfStates();
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> SparseModelMemoryProduct<ValueType, RewardModelType>::build() {
std::vector<uint64_t> memorySuccessors = computeMemorySuccessors();
initialize();
// Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false);
auto memoryInitIt = memory.getInitialMemoryStates().begin();
for (auto const& modelInit : model.getInitialStates()) {
initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true);
++memoryInitIt;
}
STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states.");
computeReachableStates(memorySuccessors, initialStates, scheduler);
// Compute the mapping to the states of the result
uint64_t reachableStateCount = 0;
toResultStateMapping = std::vector<uint64_t> (model.getNumberOfStates() * memoryStateCount, std::numeric_limits<uint64_t>::max());
for (auto const& reachableState : reachableStates) {
toResultStateMapping[reachableState] = reachableStateCount;
++reachableStateCount;
}
// Build the model components
storm::storage::SparseMatrix<ValueType> transitionMatrix;
if (scheduler) {
transitionMatrix = buildTransitionMatrixForScheduler(memorySuccessors, scheduler.get());
transitionMatrix = buildTransitionMatrixForScheduler();
} else if (model.getTransitionMatrix().hasTrivialRowGrouping()) {
transitionMatrix = buildDeterministicTransitionMatrix(memorySuccessors);
transitionMatrix = buildDeterministicTransitionMatrix();
} else {
transitionMatrix = buildNondeterministicTransitionMatrix(memorySuccessors);
transitionMatrix = buildNondeterministicTransitionMatrix();
}
storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix);
std::unordered_map<std::string, RewardModelType> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler);
std::unordered_map<std::string, RewardModelType> rewardModels = buildRewardModels(transitionMatrix);
// Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states.
labeling.addLabel("init", initialStates % reachableStates);
return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels), scheduler);
return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels));
}
template <typename ValueType, typename RewardModelType>
uint64_t const& SparseModelMemoryProduct<ValueType, RewardModelType>::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const {
return toResultStateMapping[modelState * memoryStateCount + memoryState];
bool SparseModelMemoryProduct<ValueType, RewardModelType>::isStateReachable(uint64_t const& modelState, uint64_t const& memoryState) {
STORM_LOG_ASSERT(modelState < getOriginalModel().getNumberOfStates(), "Invalid model state: " << modelState << ".");
STORM_LOG_ASSERT(memoryState < memoryStateCount, "Invalid memory state: " << memoryState << ".");
initialize();
return reachableStates.get(modelState * memoryStateCount + memoryState);
}
template <typename ValueType, typename RewardModelType>
uint64_t const& SparseModelMemoryProduct<ValueType, RewardModelType>::getResultState(uint64_t const& modelState, uint64_t const& memoryState) {
initialize();
STORM_LOG_ASSERT(isStateReachable(modelState, memoryState), "Tried to get unreachable product state (" << modelState << "," << memoryState << ")");
return toResultStateMapping[modelState * memoryStateCount + memoryState];
}
template <typename ValueType, typename RewardModelType>
std::vector<uint64_t> SparseModelMemoryProduct<ValueType, RewardModelType>::computeMemorySuccessors() const {
void SparseModelMemoryProduct<ValueType, RewardModelType>::computeMemorySuccessors() {
uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount();
std::vector<uint64_t> result(modelTransitionCount * memoryStateCount, std::numeric_limits<uint64_t>::max());
memorySuccessors = std::vector<uint64_t>(modelTransitionCount * memoryStateCount, std::numeric_limits<uint64_t>::max());
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
for (uint64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) {
auto const& memoryTransition = memory.getTransitionMatrix()[memoryState][transitionGoal];
if (memoryTransition) {
for (auto const& modelTransitionIndex : memoryTransition.get()) {
result[modelTransitionIndex * memoryStateCount + memoryState] = transitionGoal;
memorySuccessors[modelTransitionIndex * memoryStateCount + memoryState] = transitionGoal;
}
}
}
}
return result;
}
template <typename ValueType, typename RewardModelType>
void SparseModelMemoryProduct<ValueType, RewardModelType>::computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) {
void SparseModelMemoryProduct<ValueType, RewardModelType>::computeReachableStates(storm::storage::BitVector const& initialStates) {
// Explore the reachable states via DFS.
// A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
reachableStates |= initialStates;
@ -153,7 +176,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildDeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const {
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildDeterministicTransitionMatrix() {
uint64_t numResStates = reachableStates.getNumberOfSetBits();
uint64_t numResTransitions = 0;
for (auto const& stateIndex : reachableStates) {
@ -168,7 +191,7 @@ namespace storm {
auto const& modelRow = model.getTransitionMatrix().getRow(modelState);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
++currentRow;
@ -178,7 +201,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildNondeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const {
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildNondeterministicTransitionMatrix() {
uint64_t numResStates = reachableStates.getNumberOfSetBits();
uint64_t numResChoices = 0;
uint64_t numResTransitions = 0;
@ -200,7 +223,7 @@ namespace storm {
auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
++currentRow;
@ -211,7 +234,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildTransitionMatrixForScheduler(std::vector<uint64_t> const& memorySuccessors, storm::storage::Scheduler<ValueType> const& scheduler) const {
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildTransitionMatrixForScheduler() {
uint64_t numResStates = reachableStates.getNumberOfSetBits();
uint64_t numResChoices = 0;
uint64_t numResTransitions = 0;
@ -219,7 +242,7 @@ namespace storm {
for (auto const& stateIndex : reachableStates) {
uint64_t modelState = stateIndex / memoryStateCount;
uint64_t memoryState = stateIndex % memoryStateCount;
storm::storage::SchedulerChoice<ValueType> choice = scheduler.getChoice(modelState, memoryState);
storm::storage::SchedulerChoice<ValueType> choice = scheduler->getChoice(modelState, memoryState);
if (choice.isDefined()) {
++numResChoices;
if (choice.isDeterministic()) {
@ -256,14 +279,14 @@ namespace storm {
if (!hasTrivialNondeterminism) {
builder.newRowGroup(currentRow);
}
storm::storage::SchedulerChoice<ValueType> choice = scheduler.getChoice(modelState, memoryState);
storm::storage::SchedulerChoice<ValueType> choice = scheduler->getChoice(modelState, memoryState);
if (choice.isDefined()) {
if (choice.isDeterministic()) {
uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choice.getDeterministicChoice();
auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
} else {
@ -274,7 +297,7 @@ namespace storm {
auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
ValueType transitionValue = choiceIndex.second * entryIt->getValue();
auto insertionRes = transitions.insert(std::make_pair(getResultState(entryIt->getColumn(), successorMemoryState), transitionValue));
if (!insertionRes.second) {
@ -293,7 +316,7 @@ namespace storm {
auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
++currentRow;
@ -305,7 +328,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
storm::models::sparse::StateLabeling SparseModelMemoryProduct<ValueType, RewardModelType>::buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const {
storm::models::sparse::StateLabeling SparseModelMemoryProduct<ValueType, RewardModelType>::buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) {
uint64_t modelStateCount = model.getNumberOfStates();
uint64_t numResStates = resultTransitionMatrix.getRowGroupCount();
@ -316,10 +339,8 @@ namespace storm {
storm::storage::BitVector resLabeledStates(numResStates, false);
for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) {
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
resLabeledStates.set(resState, true);
if (isStateReachable(modelState, memoryState)) {
resLabeledStates.set(getResultState(modelState, memoryState), true);
}
}
}
@ -331,20 +352,27 @@ namespace storm {
storm::storage::BitVector resLabeledStates(numResStates, false);
for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) {
for (uint64_t modelState = 0; modelState < modelStateCount; ++modelState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
resLabeledStates.set(resState, true);
if (isStateReachable(modelState, memoryState)) {
resLabeledStates.set(getResultState(modelState, memoryState), true);
}
}
}
resultLabeling.addLabel(memoryLabel, std::move(resLabeledStates));
}
storm::storage::BitVector initialStates(numResStates, false);
auto memoryInitIt = memory.getInitialMemoryStates().begin();
for (auto const& modelInit : model.getInitialStates()) {
initialStates.set(getResultState(modelInit, *memoryInitIt), true);
++memoryInitIt;
}
resultLabeling.addLabel("init", std::move(initialStates));
return resultLabeling;
}
template <typename ValueType, typename RewardModelType>
std::unordered_map<std::string, RewardModelType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const {
std::unordered_map<std::string, RewardModelType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) {
typedef typename RewardModelType::ValueType RewardValueType;
@ -359,10 +387,8 @@ namespace storm {
for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) {
if (!storm::utility::isZero(modelStateReward)) {
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
stateRewards.get()[resState] = modelStateReward;
if (isStateReachable(modelState, memoryState)) {
stateRewards.get()[getResultState(modelState, memoryState)] = modelStateReward;
}
}
}
@ -381,14 +407,12 @@ namespace storm {
}
uint64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState];
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
if (isStateReachable(modelState, memoryState)) {
if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) {
ValueType factor = scheduler->getChoice(modelState, memoryState).getChoiceAsDistribution().getProbability(rowOffset);
stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState]] = factor * modelStateActionReward;
stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[getResultState(modelState, memoryState)]] = factor * modelStateActionReward;
} else {
stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward;
stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[getResultState(modelState, memoryState)] + rowOffset] = modelStateActionReward;
}
}
}
@ -416,7 +440,7 @@ namespace storm {
++transitionEntryIt;
}
uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
auto insertionRes = rewards.insert(std::make_pair(getResultState(rewardEntry.getColumn(), successorMemoryState), rewardEntry.getValue()));
if (!insertionRes.second) {
insertionRes.first->second += rewardEntry.getValue();
@ -438,7 +462,7 @@ namespace storm {
++transitionEntryIt;
}
uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(resRowIndex, getResultState(rewardEntry.getColumn(), successorMemoryState), rewardEntry.getValue());
}
}
@ -454,7 +478,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> SparseModelMemoryProduct<ValueType, RewardModelType>::buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const {
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> SparseModelMemoryProduct<ValueType, RewardModelType>::buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, RewardModelType>&& rewardModels) {
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> components (std::move(matrix), std::move(labeling), std::move(rewardModels));
if (model.isOfType(storm::models::ModelType::Ctmc)) {

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

@ -25,48 +25,63 @@ namespace storm {
class SparseModelMemoryProduct {
public:
// Constructs the product w.r.t. the given model and the given memory structure
SparseModelMemoryProduct(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure);
// Constructs the product w.r.t. the given model and the given (finite memory) scheduler.
SparseModelMemoryProduct(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel, storm::storage::Scheduler<ValueType> const& scheduler);
// 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 under the specified scheduler (if given).
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build(boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler = boost::none);
// Returns true iff the given model and memory state is reachable in the product
bool isStateReachable(uint64_t const& modelState, uint64_t const& memoryState);
// Retrieves the state of the resulting model that represents the given memory and model state.
// 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;
// This method should only be called if the given state is reachable.
uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState);
// Invokes the building of the product under the specified scheduler (if given).
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
storm::models::sparse::Model<ValueType, RewardModelType> const& getOriginalModel() const;
storm::storage::MemoryStructure const& getMemory() const;
private:
// Initializes auxiliary data for building the product
void initialize();
// Computes for each pair of memory state and model transition index the successor memory state
// The resulting vector maps (modelTransition * memoryStateCount) + memoryState to the corresponding successor state of the memory structure
std::vector<uint64_t> computeMemorySuccessors() const;
void computeMemorySuccessors();
// Computes the reachable states of the resulting model
void computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler);
void computeReachableStates(storm::storage::BitVector const& initialStates);
// Methods that build the model components
// Matrix for deterministic models
storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const;
storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix();
// Matrix for nondeterministic models
storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const;
storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix();
// Matrix for models that consider a scheduler
storm::storage::SparseMatrix<ValueType> buildTransitionMatrixForScheduler(std::vector<uint64_t> const& memorySuccessors, storm::storage::Scheduler<ValueType> const& scheduler) 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;
storm::storage::SparseMatrix<ValueType> buildTransitionMatrixForScheduler();
// State labeling.
storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix);
// Reward models
std::unordered_map<std::string, RewardModelType> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const;
std::unordered_map<std::string, RewardModelType> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix);
// Builds the resulting model
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const;
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, RewardModelType>&& rewardModels);
// Stores whether this builder has already been initialized.
bool isInitialized;
// stores the successor memory states for each transition in the product
std::vector<uint64_t> memorySuccessors;
// Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState)
std::vector<uint64_t> toResultStateMapping;
@ -77,7 +92,9 @@ namespace storm {
uint64_t const memoryStateCount;
storm::models::sparse::Model<ValueType, RewardModelType> const& model;
boost::optional<storm::storage::MemoryStructure> localMemory;
storm::storage::MemoryStructure const& memory;
boost::optional<storm::storage::Scheduler<ValueType> const&> scheduler;
};
}

Write Preview
Loading…
Cancel
Save