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

Improved memory structure so that a memory update is triggered based on the transition that was taken (and not only the state that was reached)

tempestpy_adaptions
TimQu 8 years ago
parent
ada12204e1
commit
16041bc936
7 changed files with 185 additions and 73 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. 41
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
  2. 31
      src/storm/storage/memorystructure/MemoryStructure.cpp
  3. 8
      src/storm/storage/memorystructure/MemoryStructure.h
  4. 75
      src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
  5. 40
      src/storm/storage/memorystructure/MemoryStructureBuilder.h
  6. 59
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  7. 4
      src/storm/storage/memorystructure/SparseModelMemoryProduct.h

41
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
View File

@ -69,8 +69,8 @@ namespace storm {
template <typename SparseModelType>
SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) {
storm::storage::MemoryStructureBuilder memoryBuilder(1);
memoryBuilder.setTransition(0,0, storm::logic::Formula::getTrueFormula());
storm::storage::MemoryStructureBuilder<ValueType, RewardModelType> memoryBuilder(1, model);
memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true));
memory = std::make_shared<storm::storage::MemoryStructure>(memoryBuilder.build());
// The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names
@ -232,24 +232,28 @@ namespace storm {
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data) {
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.originalModel);
storm::storage::BitVector rightSubformulaResult = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector leftSubformulaResult = mc.check(formula.getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
// Check if the formula is already satisfied in the initial state because then the transformation to expected rewards will fail.
if (!data.objectives.back()->lowerTimeBound) {
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.originalModel);
if (!(data.originalModel.getInitialStates() & mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()).empty()) {
if (!(data.originalModel.getInitialStates() & rightSubformulaResult).empty()) {
// TODO: Handle this case more properly
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The Probability for the objective " << *data.objectives.back()->originalFormula << " is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented.");
}
}
// Create a memory structure that stores whether a non-PhiState or a PsiState has already been reached
storm::storage::MemoryStructureBuilder builder(2);
storm::storage::MemoryStructureBuilder<ValueType, RewardModelType> builder(2, data.originalModel);
std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant";
builder.setLabel(0, relevantStatesLabel);
auto negatedLeftSubFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getLeftSubformula().asSharedPointer());
auto targetFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer());
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, targetFormula));
builder.setTransition(0, 1, targetFormula);
builder.setTransition(1, 1, storm::logic::Formula::getTrueFormula());
storm::storage::BitVector nonRelevantStates = ~leftSubformulaResult | rightSubformulaResult;
builder.setTransition(0, 0, ~nonRelevantStates);
builder.setTransition(0, 1, nonRelevantStates);
builder.setTransition(1, 1, storm::storage::BitVector(data.originalModel.getNumberOfStates(), true));
for (auto const& initState : data.originalModel.getInitialStates()) {
builder.setInitialMemoryState(initState, nonRelevantStates.get(initState) ? 1 : 0);
}
storm::storage::MemoryStructure objectiveMemory = builder.build();
data.memory = std::make_shared<storm::storage::MemoryStructure>(data.memory->product(objectiveMemory));
@ -295,15 +299,22 @@ namespace storm {
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data);
return;
}
// Analyze the subformula
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.originalModel);
storm::storage::BitVector subFormulaResult = mc.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
// Create a memory structure that stores whether a target state has already been reached
storm::storage::MemoryStructureBuilder builder(2);
storm::storage::MemoryStructureBuilder<ValueType, RewardModelType> builder(2, data.originalModel);
// Get a unique label that is not already present in the model
std::string relevantStatesLabel = data.memoryLabelPrefix + "_obj" + std::to_string(data.objectives.size()) + "_relevant";
builder.setLabel(0, relevantStatesLabel);
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()));
builder.setTransition(0, 1, formula.getSubformula().asSharedPointer());
builder.setTransition(1, 1, std::make_shared<storm::logic::BooleanLiteralFormula>(true));
builder.setTransition(0, 0, ~subFormulaResult);
builder.setTransition(0, 1, subFormulaResult);
builder.setTransition(1, 1, storm::storage::BitVector(data.originalModel.getNumberOfStates(), true));
for (auto const& initState : data.originalModel.getInitialStates()) {
builder.setInitialMemoryState(initState, subFormulaResult.get(initState) ? 1 : 0);
}
storm::storage::MemoryStructure objectiveMemory = builder.build();
data.memory = std::make_shared<storm::storage::MemoryStructure>(data.memory->product(objectiveMemory));

