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

added nondeterministic memory structure

main
TimQu 7 years ago
parent
51a5a82a5f
commit
5163803243
8 changed files with 487 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. 103
      src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.cpp
  2. 33
      src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h
  3. 76
      src/storm/storage/memorystructure/NondeterministicMemoryStructure.cpp
  4. 25
      src/storm/storage/memorystructure/NondeterministicMemoryStructure.h
  5. 115
      src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.cpp
  6. 47
      src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h
  7. 187
      src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp
  8. 37
      src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h

103
src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.cpp
View File

@ -1,103 +0,0 @@
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
#include "storm/logic/Formulas.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
namespace preprocessing {
template <class SparseModelType>
storm::storage::MemoryStructure getGoalMemory(SparseModelType const& model, storm::logic::Formula const& propositionalGoalStateFormula) {
STORM_LOG_THROW(propositionalGoalStateFormula.isInFragment(storm::logic::propositional()), storm::exceptions::NotSupportedException, "The subformula " << propositionalGoalStateFormula << " should be propositional.");
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(model);
storm::storage::BitVector goalStates = mc.check(propositionalGoalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
// Check if the formula is already satisfied for all initial states. In such a case the trivial memory structure suffices.
if (model.getInitialStates().isSubsetOf(goalStates)) {
STORM_LOG_INFO("One objective is already satisfied for all initial states.");
return storm::storage::MemoryStructureBuilder<typename SparseModelType::ValueType, typename SparseModelType::RewardModelType>::buildTrivialMemoryStructure(model);
}
// Create a memory structure that stores whether a goal state has already been reached
storm::storage::MemoryStructureBuilder<typename SparseModelType::ValueType, typename SparseModelType::RewardModelType> builder(2, model);
builder.setTransition(0, 0, ~goalStates);
builder.setTransition(0, 1, goalStates);
builder.setTransition(1, 1, storm::storage::BitVector(model.getNumberOfStates(), true));
for (auto const& initState : model.getInitialStates()) {
builder.setInitialMemoryState(initState, goalStates.get(initState) ? 1 : 0);
}
return builder.build();
}
template <class SparseModelType>
storm::storage::MemoryStructure getUntilFormulaMemory(SparseModelType const& model, storm::logic::Formula const& leftSubFormula, storm::logic::Formula const& rightSubFormula) {
auto notLeftOrRight = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or,
std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, leftSubFormula.asSharedPointer()),
rightSubFormula.asSharedPointer());
return getGoalMemory<SparseModelType>(model, *notLeftOrRight);
}
template <class SparseModelType>
std::shared_ptr<SparseModelType> SparseMultiObjectiveMemoryIncorporation<SparseModelType>::incorporateGoalMemory(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) {
storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(model);
for (auto const& subFormula : formula.getSubformulas()) {
STORM_LOG_THROW(subFormula->isOperatorFormula(), storm::exceptions::NotSupportedException, "The given Formula " << *subFormula << " is not supported.");
auto const& subsubFormula = subFormula->asOperatorFormula().getSubformula();
if (subsubFormula.isEventuallyFormula()) {
memory = memory.product(getGoalMemory(model, subsubFormula.asEventuallyFormula().getSubformula()));
} else if (subsubFormula.isUntilFormula()) {
memory = memory.product(getUntilFormulaMemory(model, subsubFormula.asUntilFormula().getLeftSubformula(), subsubFormula.asUntilFormula().getRightSubformula()));
} else if (subsubFormula.isBoundedUntilFormula()) {
// For bounded formulas it is only reasonable to add the goal memory if it considers a single upper step/time bound.
auto const& buf = subsubFormula.asBoundedUntilFormula();
if (!buf.isMultiDimensional() && !buf.getTimeBoundReference().isRewardBound() && (!buf.hasLowerBound() || (!buf.isLowerBoundStrict() && storm::utility::isZero(buf.template getLowerBound<storm::RationalNumber>())))) {
memory = memory.product(getUntilFormulaMemory(model, buf.getLeftSubformula(), buf.getRightSubformula()));
}
} else if (subsubFormula.isGloballyFormula()) {
auto notPhi = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, subsubFormula.asGloballyFormula().getSubformula().asSharedPointer());
memory = memory.product(getGoalMemory(model, *notPhi));
} else {
STORM_LOG_THROW(subFormula->isOperatorFormula(), storm::exceptions::NotSupportedException, "The given Formula " << subsubFormula << " is not supported.");
}
}
storm::storage::SparseModelMemoryProduct<ValueType> product = memory.product(model);
return std::dynamic_pointer_cast<SparseModelType>(product.build());
}
template <class SparseModelType>
std::shared_ptr<SparseModelType> SparseMultiObjectiveMemoryIncorporation<SparseModelType>::incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "not implemented");
return nullptr;
}
template class SparseMultiObjectiveMemoryIncorporation<storm::models::sparse::Mdp<double>>;
template class SparseMultiObjectiveMemoryIncorporation<storm::models::sparse::MarkovAutomaton<double>>;
template class SparseMultiObjectiveMemoryIncorporation<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class SparseMultiObjectiveMemoryIncorporation<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
}
}
}
}

