From 16041bc93658d46f660b8dd1d3a59cddfe890ed2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 14 Jun 2017 16:06:42 +0200 Subject: [PATCH] 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) --- .../SparseMultiObjectivePreprocessor.cpp | 41 ++++++---- .../memorystructure/MemoryStructure.cpp | 31 +++++--- .../storage/memorystructure/MemoryStructure.h | 8 +- .../MemoryStructureBuilder.cpp | 75 ++++++++++++++++--- .../memorystructure/MemoryStructureBuilder.h | 40 +++++++--- .../SparseModelMemoryProduct.cpp | 59 ++++++++------- .../SparseModelMemoryProduct.h | 4 +- 7 files changed, 185 insertions(+), 73 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 252af5a7a..b2da20897 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -69,8 +69,8 @@ namespace storm { template SparseMultiObjectivePreprocessor::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) { - storm::storage::MemoryStructureBuilder memoryBuilder(1); - memoryBuilder.setTransition(0,0, storm::logic::Formula::getTrueFormula()); + storm::storage::MemoryStructureBuilder memoryBuilder(1, model); + memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); memory = std::make_shared(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 void SparseMultiObjectivePreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data) { + storm::modelchecker::SparsePropositionalModelChecker 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 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 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::OperatorType::Not, formula.getLeftSubformula().asSharedPointer()); - auto targetFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer()); - builder.setTransition(0, 0, std::make_shared(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(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 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 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::OperatorType::Not, formula.getSubformula().asSharedPointer())); - builder.setTransition(0, 1, formula.getSubformula().asSharedPointer()); - builder.setTransition(1, 1, std::make_shared(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(data.memory->product(objectiveMemory)); diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index 69266f562..3d9348c44 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -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 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&& 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 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>(resNumStates)); + TransitionMatrix resultTransitions(resNumStates, std::vector>(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::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 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 @@ -129,8 +144,6 @@ namespace storm { template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; - - } } diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h index 41052c7fa..9df320fd3 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -20,7 +20,7 @@ namespace storm { class MemoryStructure { public: - typedef std::vector>> TransitionMatrix; + typedef std::vector>> 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 const& initialMemoryStates); + MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates); TransitionMatrix const& getTransitionMatrix() const; storm::models::sparse::StateLabeling const& getStateLabeling() const; + std::vector const& getInitialMemoryStates() const; uint_fast64_t getNumberOfStates() const; /*! @@ -60,6 +61,7 @@ namespace storm { private: TransitionMatrix transitions; storm::models::sparse::StateLabeling stateLabeling; + std::vector initialMemoryStates; }; } diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index b2b654a93..9ee23eaa6 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -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>(numberOfStates)), stateLabeling(numberOfStates) { + template + MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model) : model(model), transitions(numberOfMemoryStates, std::vector>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0) { // Intentionally left empty } + + template + void MemoryStructureBuilder::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 + void MemoryStructureBuilder::setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, storm::storage::BitVector const& modelStates, boost::optional const& modelChoices) { + + auto const& modelTransitions = model.getTransitionMatrix(); - void MemoryStructureBuilder::setTransition(uint_fast64_t const& startState, uint_fast64_t const& goalState, std::shared_ptr 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 + void MemoryStructureBuilder::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 + MemoryStructure MemoryStructureBuilder::build() { + return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates)); } + template class MemoryStructureBuilder; + template class MemoryStructureBuilder; + template class MemoryStructureBuilder; + } } diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h index e87992d56..9fbe65c78 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -3,44 +3,66 @@ #include #include -#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 > 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 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 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 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 const& model; MemoryStructure::TransitionMatrix transitions; storm::models::sparse::StateLabeling stateLabeling; + std::vector initialMemoryStates; }; } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index bc4e49782..56b3a6aa0 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -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 (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits::max()); @@ -64,21 +68,18 @@ namespace storm { return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } - template std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { - uint_fast64_t modelStateCount = model.getNumberOfStates(); + uint_fast64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - std::vector result(modelStateCount * memoryStateCount, std::numeric_limits::max()); + std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); - storm::modelchecker::SparsePropositionalModelChecker> 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()); } } } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 170efba3f..0c60923e7 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -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 computeMemorySuccessors() const; // Computes the reachable states of the resulting model