31
src/storm/storage/memorystructure/MemoryStructure.cpp
View File

@ -11,11 +11,11 @@
namespace storm {
namespace storage {
MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling) {
MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates) {
// intentionally left empty
}
MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)) {
MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)) {
// intentionally left empty
}
@ -27,6 +27,10 @@ namespace storm {
return stateLabeling;
}
std::vector<uint_fast64_t> const& MemoryStructure::getInitialMemoryStates() const {
return initialMemoryStates;
}
uint_fast64_t MemoryStructure::getNumberOfStates() const {
return transitions.size();
}
@ -37,7 +41,7 @@ namespace storm {
uint_fast64_t resNumStates = lhsNumStates * rhsNumStates;
// Transition matrix
TransitionMatrix resultTransitions(resNumStates, std::vector<std::shared_ptr<storm::logic::Formula const>>(resNumStates));
TransitionMatrix resultTransitions(resNumStates, std::vector<boost::optional<storm::storage::BitVector>>(resNumStates));
uint_fast64_t resState = 0;
for (uint_fast64_t lhsState = 0; lhsState < lhsNumStates; ++lhsState) {
for (uint_fast64_t rhsState = 0; rhsState < rhsNumStates; ++rhsState) {
@ -50,7 +54,11 @@ namespace storm {
auto& rhsTransition = rhs.getTransitionMatrix()[rhsState][rhsTransitionTarget];
if (rhsTransition) {
uint_fast64_t resTransitionTarget = (lhsTransitionTarget * rhsNumStates) + rhsTransitionTarget;
resStateTransitions[resTransitionTarget] = std::make_shared<storm::logic::BinaryBooleanStateFormula const>(storm::logic::BinaryBooleanStateFormula::OperatorType::And, lhsTransition,rhsTransition);
resStateTransitions[resTransitionTarget] = rhsTransition.get() & lhsTransition.get();
// If it is not possible to take the considered transition w.r.t. the considered model, we can delete it.
if (resStateTransitions[resTransitionTarget]->empty()) {
resStateTransitions[resTransitionTarget] = boost::none;
}
}
}
}
@ -84,11 +92,18 @@ namespace storm {
}
resultLabeling.addLabel(rhsLabel, std::move(resLabeledStates));
}
//return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling));
MemoryStructure res(std::move(resultTransitions), std::move(resultLabeling));
return res;
// Initial States
std::vector<uint_fast64_t> resultInitialMemoryStates;
STORM_LOG_THROW(this->getInitialMemoryStates().size() == rhs.getInitialMemoryStates().size(), storm::exceptions::InvalidOperationException, "Tried to build the product of two memory structures that consider a different number of initial model states.");
resultInitialMemoryStates.reserve(this->getInitialMemoryStates().size());
auto lhsStateIt = this->getInitialMemoryStates().begin();
auto rhsStateIt = rhs.getInitialMemoryStates().begin();
for (; lhsStateIt != this->getInitialMemoryStates().end(); ++lhsStateIt, ++rhsStateIt) {
resultInitialMemoryStates.push_back(*lhsStateIt * rhsNumStates + *rhsStateIt);
}
return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling), std::move(resultInitialMemoryStates));
}
template <typename ValueType>
@ -129,8 +144,6 @@ namespace storm {
template SparseModelMemoryProduct<double> MemoryStructure::product(storm::models::sparse::Model<double> const& sparseModel) const;
template SparseModelMemoryProduct<storm::RationalNumber> MemoryStructure::product(storm::models::sparse::Model<storm::RationalNumber> const& sparseModel) const;
}
}

8
src/storm/storage/memorystructure/MemoryStructure.h
View File