33
src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h
View File

@ -1,33 +0,0 @@
#pragma once
#include <memory>
#include "storm/storage/memorystructure/MemoryStructure.h"
#include "storm/logic/MultiObjectiveFormula.h"
#include "storm/logic/Formula.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
namespace preprocessing {
template <class SparseModelType>
class SparseMultiObjectiveMemoryIncorporation {
typedef typename SparseModelType::ValueType ValueType;
typedef typename SparseModelType::RewardModelType RewardModelType;
public:
static std::shared_ptr<SparseModelType> incorporateGoalMemory(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula);
static std::shared_ptr<SparseModelType> incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates);
};
}
}
}
}

76
src/storm/storage/memorystructure/NondeterministicMemoryStructure.cpp
View File

@ -0,0 +1,76 @@
#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h"
#include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace storage {
NondeterministicMemoryStructure::NondeterministicMemoryStructure(std::vector<storm::storage::BitVector> const& transitions, uint64_t initialState) : transitions(transitions), initialState(initialState) {
STORM_LOG_THROW(this->initialState < this->transitions.size(), storm::exceptions::InvalidArgumentException, "Initial state " << this->initialState << " of nondeterministic memory structure is invalid.");
for (auto const& t : this->transitions) {
STORM_LOG_THROW(t.size() == this->transitions.size(), storm::exceptions::InvalidArgumentException, "Invalid dimension of transition matrix of nondeterministic memory structure.");
STORM_LOG_THROW(!t.empty(), storm::exceptions::InvalidArgumentException, "Invalid transition matrix of nondeterministic memory structure: No deadlock states allowed.");
}
}
uint64_t NondeterministicMemoryStructure::getNumberOfStates() const {
return transitions.size();
}
uint64_t NondeterministicMemoryStructure::getInitialState() const {
return initialState;
}
storm::storage::BitVector const& NondeterministicMemoryStructure::getTransitions(uint64_t state) const {
return transitions.at(state);
}
uint64_t NondeterministicMemoryStructure::getNumberOfOutgoingTransitions(uint64_t state) const {
return getTransitions(state).getNumberOfSetBits();
}
std::vector<storm::storage::BitVector> const& NondeterministicMemoryStructure::getTransitions() const {
return transitions;
}
std::string NondeterministicMemoryStructure::toString() const {
std::string result = "NondeterministicMemoryStructure with " + std::to_string(getNumberOfStates()) + " states.\n";
result += "Initial state is " + std::to_string(getInitialState()) + ". Transitions are \n";
// header
result += " |";
for (uint64_t state = 0; state < getNumberOfStates(); ++state) {
if (state < 10) {
result += " ";
}
result += std::to_string(state);
}
result += "\n";
result += "--|";
for (uint64_t state = 0; state < getNumberOfStates(); ++state) {
result += "--";
}
result += "\n";
// transition matrix entries
for (uint64_t state = 0; state < getNumberOfStates(); ++state) {
if (state < 10) {
result += " ";
}
result += std::to_string(state) + "|";
for (uint64_t statePrime = 0; statePrime < getNumberOfStates(); ++statePrime) {
result += " ";
if (getTransitions(state).get(statePrime)) {
result += "1";
} else {
result += "0";
}
}
result += "\n";
}
return result;
}
}
}

