diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 8fd066a00..252af5a7a 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -379,7 +379,7 @@ namespace storm { storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false); targetStateAsVector.set(*mergerResult.targetState, true); // The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself. - result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowIndicesOfRowGroups(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector)); + result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowFilter(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector)); result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true); // There is an additional state in the result result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index a5427ccd8..3087ef7a1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -96,7 +96,7 @@ namespace storm { } STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(getUnderApproximationOfInitialStateResults()))); // Validate that the results are sufficiently precise - ValueType resultingWeightedPrecision = storm::utility::abs(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector)); + ValueType resultingWeightedPrecision = storm::utility::abs(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector)); resultingWeightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weightVector, weightVector)); STORM_LOG_THROW(resultingWeightedPrecision <= weightedPrecision, storm::exceptions::UnexpectedException, "The desired precision was not reached"); } diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index c579b236f..a4149709c 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -266,11 +266,11 @@ namespace storm { if (this->hasStateActionRewards()) { result = storm::utility::vector::filterZero(this->getStateActionRewardVector()); if (this->hasStateRewards()) { - result &= transitionMatrix.getRowIndicesOfRowGroups(storm::utility::vector::filterZero(this->getStateRewardVector())); + result &= transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector())); } } else { if (this->hasStateRewards()) { - result = transitionMatrix.getRowIndicesOfRowGroups(storm::utility::vector::filterZero(this->getStateRewardVector())); + result = transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector())); } else { result = storm::storage::BitVector(transitionMatrix.getRowCount(), true); }