@ -20,7 +20,7 @@ namespace storm {
class MemoryStructure {
public:
typedef std::vector<std::vector<std::shared_ptr<storm::logic::Formula const>>> TransitionMatrix;
typedef std::vector<std::vector<boost::optional<storm::storage::BitVector>>> TransitionMatrix;
/*!
* Creates a memory structure with the given transition matrix and the given memory state labeling.
@ -34,11 +34,12 @@ namespace storm {
* @param transitionMatrix The transition matrix
* @param memoryStateLabeling A labeling of the memory states to specify, e.g., accepting states
*/
MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling);
MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling);
MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates);
MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates);
TransitionMatrix const& getTransitionMatrix() const;
storm::models::sparse::StateLabeling const& getStateLabeling() const;
std::vector<uint_fast64_t> const& getInitialMemoryStates() const;
uint_fast64_t getNumberOfStates() const;
/*!
@ -60,6 +61,7 @@ namespace storm {
private:
TransitionMatrix transitions;
storm::models::sparse::StateLabeling stateLabeling;
std::vector<uint_fast64_t> initialMemoryStates;
};
}

75
src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
View File

@ -1,6 +1,7 @@
#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/models/sparse/Model.h"
#include "storm/storage/BitVector.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidOperationException.h"
@ -8,29 +9,83 @@
namespace storm {
namespace storage {
MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t const& numberOfStates) : transitions(numberOfStates, std::vector<std::shared_ptr<storm::logic::Formula const>>(numberOfStates)), stateLabeling(numberOfStates) {
template <typename ValueType, typename RewardModelType>
MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0) {
// Intentionally left empty
}
template <typename ValueType, typename RewardModelType>
void MemoryStructureBuilder<ValueType, RewardModelType>::setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState) {
STORM_LOG_THROW(model.getInitialStates().get(initialModelState), storm::exceptions::InvalidOperationException, "Invalid index of initial model state: " << initialMemoryState << ". This is not an initial state of the model.");
STORM_LOG_THROW(initialMemoryState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of initial memory state: " << initialMemoryState << ". There are only " << transitions.size() << " states in this memory structure.");
auto initMemStateIt = initialMemoryStates.begin();
for (auto const& initState : model.getInitialStates()) {
if (initState == initialModelState) {
*initMemStateIt = initialMemoryState;
break;
}
++initMemStateIt;
}
assert(initMemStateIt != initialMemoryStates.end());
}
template <typename ValueType, typename RewardModelType>
void MemoryStructureBuilder<ValueType, RewardModelType>::setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, storm::storage::BitVector const& modelStates, boost::optional<storm::storage::BitVector> const& modelChoices) {
auto const& modelTransitions = model.getTransitionMatrix();
void MemoryStructureBuilder::setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr<storm::logic::Formula const> formula) {
STORM_LOG_THROW(startState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of start state: " << startState << ". There are only " << transitions.size() << " states in this memory structure.");
STORM_LOG_THROW(goalState < transitions.size(), storm::exceptions::InvalidOperationException, "Invalid index of goal state: " << startState << ". There are only " << transitions.size() << " states in this memory structure.");
STORM_LOG_THROW(formula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidOperationException, "The formula '" << *formula << "' is not propositional");
STORM_LOG_THROW(modelStates.size() == modelTransitions.getRowGroupCount(), storm::exceptions::InvalidOperationException, "The modelStates have invalid size.");
STORM_LOG_THROW(!modelChoices || modelChoices->size() == modelTransitions.getRowGroupCount(), storm::exceptions::InvalidOperationException, "The modelChoices have invalid size.");
// translate the two bitvectors to a single BitVector that indicates the corresponding model transitions.
transitions[startState][goalState] = formula;
storm::storage::BitVector transitionVector(modelTransitions.getEntryCount(), false);
if (modelChoices) {
for (auto const& choice : modelChoices.get()) {
for (auto entryIt = modelTransitions.getRow(choice).begin(); entryIt < modelTransitions.getRow(choice).end(); ++entryIt) {
if (modelStates.get(entryIt->getColumn())) {
transitionVector.set(entryIt - modelTransitions.begin());
}
}
}
} else {
for (uint_fast64_t choice = 0; choice < modelTransitions.getRowCount(); ++choice) {
for (auto entryIt = modelTransitions.getRow(choice).begin(); entryIt < modelTransitions.getRow(choice).end(); ++entryIt) {
if (modelStates.get(entryIt->getColumn())) {
transitionVector.set(entryIt - modelTransitions.begin());
}
}
}
}
// Do not insert the transition if it is never taken.
if (transitionVector.empty()) {
transitions[startState][goalState] = boost::none;
} else {
transitions[startState][goalState] = std::move(transitionVector);
}
}
void MemoryStructureBuilder::setLabel(uint_fast64_t const& state, std::string const& label) {
template <typename ValueType, typename RewardModelType>
void MemoryStructureBuilder<ValueType, RewardModelType>::setLabel(uint_fast64_t const& state, std::string const& label) {
STORM_LOG_THROW(state < transitions.size(), storm::exceptions::InvalidOperationException, "Can not add label to state with index " << state << ". There are only " << transitions.size() << " states in this memory structure.");
if (!stateLabeling.containsLabel(label)) {
stateLabeling.addLabel(label);
}
stateLabeling.addLabelToState(label, state);
}
MemoryStructure MemoryStructureBuilder::build() {
return MemoryStructure(std::move(transitions), std::move(stateLabeling));
template <typename ValueType, typename RewardModelType>
MemoryStructure MemoryStructureBuilder<ValueType, RewardModelType>::build() {
return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates));
}
template class MemoryStructureBuilder<double>;
template class MemoryStructureBuilder<storm::RationalNumber>;
template class MemoryStructureBuilder<storm::RationalFunction>;
}
}

40
src/storm/storage/memorystructure/MemoryStructureBuilder.h
View File

@ -3,44 +3,66 @@
#include <vector>
#include <memory>
#include "storm/logic/Formula.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/storage/memorystructure/MemoryStructure.h"
namespace storm {
namespace storage {
template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
class MemoryStructureBuilder {
public:
/*!
* Initializes a new builder for a memory structure
* @param numberOfStates The number of states the resulting memory structure should have
* @param numberOfMemoryStates The number of states the resulting memory structure should have
*/
MemoryStructureBuilder(uint_fast64_t const& numberOfStates);
MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model);
/*!
* Specifies a transition. The formula should be a propositional formula
* Specifies for the given initial state of the model the corresponding initial memory state.
*
* @note The default initial memory state is 0.
*
* @param initialModelState the index of an initial state of the model.
* @param initialMemoryState the initial memory state associated to the corresponding model state.
*/
void setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr<storm::logic::Formula const> formula);
void setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState);
/*!
* Specifies a transition of the memory structure.
* The interpretation is that we switch from startState to goalState upon entering one of the specified model states (via one of the specified choices).
*
* @note If it is not possible to move from startState to goalState, such a transition does not have to be set explicitly.
*
* @param startState the memorystate in which the transition starts
* @param goalState the memorystate in which the transition ends
* @param modelStates the model states that trigger this transition.
* @param modelChoices if given, filers the choices of the model that trigger this transition.
*
*/
void setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, storm::storage::BitVector const& modelStates, boost::optional<storm::storage::BitVector> const& modelChoices = boost::none);
/*!
* Sets a label to the given state.
* Sets a label to the given memory state.
*/
void setLabel(uint_fast64_t const& state, std::string const& label);
/*!
* Builds the memory structure.
* @note Calling this invalidates this builder.
* @note When calling this method, the specified transitions should be deterministic and complete. This is not checked.
* @note When calling this method, the specified transitions should be deterministic and complete, i.e., every triple
* (memoryState, modelChoice, modelState) should uniquely specify a successor memory state.
*/
MemoryStructure build();
private:
storm::models::sparse::Model<ValueType, RewardModelType> const& model;
MemoryStructure::TransitionMatrix transitions;
storm::models::sparse::StateLabeling stateLabeling;
std::vector<uint_fast64_t> initialMemoryStates;
};
}

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