25
src/storm/storage/memorystructure/NondeterministicMemoryStructure.h
View File

@ -0,0 +1,25 @@
#pragma once
#include <vector>
#include "storm/storage/BitVector.h"
namespace storm {
namespace storage {
class NondeterministicMemoryStructure {
public:
NondeterministicMemoryStructure(std::vector<storm::storage::BitVector> const& transitions, uint64_t initialState);
uint64_t getNumberOfStates() const;
uint64_t getInitialState() const;
storm::storage::BitVector const& getTransitions(uint64_t state) const;
uint64_t getNumberOfOutgoingTransitions(uint64_t state) const;
std::vector<storm::storage::BitVector> const& getTransitions() const;
std::string toString() const;
private:
std::vector<storm::storage::BitVector> transitions;
uint64_t initialState;
};
}
}

115
src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.cpp
View File

@ -0,0 +1,115 @@
#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h"
#include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace storage {
std::string toString(NondeterministicMemoryStructurePattern const& pattern) {
switch (pattern) {
case NondeterministicMemoryStructurePattern::Trivial:
return "trivial";
case NondeterministicMemoryStructurePattern::FixedCounter:
return "fixedcounter";
case NondeterministicMemoryStructurePattern::SelectiveCounter:
return "selectivecounter";
case NondeterministicMemoryStructurePattern::FixedRing:
return "fixedring";
case NondeterministicMemoryStructurePattern::SelectiveRing:
return "ring";
case NondeterministicMemoryStructurePattern::SettableBits:
return "settablebits";
case NondeterministicMemoryStructurePattern::Full:
return "full";
}
return "unknown";
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::build(NondeterministicMemoryStructurePattern pattern, uint64_t numStates) const {
switch (pattern) {
case NondeterministicMemoryStructurePattern::Trivial:
STORM_LOG_ERROR_COND(numStates == 1, "Invoked building trivial nondeterministic memory structure with " << numStates << " states. However, trivial nondeterministic memory structure always has one state.");
return buildTrivialMemory();
case NondeterministicMemoryStructurePattern::FixedCounter:
return buildFixedCountingMemory(numStates);
case NondeterministicMemoryStructurePattern::SelectiveCounter:
return buildSelectiveCountingMemory(numStates);
case NondeterministicMemoryStructurePattern::FixedRing:
return buildFixedRingMemory(numStates);
case NondeterministicMemoryStructurePattern::SelectiveRing:
return buildSelectiveRingMemory(numStates);
case NondeterministicMemoryStructurePattern::SettableBits:
return buildSettableBitsMemory(numStates);
case NondeterministicMemoryStructurePattern::Full:
return buildFullyConnectedMemory(numStates);
}
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildTrivialMemory() const {
return buildFullyConnectedMemory(1);
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFixedCountingMemory(uint64_t numStates) const {
std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
for (uint64_t state = 0; state < numStates; ++state) {
transitions[state].set(std::min(state + 1, numStates - 1));
}
return NondeterministicMemoryStructure(transitions, 0);
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSelectiveCountingMemory(uint64_t numStates) const {
std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
for (uint64_t state = 0; state < numStates; ++state) {
transitions[state].set(state);
transitions[state].set(std::min(state + 1, numStates - 1));
}
return NondeterministicMemoryStructure(transitions, 0);
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFixedRingMemory(uint64_t numStates) const {
std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
for (uint64_t state = 0; state < numStates; ++state) {
transitions[state].set((state + 1) % numStates);
}
return NondeterministicMemoryStructure(transitions, 0);
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSelectiveRingMemory(uint64_t numStates) const {
std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, false));
for (uint64_t state = 0; state < numStates; ++state) {
transitions[state].set(state);
transitions[state].set((state + 1) % numStates);
}
return NondeterministicMemoryStructure(transitions, 0);
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSettableBitsMemory(uint64_t numStates) const {
// compute the number of bits, i.e., floor(log(numStates))
uint64_t numBits = 0;
uint64_t actualNumStates = 1;
while (actualNumStates * 2 <= numStates) {
actualNumStates *= 2;
++numBits;
}
STORM_LOG_WARN_COND(actualNumStates == numStates, "The number of memory states for the settable bits pattern has to be a power of 2. Shrinking the number of memory states to " << actualNumStates << ".");
std::vector<storm::storage::BitVector> transitions(actualNumStates, storm::storage::BitVector(actualNumStates, false));
for (uint64_t state = 0; state < actualNumStates; ++state) {
transitions[state].set(state);
for (uint64_t bit = 0; bit < numBits; ++bit) {
uint64_t bitMask = 1u << bit;
transitions[state].set(state | bitMask);
}
}
return NondeterministicMemoryStructure(transitions, 0);
}
NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFullyConnectedMemory(uint64_t numStates) const {
std::vector<storm::storage::BitVector> transitions(numStates, storm::storage::BitVector(numStates, true));
return NondeterministicMemoryStructure(transitions, 0);
}
}
}

47
src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h
View File

@ -0,0 +1,47 @@
#pragma once
#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h"
namespace storm {
namespace storage {
enum class NondeterministicMemoryStructurePattern {
Trivial, FixedCounter, SelectiveCounter, FixedRing, SelectiveRing, SettableBits, Full
};
std::string toString(NondeterministicMemoryStructurePattern const& pattern);
class NondeterministicMemoryStructureBuilder {
public:
// Builds a memory structure with the given pattern and the given number of states.
NondeterministicMemoryStructure build(NondeterministicMemoryStructurePattern pattern, uint64_t numStates) const;
// Builds a memory structure that consists of just a single memory state
NondeterministicMemoryStructure buildTrivialMemory() const;
// Builds a memory structure that consists of a chain of the given number of states.
// Every state has exactly one transition to the next state. The last state has just a selfloop.
NondeterministicMemoryStructure buildFixedCountingMemory(uint64_t numStates) const;
// Builds a memory structure that consists of a chain of the given number of states.
// Every state has a selfloop and a transition to the next state. The last state just has a selfloop.
NondeterministicMemoryStructure buildSelectiveCountingMemory(uint64_t numStates) const;
// Builds a memory structure that consists of a ring of the given number of states.
// Every state has a transition to the successor state
NondeterministicMemoryStructure buildFixedRingMemory(uint64_t numStates) const;
// Builds a memory structure that consists of a ring of the given number of states.
// Every state has a transition to the successor state and a selfloop
NondeterministicMemoryStructure buildSelectiveRingMemory(uint64_t numStates) const;
// Builds a memory structure that represents floor(log(numStates)) bits that can only be set from zero to one or from zero to zero.
NondeterministicMemoryStructure buildSettableBitsMemory(uint64_t numStates) const;
// Builds a memory structure that consists of the given number of states which are fully connected.
NondeterministicMemoryStructure buildFullyConnectedMemory(uint64_t numStates) const;
};
}
}

187
src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp
View File

@ -0,0 +1,187 @@
#include "storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h"
#include <limits>
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/utility/graph.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace storage {
template<typename SparseModelType>
SparseModelNondeterministicMemoryProduct<SparseModelType>::SparseModelNondeterministicMemoryProduct(SparseModelType const& model, storm::storage::NondeterministicMemoryStructure const& memory) : model(model), memory(memory) {
// intentionally left empty
}
template<typename SparseModelType>
std::shared_ptr<SparseModelType> SparseModelNondeterministicMemoryProduct<SparseModelType>::build() const {
// For simplicity we first build the 'full' product of model and memory (with model.numStates * memory.numStates states).
storm::storage::sparse::ModelComponents<ValueType> components;
components.transitionMatrix = buildTransitions();
components.stateLabeling = buildStateLabeling();
// Now delete unreachable states.
storm::storage::BitVector allStates(components.transitionMatrix.getRowGroupCount(), true);
auto reachableStates = storm::utility::graph::getReachableStates(components.transitionMatrix, components.stateLabeling.getStates("init"), allStates, ~allStates);
components.transitionMatrix = components.transitionMatrix.getSubmatrix(true, reachableStates, reachableStates);
components.stateLabeling = components.stateLabeling.getSubLabeling(reachableStates);
// build the remaining components
for (auto const& rewModel : model.getRewardModels()) {
components.rewardModels.emplace(rewModel.first, buildRewardModel(rewModel.second, reachableStates));
}
if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
STORM_LOG_ASSERT((std::is_same<SparseModelType, storm::models::sparse::MarkovAutomaton<ValueType>>::value), "Model has unexpected type.");
auto ma = model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
components.exitRates = buildExitRateVector(*ma, reachableStates);
components.markovianStates = buildMarkovianStateLabeling(*ma, reachableStates);
}
return std::make_shared<SparseModelType>(std::move(components));
}
template<typename SparseModelType>
storm::storage::SparseMatrix<typename SparseModelNondeterministicMemoryProduct<SparseModelType>::ValueType> SparseModelNondeterministicMemoryProduct<SparseModelType>::buildTransitions() const {
storm::storage::SparseMatrix<ValueType> const& origTransitions = model.getTransitionMatrix();
uint64_t numRows = 0;
uint64_t numEntries = 0;
for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) {
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
numRows += origTransitions.getRowGroupSize(modelState) * memory.getNumberOfOutgoingTransitions(memState);
numEntries += origTransitions.getRowGroup(modelState).getNumberOfEntries() * memory.getNumberOfOutgoingTransitions(memState);
}
}
storm::storage::SparseMatrixBuilder<ValueType> builder(numRows,
model.getNumberOfStates() * memory.getNumberOfStates(),
numEntries,
true,
true,
model.getNumberOfStates() * memory.getNumberOfStates());
uint64_t row = 0;
for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) {
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
builder.newRowGroup(row);
for (uint64_t origRow = origTransitions.getRowGroupIndices()[modelState]; origRow < origTransitions.getRowGroupIndices()[modelState + 1]; ++origRow) {
for (auto const& memStatePrime : memory.getTransitions(memState)) {
for (auto const& entry : origTransitions.getRow(origRow)) {
builder.addNextValue(row, getProductState(entry.getColumn(), memStatePrime), entry.getValue());
}
++row;
}
}
}
}
return builder.build();
}
template<typename SparseModelType>
storm::models::sparse::StateLabeling SparseModelNondeterministicMemoryProduct<SparseModelType>::buildStateLabeling() const {
storm::models::sparse::StateLabeling labeling(model.getNumberOfStates() * memory.getNumberOfStates());
for (auto const& labelName : model.getStateLabeling().getLabels()) {
storm::storage::BitVector newStates(model.getNumberOfStates() * memory.getNumberOfStates(), false);
// The init label is only assigned to Product states with the initial memory state
if (labelName == "init") {
for (auto const& modelState : model.getStateLabeling().getStates(labelName)) {
newStates.set(getProductState(modelState, memory.getInitialState()));
}
} else {
for (auto const& modelState : model.getStateLabeling().getStates(labelName)) {
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
newStates.set(getProductState(modelState, memState));
}
}
}
labeling.addLabel(labelName, std::move(newStates));
}
return labeling;
}
template<typename SparseModelType>
storm::models::sparse::StandardRewardModel<typename SparseModelNondeterministicMemoryProduct<SparseModelType>::ValueType> SparseModelNondeterministicMemoryProduct<SparseModelType>::buildRewardModel(storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel, storm::storage::BitVector const& reachableStates) const {
boost::optional<std::vector<ValueType>> stateRewards, actionRewards;
if (rewardModel.hasStateRewards()) {
stateRewards = std::vector<ValueType>();
stateRewards->reserve(model.getNumberOfStates() * memory.getNumberOfStates());
for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) {
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
if (reachableStates.get(getProductState(modelState, memState))) {
stateRewards->push_back(rewardModel.getStateReward(modelState));
}
}
}
}
if (rewardModel.hasStateActionRewards()) {
actionRewards = std::vector<ValueType>();
for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) {
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
if (reachableStates.get(getProductState(modelState, memState))) {
for (uint64_t origRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; origRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++origRow) {
ValueType const& actionReward = rewardModel.getStateActionReward(origRow);
actionRewards->insert(actionRewards->end(), memory.getNumberOfOutgoingTransitions(memState), actionReward);
}
}
}
}
}
STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported.");
return storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards), std::move(actionRewards));
}
template<typename SparseModelType>
std::vector<typename SparseModelNondeterministicMemoryProduct<SparseModelType>::ValueType> SparseModelNondeterministicMemoryProduct<SparseModelType>::buildExitRateVector(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const {
std::vector<ValueType> res;
res.reserve(model.getNumberOfStates() * memory.getNumberOfStates());
for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) {
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
if (reachableStates.get(getProductState(modelState, memState))) {
res.push_back(modelAsMA.getExitRate(modelState));
}
}
}
return res;
}
template<typename SparseModelType>
storm::storage::BitVector SparseModelNondeterministicMemoryProduct<SparseModelType>::buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const {
storm::storage::BitVector res(reachableStates.getNumberOfSetBits(), false);
uint64_t currReachableState = 0;
for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) {
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
if (reachableStates.get(getProductState(modelState, memState))) {
if (modelAsMA.isMarkovianState(modelState)) {
res.set(currReachableState, true);
}
++currReachableState;
}
}
}
assert(currReachableState == reachableStates.getNumberOfSetBits());
return res;
}
template<typename SparseModelType>
uint64_t SparseModelNondeterministicMemoryProduct<SparseModelType>::getProductState(uint64_t modelState, uint64_t memoryState) const {
return modelState * memory.getNumberOfStates() + memoryState;
}
template<typename SparseModelType>
uint64_t SparseModelNondeterministicMemoryProduct<SparseModelType>::getModelState(uint64_t productState) const {
return productState / memory.getNumberOfStates();
}
template<typename SparseModelType>
uint64_t SparseModelNondeterministicMemoryProduct<SparseModelType>::getMemoryState(uint64_t productState) const {
return productState % memory.getNumberOfStates();
}
template class SparseModelNondeterministicMemoryProduct<storm::models::sparse::Mdp<double>>;
template class SparseModelNondeterministicMemoryProduct<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class SparseModelNondeterministicMemoryProduct<storm::models::sparse::MarkovAutomaton<double>>;
template class SparseModelNondeterministicMemoryProduct<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
}
}

