diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 45d99f003..d06b3ce40 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -102,7 +102,7 @@ namespace storm { storm::storage::BitVector probabilisticStates = ~this->model.getMarkovianStates(); result.states = createMS ? this->model.getMarkovianStates() : probabilisticStates; - result.choices = this->model.getTransitionMatrix().getRowIndicesOfRowGroups(result.states); + result.choices = this->model.getTransitionMatrix().getRowFilter(result.states); STORM_LOG_ASSERT(!createMS || result.states.getNumberOfSetBits() == result.choices.getNumberOfSetBits(), "row groups for Markovian states should consist of exactly one row"); //We need to add diagonal entries for selfloops on Markovian states. diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index 066a5f1b7..d9e2610fe 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -69,7 +69,7 @@ namespace storm { // Create the vector of one-step probabilities to go to target states. std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates), maybeStates); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates); computePlayer1Matrix(); applyPreviousResultAsHint = false; @@ -104,7 +104,7 @@ namespace storm { // Create the vector of one-step probabilities to go to target states. std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second); - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates), maybeStates); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates); computePlayer1Matrix(); // Check whether there is an EC consisting of maybestates @@ -146,16 +146,8 @@ namespace storm { std::vector b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); // We need to handle choices that lead to an infinity state. - // As a maybeState does not have reward infinity, such a choice will never be picked. Hence, we can unselect the corresponding rows - storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates); - for (uint_fast64_t row : selectedRows) { - for (auto const& element : this->parametricModel.getTransitionMatrix().getRow(row)) { - if (infinityStates.get(element.getColumn())) { - selectedRows.set(row, false); - break; - } - } - } + // As a maybeState does not have reward infinity, a choice leading to an infinity state will never be picked. Hence, we can unselect the corresponding rows + storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates); parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, selectedRows, maybeStates); computePlayer1Matrix(); diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index f0eb0fc39..88a77b43d 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -140,14 +140,14 @@ namespace storm { this->getTransitionMatrix() = this->getTransitionMatrix().restrictRows(keptChoices); for(auto& rewModel : this->getRewardModels()) { if(rewModel.second.hasStateActionRewards()) { - rewModel.second.getStateActionRewardVector() = storm::utility::vector::filterVector(rewModel.second.getStateActionRewardVector(), keptChoices); + storm::utility::vector::filterVectorInPlace(rewModel.second.getStateActionRewardVector(), keptChoices); } if(rewModel.second.hasTransitionRewards()) { rewModel.second.getTransitionRewardMatrix() = rewModel.second.getTransitionRewardMatrix().restrictRows(keptChoices); } } if(this->hasChoiceLabeling()) { - this->getOptionalChoiceLabeling() = storm::utility::vector::filterVector(this->getOptionalChoiceLabeling().get(), keptChoices); + storm::utility::vector::filterVectorInPlace(this->getOptionalChoiceLabeling().get(), keptChoices); } // Mark the automaton as closed. @@ -329,7 +329,7 @@ namespace storm { storm::models::sparse::StateLabeling stateLabeling = this->getStateLabeling().getSubLabeling(keepStates); boost::optional> optionalChoiceLabeling = this->getOptionalChoiceLabeling(); if (optionalChoiceLabeling) { - optionalChoiceLabeling = storm::utility::vector::filterVector(optionalChoiceLabeling.get(), keepStates); + storm::utility::vector::filterVectorInPlace(optionalChoiceLabeling.get(), keepStates); } //TODO update reward models according to kept states STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 36319b394..d481f7063 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -555,10 +555,11 @@ namespace storm { } template - storm::storage::BitVector SparseMatrix::getRowIndicesOfRowGroups(storm::storage::BitVector const& groups) const { + storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint) const { storm::storage::BitVector res(this->getRowCount(), false); - for(auto group : groups) { - for(uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group+1]; ++row) { + for(auto group : groupConstraint) { + uint_fast64_t const endOfGroup = this->getRowGroupIndices()[group + 1]; + for(uint_fast64_t row = this->getRowGroupIndices()[group]; row < endOfGroup; ++row) { res.set(row, true); } } diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 8aab0d397..cf9211849 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -569,7 +569,7 @@ namespace storm { * @param groups the selected row groups * @return a bit vector that is true at position i iff the row group of row i is selected. */ - storm::storage::BitVector getRowIndicesOfRowGroups(storm::storage::BitVector const& groups) const; + storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint) const; /*! * Returns the indices of all rows that diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index 2f6e524f9..edd19d833 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -173,7 +173,7 @@ namespace storm { } } } - points = storm::utility::vector::filterVector(points, keptPoints); + storm::utility::vector::filterVectorInPlace(points, keptPoints); if (generateRelevantVerticesAndVertexSets) { storm::storage::BitVector keptVertices(relevantVertices.size(), true); @@ -185,7 +185,7 @@ namespace storm { } } } - relevantVertices = storm::utility::vector::filterVector(relevantVertices, keptVertices); + storm::utility::vector::filterVectorInPlace(relevantVertices, keptVertices); STORM_LOG_WARN("Can not retrieve vertex sets for degenerated polytope (not implemented)"); vertexSets.clear(); diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index f7ccc7f19..f9b81f3f6 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -46,11 +46,12 @@ namespace storm { // Get the reward models std::unordered_map rewardModels; for (auto rewardModelName : selectedRewardModels) { - auto origTotalRewards = originalModel.getRewardModel(rewardModelName).getTotalRewardVector(originalModel.getTransitionMatrix()); - auto transitionsOfMaybeStates = originalModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates); - auto resTotalRewards = storm::utility::vector::filterVector(origTotalRewards, transitionsOfMaybeStates); - resTotalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero()); - rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, resTotalRewards))); + auto totalRewards = originalModel.getRewardModel(rewardModelName).getTotalRewardVector(originalModel.getTransitionMatrix()); + auto choicesOfMaybeStates = originalModel.getTransitionMatrix().getRowFilter(maybeStates); + storm::utility::vector::filterVectorInPlace(totalRewards, choicesOfMaybeStates); + // add zero reward for the sink and goal states (if they exists) + totalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero()); + rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, totalRewards))); } // modify the given target and sink states diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm/transformer/SparseParametricModelSimplifier.cpp index 54fba2338..2dd62ce6b 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm/transformer/SparseParametricModelSimplifier.cpp @@ -138,13 +138,13 @@ namespace storm { stateEliminator.eliminateState(state, true); } selectedStates.complement(); - auto keptRows = sparseMatrix.getRowIndicesOfRowGroups(selectedStates); + auto keptRows = sparseMatrix.getRowFilter(selectedStates); storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates); // obtain the reward model for the resulting system std::unordered_map rewardModels; if(rewardModelName) { - actionRewards = storm::utility::vector::filterVector(actionRewards, keptRows); + storm::utility::vector::filterVectorInPlace(actionRewards, keptRows); rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(boost::none, std::move(actionRewards)))); } diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index c26c17774..6bf06a4f9 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -863,8 +863,15 @@ namespace storm { void filterVectorInPlace(std::vector& v, storm::storage::BitVector const& filter) { STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector"); auto vIt = v.begin(); - for(auto index : filter) { - *vIt = std::move(v[index]); + auto filterIt = filter.begin(); + // get the first position where the filter has a 0. + // Note that we do not have to modify the entries of v on all positions before + for (uint_fast64_t i = 0; i == *filterIt && filterIt != filter.end(); ++i) { + ++filterIt; + ++vIt; + } + for (; filterIt != filter.end(); ++filterIt) { + *vIt = std::move(v[*filterIt]); ++vIt; } v.resize(vIt - v.begin()); @@ -875,7 +882,7 @@ namespace storm { bool hasNegativeEntry(std::vector const& v){ return std::any_of(v.begin(), v.end(), [](T value){return value < storm::utility::zero();}); } - + template bool hasPositiveEntry(std::vector const& v){ return std::any_of(v.begin(), v.end(), [](T value){return value > storm::utility::zero();});