@ -31,11 +31,15 @@ namespace storm {
// 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()) {
// Note: The initial state of a memory structure is always 0.
initialStates.set(modelInit * memoryStateCount + memorySuccessors[modelInit * memoryStateCount], true);
initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true);
++memoryInitIt;
}
STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states.");
storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates);
// Compute the mapping to the states of the result
uint_fast64_t reachableStateCount = 0;
toResultStateMapping = std::vector<uint_fast64_t> (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits<uint_fast64_t>::max());
@ -64,21 +68,18 @@ namespace storm {
return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState];
}
template <typename ValueType>
std::vector<uint_fast64_t> SparseModelMemoryProduct<ValueType>::computeMemorySuccessors() const {
uint_fast64_t modelStateCount = model.getNumberOfStates();
uint_fast64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount();
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
std::vector<uint_fast64_t> result(modelStateCount * memoryStateCount, std::numeric_limits<uint_fast64_t>::max());
std::vector<uint_fast64_t> result(modelTransitionCount * memoryStateCount, std::numeric_limits<uint_fast64_t>::max());
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> mc(model);
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
for (uint_fast64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) {
auto const& transition = memory.getTransitionMatrix()[memoryState][transitionGoal];
if (transition) {
auto mcResult = mc.check(*transition);
for (auto const& modelState : mcResult->asExplicitQualitativeCheckResult().getTruthValuesVector()) {
result[modelState * memoryStateCount + memoryState] = transitionGoal;
auto const& memoryTransition = memory.getTransitionMatrix()[memoryState][transitionGoal];
if (memoryTransition) {
for (auto const& modelTransitionIndex : memoryTransition.get()) {
result[modelTransitionIndex * memoryStateCount + memoryState] = transitionGoal;
}
}
}
@ -99,10 +100,12 @@ namespace storm {
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint_fast64_t memoryState = stateIndex % memoryStateCount;
for (auto const& modelTransition : model.getTransitionMatrix().getRowGroup(modelState)) {
if (!storm::utility::isZero(modelTransition.getValue())) {
uint_fast64_t successorModelState = modelTransition.getColumn();
uint_fast64_t successorMemoryState = memorySuccessors[successorModelState * memoryStateCount + memoryState];
auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState);
for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) {
if (!storm::utility::isZero(modelTransitionIt->getValue())) {
uint_fast64_t successorModelState = modelTransitionIt->getColumn();
uint_fast64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin();
uint_fast64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState];
uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState;
if (!reachableStates.get(successorStateIndex)) {
reachableStates.set(successorStateIndex, true);
@ -128,9 +131,11 @@ namespace storm {
for (auto const& stateIndex : reachableStates) {
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint_fast64_t memoryState = stateIndex % memoryStateCount;
for (auto const& entry : model.getTransitionMatrix().getRow(modelState)) {
uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue());
auto const& modelRow = model.getTransitionMatrix().getRow(modelState);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
++currentRow;
}
@ -158,10 +163,12 @@ namespace storm {
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint_fast64_t memoryState = stateIndex % memoryStateCount;
builder.newRowGroup(currentRow);
for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) {
for (auto const& entry : model.getTransitionMatrix().getRow(modelRow)) {
uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue());
for (uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) {
auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
++currentRow;
}
@ -268,9 +275,11 @@ namespace storm {
for (uint_fast64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) {
uint_fast64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset;
uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset;
for (auto const& entry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) {
uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState];
builder.addNextValue(resRowIndex, getResultState(entry.getColumn(), successorMemoryState), entry.getValue());
auto const& rewardMatrixRow = rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex);
for (auto entryIt = rewardMatrixRow.begin(); entryIt != rewardMatrixRow.end(); ++entryIt) {
uint_fast64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin();
uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(resRowIndex, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
}
}

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

@ -37,8 +37,8 @@ namespace storm {
private:
// Computes for each pair of memory and model state the successor memory state
// The resulting vector maps (modelState * memoryStateCount) + memoryState to the corresponding successor state of the memory structure
// 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<uint_fast64_t> computeMemorySuccessors() const;
// Computes the reachable states of the resulting model

Write Preview
Loading…
Cancel
Save