37
src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h
View File

@ -0,0 +1,37 @@
#pragma once
#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h"
#include "storm/models/sparse/MarkovAutomaton.h"
namespace storm {
namespace storage {
template<typename SparseModelType>
class SparseModelNondeterministicMemoryProduct {
public:
typedef typename SparseModelType::ValueType ValueType;
SparseModelNondeterministicMemoryProduct(SparseModelType const& model, storm::storage::NondeterministicMemoryStructure const& memory);
std::shared_ptr<SparseModelType> build() const;
private:
storm::storage::SparseMatrix<ValueType> buildTransitions() const;
storm::models::sparse::StateLabeling buildStateLabeling() const;
storm::models::sparse::StandardRewardModel<ValueType> buildRewardModel(storm::models::sparse::StandardRewardModel<ValueType> const& rewardModel, storm::storage::BitVector const& reachableStates) const;
// Markov automaton specific components
std::vector<ValueType> buildExitRateVector(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const;
storm::storage::BitVector buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton<ValueType> const& modelAsMA, storm::storage::BitVector const& reachableStates) const;
uint64_t getProductState(uint64_t modelState, uint64_t memoryState) const;
uint64_t getModelState(uint64_t productState) const;
uint64_t getMemoryState(uint64_t productState) const;
SparseModelType const& model;
storm::storage::NondeterministicMemoryStructure const& memory;
};
}
}
Write Preview
Loading…
Cancel
Save