From 6d24ea96063425678a1155eb0c035fd6717664c1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 17 Feb 2021 21:30:54 +0100 Subject: [PATCH] Silenced many 'loop variable is always a copy' warnings --- .../SMTMinimalLabelSetGenerator.h | 2 +- src/storm-parsers/parser/PrismParser.cpp | 2 +- .../csl/helper/SparseCtmcCslHelper.cpp | 20 +++++------ .../helper/SparseMarkovAutomatonCslHelper.cpp | 8 ++--- ...arseDeterministicInfiniteHorizonHelper.cpp | 4 +-- ...eNondeterministicInfiniteHorizonHelper.cpp | 6 ++-- .../DeterministicSchedsLpChecker.cpp | 12 +++---- .../DeterministicSchedsObjectiveHelper.cpp | 8 ++--- ...ewardBoundedMdpPcaaWeightVectorChecker.cpp | 10 +++--- .../SparseMultiObjectivePreprocessor.cpp | 4 +-- .../SparseMultiObjectiveRewardAnalysis.cpp | 2 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 6 ++-- .../SparseMdpEndComponentInformation.cpp | 2 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 20 +++++------ .../prctl/helper/rewardbounded/EpochModel.cpp | 12 +++---- .../MultiDimensionalRewardUnfolding.cpp | 20 +++++------ .../helper/rewardbounded/ProductModel.cpp | 36 +++++++++---------- .../helper/rewardbounded/QuantileHelper.cpp | 12 +++---- .../ExplicitQuantitativeCheckResult.cpp | 2 +- .../TopologicalLinearEquationSolver.cpp | 2 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 2 +- src/storm/storage/FlexibleSparseMatrix.cpp | 6 ++-- src/storm/storage/Scheduler.cpp | 2 +- src/storm/storage/SparseMatrix.cpp | 8 ++--- src/storm/storage/geometry/NativePolytope.cpp | 2 +- src/storm/storage/geometry/Polytope.cpp | 6 ++-- .../nativepolytopeconversion/QuickHull.cpp | 2 +- .../memorystructure/MemoryStructure.cpp | 4 +-- .../MemoryStructureBuilder.cpp | 4 +-- .../SparseModelMemoryProduct.cpp | 24 ++++++------- ...arseModelNondeterministicMemoryProduct.cpp | 6 ++-- src/storm/transformer/GoalStateMerger.cpp | 2 +- src/storm/transformer/MemoryIncorporation.cpp | 2 +- src/storm/transformer/SubsystemBuilder.cpp | 8 ++--- src/storm/utility/graph.cpp | 16 ++++----- 35 files changed, 142 insertions(+), 142 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 0c257678f..609bd8d50 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1909,7 +1909,7 @@ namespace storm { // Create a queue of reachable prob0E(psi) states so we can check which commands need to be added // to give them a strategy that avoids psi states. std::queue prob0EWorklist; - for (auto const& e : reachableProb0EStates) { + for (auto e : reachableProb0EStates) { prob0EWorklist.push(e); } diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 1fa1a38c7..470993e8f 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -408,7 +408,7 @@ namespace storm { } } if (!unprocessed.empty()) { - for (auto const& formulaIndex : unprocessed) { + for (auto formulaIndex : unprocessed) { STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Invalid expression for formula '" << formulas[formulaIndex].getName() << "' at line '" << formulas[formulaIndex].getLineNumber() << "':\n\t" << formulaExpressions[formulaIndex]); } STORM_LOG_THROW(unprocessed.getNumberOfSetBits() == 1, storm::exceptions::WrongFormatException, "Unable to parse expressions for " << unprocessed.getNumberOfSetBits() << " formulas. This could be due to circular dependencies"); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 58cdd4b15..64e2df615 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -47,7 +47,7 @@ namespace storm { // If we need to compute values with relative precision, it might be necessary to increase the precision requirements (epsilon) ValueType newEpsilon = epsilon; // Only consider positions that are relevant for the solve goal (e.g. initial states of the model) and are supposed to have a non-zero value - for (auto const& state : relevantPositions) { + for (auto state : relevantPositions) { if (storm::utility::isZero(resultVector[state])) { newEpsilon = std::min(epsilon * storm::utility::convertNumber(0.1), newEpsilon); } else { @@ -120,7 +120,7 @@ namespace storm { if (!statesWithProbabilityGreater0NonPsi.empty()) { // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. ValueType uniformizationRate = 0; - for (auto const& state : statesWithProbabilityGreater0NonPsi) { + for (auto state : statesWithProbabilityGreater0NonPsi) { uniformizationRate = std::max(uniformizationRate, exitRates[state]); } uniformizationRate *= 1.02; @@ -153,7 +153,7 @@ namespace storm { storm::utility::vector::selectVectorValues(subResult, relevantStates, result); ValueType uniformizationRate = 0; - for (auto const& state : relevantStates) { + for (auto state : relevantStates) { uniformizationRate = std::max(uniformizationRate, exitRates[state]); } uniformizationRate *= 1.02; @@ -181,7 +181,7 @@ namespace storm { if (!statesWithProbabilityGreater0NonPsi.empty()) { // Find the maximal rate of all 'maybe' states to take it as the uniformization rate. ValueType uniformizationRate = storm::utility::zero(); - for (auto const& state : statesWithProbabilityGreater0NonPsi) { + for (auto state : statesWithProbabilityGreater0NonPsi) { uniformizationRate = std::max(uniformizationRate, exitRates[state]); } uniformizationRate *= 1.02; @@ -206,7 +206,7 @@ namespace storm { // Then compute the transient probabilities of being in such a state after t time units. For this, // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. ValueType uniformizationRate = storm::utility::zero(); - for (auto const& state : relevantStates) { + for (auto state : relevantStates) { uniformizationRate = std::max(uniformizationRate, exitRates[state]); } uniformizationRate *= 1.02; @@ -229,7 +229,7 @@ namespace storm { // Then compute the transient probabilities of being in such a state after t time units. For this, // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. ValueType uniformizationRate = storm::utility::zero(); - for (auto const& state : statesWithProbabilityGreater0) { + for (auto state : statesWithProbabilityGreater0) { uniformizationRate = std::max(uniformizationRate, exitRates[state]); } uniformizationRate *= 1.02; @@ -495,7 +495,7 @@ namespace storm { storm::storage::SparseMatrix transposedMatrix(rateMatrix); transposedMatrix.makeRowsAbsorbing(psiStates); std::vector newRates = exitRates; - for (auto const& state : psiStates) { + for (auto state : psiStates) { newRates[state] = storm::utility::one(); } @@ -510,7 +510,7 @@ namespace storm { if (!relevantStates.empty()) { // Find the maximal rate of all relevant states to take it as the uniformization rate. ValueType uniformizationRate = 0; - for (auto const& state : relevantStates) { + for (auto state : relevantStates) { uniformizationRate = std::max(uniformizationRate, newRates[state]); } uniformizationRate *= 1.02; @@ -534,7 +534,7 @@ namespace storm { // Set initial states size_t i = 0; ValueType initDist = storm::utility::one() / initialStates.getNumberOfSetBits(); - for (auto const& state : relevantStates) { + for (auto state : relevantStates) { if (initialStates.get(state)) { values[i] = initDist; } @@ -567,7 +567,7 @@ namespace storm { // the uniformization rate, and the diagonal needs to be set to the negative exit rate of the // state plus the self-loop rate and then increased by one. uint_fast64_t currentRow = 0; - for (auto const& state : maybeStates) { + for (auto state : maybeStates) { for (auto& element : uniformizedMatrix.getRow(currentRow)) { if (element.getColumn() == currentRow) { element.setValue((element.getValue() - exitRates[state]) / uniformizationRate + storm::utility::one()); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index bdd1f544b..df0fe5d79 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -255,7 +255,7 @@ namespace storm { // Store the best solution we have found so far. if (relevantMaybeStates) { auto currentSolIt = bestKnownSolution.begin(); - for (auto const& state : relevantMaybeStates.get()) { + for (auto state : relevantMaybeStates.get()) { // We take the average of the lower and upper bounds *currentSolIt = (maybeStatesValuesLower[state] + maybeStatesValuesUpper[state]) / two; ++currentSolIt; @@ -360,7 +360,7 @@ namespace storm { storm::storage::SparseMatrixBuilder builder(submatrix.getRowCount(), submatrix.getColumnCount()); auto markovianStateColumns = markovianMaybeStates % maybeStates; uint64_t row = 0; - for (auto const& selfloopColumn : markovianStateColumns) { + for (auto selfloopColumn : markovianStateColumns) { ValueType const& oldExitRate = oldRates[row]; bool foundSelfoop = false; for (auto const& entry : submatrix.getRow(row)) { @@ -385,7 +385,7 @@ namespace storm { void uniformize(storm::storage::SparseMatrix& matrix, std::vector>& oneSteps, std::vector const& oldRates, ValueType uniformizationRate, storm::storage::BitVector const& selfloopColumns) { uint64_t row = 0; - for (auto const& selfloopColumn : selfloopColumns) { + for (auto selfloopColumn : selfloopColumns) { ValueType const& oldExitRate = oldRates[row]; if (oldExitRate == uniformizationRate) { // Already uniformized. @@ -415,7 +415,7 @@ namespace storm { ValueType rateDiff = newUniformizationRate - oldUniformizationRate; ValueType rateFraction = oldUniformizationRate / newUniformizationRate; uint64_t row = 0; - for (auto const& selfloopColumn : selfloopColumns) { + for (auto selfloopColumn : selfloopColumns) { for (auto& v : matrix.getRow(row)) { if (v.getColumn() == selfloopColumn) { ValueType newSelfLoop = rateDiff + v.getValue() * oldUniformizationRate; diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp index a987b2c47..440b9e1a2 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp @@ -372,7 +372,7 @@ namespace storm { // Create the SSP right-hand-side std::vector rhs; rhs.reserve(sspMatrix.getRowCount()); - for (auto const& state : statesNotInComponent) { + for (auto state : statesNotInComponent) { ValueType stateValue = storm::utility::zero(); for (auto const& transition : this->_transitionMatrix.getRow(state)) { if (!statesNotInComponent.get(transition.getColumn())) { @@ -409,7 +409,7 @@ namespace storm { // Map the non-component states to their index in the SSP. Note that the order of these states will be preserved. uint64_t numberOfNonComponentStates = 0; storm::storage::BitVector statesNotInComponent = ~statesInComponents; - for (auto const& nonComponentState : statesNotInComponent) { + for (auto nonComponentState : statesNotInComponent) { stateIndexMap[nonComponentState] = numberOfNonComponentStates; ++numberOfNonComponentStates; } diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp index 4dcd8088f..a6d4cb7dd 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.cpp @@ -285,7 +285,7 @@ namespace storm { storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, numberOfSspStates , 0, true, true, numberOfSspStates); // If the source state of a transition is not contained in any component, we copy its choices (and perform the necessary modifications). uint64_t currentSspChoice = 0; - for (auto const& nonComponentState : statesNotInComponent) { + for (auto nonComponentState : statesNotInComponent) { sspMatrixBuilder.newRowGroup(currentSspChoice); for (uint64_t choice = choiceIndices[nonComponentState]; choice < choiceIndices[nonComponentState + 1]; ++choice, ++currentSspChoice) { rhs.push_back(storm::utility::zero()); @@ -417,14 +417,14 @@ namespace storm { // Now take care of the non-component states. Note that the order of these states will be preserved. uint64_t numberOfNonComponentStates = 0; storm::storage::BitVector statesNotInComponent = ~statesInComponents; - for (auto const& nonComponentState : statesNotInComponent) { + for (auto nonComponentState : statesNotInComponent) { inputToSspStateMap[nonComponentState] = numberOfNonComponentStates; ++numberOfNonComponentStates; } // Finalize the mapping for the component states which now still assigns component states to to their component index. // To make sure that they point to the auxiliary states (located at the end of the SspMatrix), we need to shift them by the // number of states that are not in a component. - for (auto const& mecState : statesInComponents) { + for (auto mecState : statesInComponents) { inputToSspStateMap[mecState] += numberOfNonComponentStates; } diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index b4c97539f..f24b19896 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -147,7 +147,7 @@ namespace storm { unprocessed.erase(currentIt); bool hasSubEc = false; - for (auto const& removedState : currentStates) { + for (auto removedState : currentStates) { storm::storage::BitVector subset = currentStates; subset.set(removedState, false); storm::storage::MaximalEndComponentDecomposition subMecs(mecTransitions, backwardTransitions, subset); @@ -389,7 +389,7 @@ namespace storm { STORM_LOG_WARN_COND(largestUpperBound < storm::utility::convertNumber(1e5), "Found a large upper bound '" << storm::utility::convertNumber(largestUpperBound) << "' in the LP encoding. This might trigger numerical instabilities."); // create choiceValue variables and assert deterministic ones. std::vector choiceValVars(model.getNumberOfChoices()); - for (auto const& state : nonBottomStates) { + for (auto state : nonBottomStates) { for (uint64_t globalChoice = groups[state]; globalChoice < groups[state + 1]; ++globalChoice) { choiceValVars[globalChoice] = lpModel->addBoundedContinuousVariable("y" + std::to_string(globalChoice), storm::utility::zero(), visitingTimesUpperBounds[state]).getExpression(); if (model.getNumberOfChoices(state) > 1) {; @@ -400,7 +400,7 @@ namespace storm { // create EC 'slack' variables for states that lie in an ec std::vector ecValVars(model.getNumberOfStates()); if (hasEndComponents) { - for (auto const& state : nonBottomStates) { + for (auto state : nonBottomStates) { // For the in-out-encoding, all objectives have the same ECs (because there are no non-zero scheduler independend state values). // Hence, we only care for the variables of the first objective. if (ecVars.front()[state].isInitialized()) { @@ -413,7 +413,7 @@ namespace storm { std::vector bottomStatesIn; std::vector> ins(numStates), outs(numStates); ins[initialState].push_back(one); - for (auto const& state : nonBottomStates) { + for (auto state : nonBottomStates) { for (uint64_t globalChoice = groups[state]; globalChoice < groups[state + 1]; ++globalChoice) { for (auto const& transition : model.getTransitionMatrix().getRow(globalChoice)) { uint64_t successor = transition.getColumn(); @@ -433,7 +433,7 @@ namespace storm { } // Assert 'in == out' at each state - for (auto const& state : nonBottomStates) { + for (auto state : nonBottomStates) { lpModel->addConstraint("", storm::expressions::sum(ins[state]) == storm::expressions::sum(outs[state])); } @@ -444,7 +444,7 @@ namespace storm { for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) { auto choiceValueOffsets = objectiveHelper[objIndex].getChoiceValueOffsets(); std::vector objValue; - for (auto const& state : nonBottomStates) { + for (auto state : nonBottomStates) { for (uint64_t globalChoice = groups[state]; globalChoice < groups[state + 1]; ++globalChoice) { auto choiceValueIt = choiceValueOffsets.find(globalChoice); if (choiceValueIt != choiceValueOffsets.end()) { diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp index 5c01236e5..82a7f7e7e 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp @@ -75,13 +75,13 @@ namespace storm { auto backwardTransitions = model.getBackwardTransitions(); { storm::storage::BitVector prob1States = storm::utility::graph::performProb1A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates); - for (auto const& prob1State : prob1States) { + for (auto prob1State : prob1States) { result[prob1State] = storm::utility::one(); } } { storm::storage::BitVector prob0States = storm::utility::graph::performProb0A(backwardTransitions, phiStates, psiStates); - for (auto const& prob0State : prob0States) { + for (auto prob0State : prob0States) { result[prob0State] = storm::utility::zero(); } } @@ -93,7 +93,7 @@ namespace storm { storm::storage::BitVector statesWithoutReward = rewardModel.get().getStatesWithZeroReward(model.getTransitionMatrix()); rew0States = storm::utility::graph::performProb1A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), model.getBackwardTransitions(), statesWithoutReward, rew0States); } - for (auto const& rew0State : rew0States) { + for (auto rew0State : rew0States) { result[rew0State] = storm::utility::zero(); } } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isTotalRewardFormula()) { @@ -102,7 +102,7 @@ namespace storm { storm::storage::BitVector statesWithoutReward = rewardModel.get().getStatesWithZeroReward(model.getTransitionMatrix()); storm::storage::BitVector rew0States = storm::utility::graph::performProbGreater0E(model.getBackwardTransitions(), statesWithoutReward, ~statesWithoutReward); rew0States.complement(); - for (auto const& rew0State : rew0States) { + for (auto rew0State : rew0States) { result[rew0State] = storm::utility::zero(); } } else { diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp index bd8215448..a8e12d4a9 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp @@ -145,7 +145,7 @@ namespace storm { auto stepSolutionIt = epochModel.stepSolutions.begin(); auto stepChoiceIt = epochModel.stepChoices.begin(); - for (auto const& state : epochModel.epochInStates) { + for (auto state : epochModel.epochInStates) { // Obtain the best choice for this state according to the weighted combination of objectives ValueType bestValue; uint64_t bestChoice = std::numeric_limits::max(); @@ -216,20 +216,20 @@ namespace storm { ValueType weight = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; if (!storm::utility::isZero(weight)) { std::vector const& objectiveReward = epochModel.objectiveRewards[objIndex]; - for (auto const& choice : epochModel.objectiveRewardFilter[objIndex]) { + for (auto choice : epochModel.objectiveRewardFilter[objIndex]) { cachedData.bMinMax[choice] += weight * objectiveReward[choice]; } } } auto stepSolutionIt = epochModel.stepSolutions.begin(); - for (auto const& choice : epochModel.stepChoices) { + for (auto choice : epochModel.stepChoices) { cachedData.bMinMax[choice] += stepSolutionIt->front(); ++stepSolutionIt; } // Invoke the min max solver cachedData.minMaxSolver->solveEquations(env, cachedData.xMinMax, cachedData.bMinMax); - for (auto const& state : epochModel.epochInStates) { + for (auto state : epochModel.epochInStates) { result.emplace_back(); result.back().reserve(solutionSize); result.back().push_back(cachedData.xMinMax[state]); @@ -301,7 +301,7 @@ namespace storm { STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); cachedData.linEqSolver->solveEquations(env, x, cachedData.bLinEq); auto resultIt = result.begin(); - for (auto const& state : epochModel.epochInStates) { + for (auto state : epochModel.epochInStates) { resultIt->push_back(x[state]); ++resultIt; } diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index 1fd427456..1dd76128f 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -202,7 +202,7 @@ namespace storm { if (!absorbingStates.empty()) { // We can make the states absorbing and delete unreachable states. storm::storage::BitVector subsystemActions(model->getNumberOfChoices(), true); - for (auto const& absorbingState : absorbingStates) { + for (auto absorbingState : absorbingStates) { for (uint64_t action = model->getTransitionMatrix().getRowGroupIndices()[absorbingState]; action < model->getTransitionMatrix().getRowGroupIndices()[absorbingState + 1]; ++action) { subsystemActions.set(action, false); } @@ -419,7 +419,7 @@ namespace storm { // Transform to expected total rewards: // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a reachableFromInit state to a goalState std::vector objectiveRewards(data.model->getTransitionMatrix().getRowCount(), storm::utility::zero()); - for (auto const& state : reachableFromInit) { + for (auto state : reachableFromInit) { for (uint_fast64_t row = data.model->getTransitionMatrix().getRowGroupIndices()[state]; row < data.model->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { objectiveRewards[row] = data.model->getTransitionMatrix().getConstrainedRowSum(row, rightSubformulaResult); } diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp index 7ae3e3d73..f02d872fd 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp @@ -93,7 +93,7 @@ namespace storm { storm::storage::BitVector maxRewardsToCheck(preprocessorResult.preprocessedModel->getNumberOfChoices(), true); storm::storage::BitVector minRewardsToCheck(preprocessorResult.preprocessedModel->getNumberOfChoices(), true); - for (auto const& objIndex : preprocessorResult.maybeInfiniteRewardObjectives) { + for (auto objIndex : preprocessorResult.maybeInfiniteRewardObjectives) { STORM_LOG_ASSERT(preprocessorResult.objectives[objIndex].formula->isRewardOperatorFormula(), "Objective needs to be checked for finite reward but has no reward operator."); auto const& rewModel = preprocessorResult.preprocessedModel->getRewardModel(preprocessorResult.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); auto unrelevantChoices = rewModel.getChoicesWithZeroReward(transitions); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index f17f0cd27..7139684a2 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -107,7 +107,7 @@ namespace storm { } std::map result; - for (auto const& initState : model.getInitialStates()) { + for (auto initState : model.getInitialStates()) { result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState); } @@ -152,7 +152,7 @@ namespace storm { std::vector const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint().getResultHint(); statesWithProbability1 = storm::storage::BitVector(maybeStates.size(), false); storm::storage::BitVector nonMaybeStates = ~maybeStates; - for (auto const& state : nonMaybeStates) { + for (auto state : nonMaybeStates) { if (storm::utility::isOne(resultsForNonMaybeStates[state])) { statesWithProbability1.set(state, true); result[state] = storm::utility::one(); @@ -267,7 +267,7 @@ namespace storm { // Set initial states size_t i = 0; ValueType initDist = storm::utility::one() / storm::utility::convertNumber(initialStates.getNumberOfSetBits()); - for (auto const& state : relevantStates) { + for (auto state : relevantStates) { if (initialStates.get(state)) { b[i] = initDist; } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp index 8db9a6c75..66ecb7d04 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp @@ -351,7 +351,7 @@ namespace storm { storm::storage::BitVector maybeStatesWithoutChoice(maybeStates.size(), false); storm::storage::BitVector ecStayChoices(transitionMatrix.getRowCount(), false); auto notInEcResultIt = fromResult.begin(); - for (auto const& state : maybeStates) { + for (auto state : maybeStates) { if (this->isStateInEc(state)) { STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix."); STORM_LOG_ASSERT(!ecToExitChoicesBefore.empty(), "No EC exit choices available. End Components have probably been build without."); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index eb63176c6..746fa85ad 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -103,7 +103,7 @@ namespace storm { } std::map result; - for (auto const& initState : initialStates) { + for (auto initState : initialStates) { result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState); } @@ -272,7 +272,7 @@ namespace storm { // Compute the hint w.r.t. the given subsystem. hintChoices.clear(); hintChoices.reserve(maybeStates.getNumberOfSetBits()); - for (auto const& state : maybeStates) { + for (auto state : maybeStates) { uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice(); if (selectedChoices) { uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state]; @@ -461,7 +461,7 @@ namespace storm { result.statesWithProbability1 = storm::storage::BitVector(result.maybeStates.size()); result.statesWithProbability0 = storm::storage::BitVector(result.maybeStates.size()); storm::storage::BitVector nonMaybeStates = ~result.maybeStates; - for (auto const& state : nonMaybeStates) { + for (auto state : nonMaybeStates) { if (storm::utility::isOne(resultsForNonMaybeStates[state])) { result.statesWithProbability1.set(state, true); } else { @@ -518,12 +518,12 @@ namespace storm { // We also need to define some arbitrary choice for the remaining states to obtain a fully defined scheduler. if (goal.minimize()) { storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.statesWithProbability0, transitionMatrix, scheduler); - for (auto const& prob1State : qualitativeStateSets.statesWithProbability1) { + for (auto prob1State : qualitativeStateSets.statesWithProbability1) { scheduler.setChoice(0, prob1State); } } else { storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates, scheduler); - for (auto const& prob0State : qualitativeStateSets.statesWithProbability0) { + for (auto prob0State : qualitativeStateSets.statesWithProbability0) { scheduler.setChoice(0, prob0State); } } @@ -760,7 +760,7 @@ namespace storm { storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix); auto ecElimResult = storm::transformer::EndComponentEliminator::transform(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), choicesWithoutReward, rew0AStates, true); storm::storage::BitVector newRew0AStates(ecElimResult.matrix.getRowGroupCount(), false); - for (auto const& oldRew0AState : rew0AStates) { + for (auto oldRew0AState : rew0AStates) { newRew0AStates.set(ecElimResult.oldToNewStateMapping[oldRew0AState]); } @@ -780,7 +780,7 @@ namespace storm { }, newRew0AStates, qualitative, false, [&] () { storm::storage::BitVector newStatesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false); - for (auto const& oldStateWithoutRew : statesWithoutReward) { + for (auto oldStateWithoutRew : statesWithoutReward) { newStatesWithoutReward.set(ecElimResult.oldToNewStateMapping[oldStateWithoutRew]); } return newStatesWithoutReward; @@ -884,7 +884,7 @@ namespace storm { result.infinityStates = storm::storage::BitVector(result.maybeStates.size()); result.rewardZeroStates = storm::storage::BitVector(result.maybeStates.size()); storm::storage::BitVector nonMaybeStates = ~result.maybeStates; - for (auto const& state : nonMaybeStates) { + for (auto state : nonMaybeStates) { if (storm::utility::isZero(resultsForNonMaybeStates[state])) { result.rewardZeroStates.set(state, true); } else { @@ -934,12 +934,12 @@ namespace storm { // the states with reward zero/infinity. if (goal.minimize()) { storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.rewardZeroStates, transitionMatrix, backwardTransitions, qualitativeStateSets.rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter()); - for (auto const& state : qualitativeStateSets.infinityStates) { + for (auto state : qualitativeStateSets.infinityStates) { scheduler.setChoice(0, state); } } else { storm::utility::graph::computeSchedulerRewInf(qualitativeStateSets.infinityStates, transitionMatrix, scheduler); - for (auto const& state : qualitativeStateSets.rewardZeroStates) { + for (auto state : qualitativeStateSets.rewardZeroStates) { scheduler.setChoice(0, state); } } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp index 63c1e2c76..68bb6622f 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp @@ -22,7 +22,7 @@ namespace storm { epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits()); auto stepSolutionIt = epochModel.stepSolutions.begin(); auto stepChoiceIt = epochModel.stepChoices.begin(); - for (auto const& state : epochModel.epochInStates) { + for (auto state : epochModel.epochInStates) { while (*stepChoiceIt < state) { ++stepChoiceIt; ++stepSolutionIt; @@ -83,11 +83,11 @@ namespace storm { // Prepare the right hand side of the equation system b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); std::vector const& objectiveValues = epochModel.objectiveRewards.front(); - for (auto const& choice : epochModel.objectiveRewardFilter.front()) { + for (auto choice : epochModel.objectiveRewardFilter.front()) { b[choice] = objectiveValues[choice]; } auto stepSolutionIt = epochModel.stepSolutions.begin(); - for (auto const& choice : epochModel.stepChoices) { + for (auto choice : epochModel.stepChoices) { b[choice] += *stepSolutionIt; ++stepSolutionIt; } @@ -109,7 +109,7 @@ namespace storm { auto stepSolutionIt = epochModel.stepSolutions.begin(); auto stepChoiceIt = epochModel.stepChoices.begin(); - for (auto const& state : epochModel.epochInStates) { + for (auto state : epochModel.epochInStates) { // Obtain the best choice for this state ValueType bestValue; uint64_t lastChoice = epochModel.epochMatrix.getRowGroupIndices()[state + 1]; @@ -194,11 +194,11 @@ namespace storm { // Prepare the right hand side of the equation system b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); std::vector const& objectiveValues = epochModel.objectiveRewards.front(); - for (auto const& choice : epochModel.objectiveRewardFilter.front()) { + for (auto choice : epochModel.objectiveRewardFilter.front()) { b[choice] = objectiveValues[choice]; } auto stepSolutionIt = epochModel.stepSolutions.begin(); - for (auto const& choice : epochModel.stepChoices) { + for (auto choice : epochModel.stepChoices) { b[choice] += *stepSolutionIt; ++stepSolutionIt; } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 269564375..834c21ad9 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -284,7 +284,7 @@ namespace storm { if (!upperBoundedDimensions.empty()) { // To not invalidate upper-bounded dimensions, one needs to consider MECS where no reward for such a dimension is collected. for (uint64_t choiceIndex = 0; choiceIndex < model.getNumberOfChoices(); ++choiceIndex) { - for (auto const& dim : upperBoundedDimensions) { + for (auto dim : upperBoundedDimensions) { if (epochManager.getDimensionOfEpoch(epochSteps[choiceIndex], dim) != 0) { choicesWithoutUpperBoundedStep.set(choiceIndex, false); break; @@ -301,14 +301,14 @@ namespace storm { } } } - for (auto const& choice : nonMecChoices) { - for (auto const& dim : infLowerBoundedDimensions) { + for (auto choice : nonMecChoices) { + for (auto dim : infLowerBoundedDimensions) { epochManager.setDimensionOfEpoch(epochSteps[choice], dim, 0); } } // Translate the dimension to '>0' - for (auto const& dim : infLowerBoundedDimensions) { + for (auto dim : infLowerBoundedDimensions) { dimensions[dim].boundType = DimensionBoundType::LowerBound; dimensions[dim].maxValue = 0; } @@ -390,7 +390,7 @@ namespace storm { } epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); auto stepSolIt = epochModel.stepSolutions.begin(); - for (auto const& reducedChoice : epochModel.stepChoices) { + for (auto reducedChoice : epochModel.stepChoices) { uint64_t productChoice = epochModelToProductChoiceMap[reducedChoice]; uint64_t productState = productModel->getProductStateFromChoice(productChoice); auto const& memoryState = productModel->getMemoryState(productState); @@ -403,7 +403,7 @@ namespace storm { for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { bool rewardEarned = !storm::utility::isZero(epochModel.objectiveRewards[objIndex][reducedChoice]); if (rewardEarned) { - for (auto const& dim : objectiveDimensions[objIndex]) { + for (auto dim : objectiveDimensions[objIndex]) { if ((dimensions[dim].boundType == DimensionBoundType::UpperBound) == epochManager.isBottomDimension(successorEpoch, dim) && productModel->getMemoryStateManager().isRelevantDimension(memoryState, dim)) { rewardEarned = false; break; @@ -554,7 +554,7 @@ namespace storm { epochModelToProductChoiceMap.clear(); epochModelToProductChoiceMap.reserve(numEpochModelStates); productToEpochModelStateMapping.assign(nonZeroRewardStates.size(), zeroRewardInState); - for (auto const& productState : nonZeroRewardStates) { + for (auto productState : nonZeroRewardStates) { productToEpochModelStateMapping[productState] = epochModelToProductChoiceMap.size(); epochModelToProductChoiceMap.push_back(productState); } @@ -596,14 +596,14 @@ namespace storm { } epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); - for (auto const& productState : productInStates) { + for (auto productState : productInStates) { STORM_LOG_ASSERT(productToEpochModelStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); epochModel.epochInStates.set(productToEpochModelStateMapping[productState], true); } std::vector toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits::max()); std::vector epochModelStateToInStateMap = epochModel.epochInStates.getNumberOfSetBitsBeforeIndices(); - for (auto const& productState : productInStates) { + for (auto productState : productInStates) { toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[productToEpochModelStateMapping[productState]]; } productStateToEpochModelInStateMap = std::make_shared const>(std::move(toEpochModelInStatesMap)); @@ -866,7 +866,7 @@ namespace storm { if (productModel->getProb1InitialStates(objIndex) && productModel->getProb1InitialStates(objIndex)->get(initialStateIndex)) { // Check whether the objective can actually hold in this epoch bool objectiveHolds = true; - for (auto const& dim : objectiveDimensions[objIndex]) { + for (auto dim : objectiveDimensions[objIndex]) { if (dimensions[dim].boundType == DimensionBoundType::LowerBound && !epochManager.isBottomDimension(epoch, dim)) { objectiveHolds = false; } else if (dimensions[dim].boundType == DimensionBoundType::UpperBound && epochManager.isBottomDimension(epoch, dim)) { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp index 871fde4de..21b351fd3 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp @@ -105,7 +105,7 @@ namespace storm { } std::vector dimensionIndexMap; - for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { + for (auto globalDimensionIndex : objectiveDimensions[objIndex]) { dimensionIndexMap.push_back(globalDimensionIndex); } @@ -123,7 +123,7 @@ namespace storm { // Get the set of states that for all subobjectives satisfy either the left or the right subformula storm::storage::BitVector constraintStates(model.getNumberOfStates(), true); - for (auto const& dim : objectiveDimensions[objIndex]) { + for (auto dim : objectiveDimensions[objIndex]) { auto const& dimension = dimensions[dim]; STORM_LOG_ASSERT(dimension.formula->isBoundedUntilFormula(), "Unexpected Formula type"); constraintStates &= @@ -139,7 +139,7 @@ namespace storm { if (memStatePrimeBV.isSubsetOf(memStateBV)) { std::shared_ptr transitionFormula = storm::logic::Formula::getTrueFormula(); - for (auto const& subObjIndex : memStateBV) { + for (auto subObjIndex : memStateBV) { std::shared_ptr subObjFormula = dimensions[dimensionIndexMap[subObjIndex]].formula->asBoundedUntilFormula().getRightSubformula().asSharedPointer(); if (memStatePrimeBV.get(subObjIndex)) { subObjFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, subObjFormula); @@ -164,7 +164,7 @@ namespace storm { prob1InitialStates[objIndex] = initialTransitionStates; } - for (auto const& initState : initialTransitionStates) { + for (auto initState : initialTransitionStates) { objMemoryBuilder.setInitialMemoryState(initState, memStatePrime); } } @@ -175,7 +175,7 @@ namespace storm { // Build the memory labels for (uint64_t memState = 0; memState < objMemStates.size(); ++memState) { auto const& memStateBV = objMemStates[memState]; - for (auto const& subObjIndex : memStateBV) { + for (auto subObjIndex : memStateBV) { objMemoryBuilder.setLabel(memState, dimensions[dimensionIndexMap[subObjIndex]].memoryLabel.get()); } } @@ -246,7 +246,7 @@ namespace storm { } for (auto const& initEpochClass : initEpochClasses) { auto memStateIt = memory.getInitialMemoryStates().begin(); - for (auto const& initState : model.getInitialStates()) { + for (auto initState : model.getInitialStates()) { uint64_t transformedMemoryState = transformMemoryState(memoryStateMap[*memStateIt], initEpochClass, memoryStateManager.getInitialMemoryState()); reachableProductStates[transformedMemoryState].set(initState, true); ++memStateIt; @@ -267,7 +267,7 @@ namespace storm { // Find the remaining set of reachable states via DFS. std::vector> dfsStack; for (MemoryState const& memState : memoryStateMap) { - for (auto const& modelState : reachableProductStates[memState]) { + for (auto modelState : reachableProductStates[memState]) { dfsStack.emplace_back(modelState, memState); } } @@ -294,7 +294,7 @@ namespace storm { } for (uint64_t memStateIndex = 0; memStateIndex < memoryStateManager.getMemoryStateCount(); ++memStateIndex) { - for (auto const& modelState : reachableProductStates[memoryStateMap[memStateIndex]]) { + for (auto modelState : reachableProductStates[memoryStateMap[memStateIndex]]) { productBuilder.addReachableState(modelState, memStateIndex); } } @@ -359,12 +359,12 @@ namespace storm { if (formula.isProbabilityOperatorFormula()) { storm::modelchecker::SparsePropositionalModelChecker> mc(getProduct()); std::vector dimensionIndexMap; - for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { + for (auto globalDimensionIndex : objectiveDimensions[objIndex]) { dimensionIndexMap.push_back(globalDimensionIndex); } std::shared_ptr sinkStatesFormula; - for (auto const& dim : objectiveDimensions[objIndex]) { + for (auto dim : objectiveDimensions[objIndex]) { auto memLabelFormula = std::make_shared(dimensions[dim].memoryLabel.get()); if (sinkStatesFormula) { sinkStatesFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, sinkStatesFormula, memLabelFormula); @@ -382,7 +382,7 @@ namespace storm { // find out whether objective reward should be earned within this epoch class bool collectRewardInEpoch = true; - for (auto const& subObjIndex : relevantObjectives) { + for (auto subObjIndex : relevantObjectives) { if (dimensions[dimensionIndexMap[subObjIndex]].boundType == DimensionBoundType::UpperBound && epochManager.isBottomDimensionEpochClass(epochClass, dimensionIndexMap[subObjIndex])) { collectRewardInEpoch = false; break; @@ -410,7 +410,7 @@ namespace storm { storm::storage::BitVector relevantStates = mc.check(*relevantStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector relevantChoices = getProduct().getTransitionMatrix().getRowFilter(relevantStates); storm::storage::BitVector goalStates = mc.check(*goalStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - for (auto const& choice : relevantChoices) { + for (auto choice : relevantChoices) { objRew[choice] += getProduct().getTransitionMatrix().getConstrainedRowSum(choice, goalStates); } } @@ -423,7 +423,7 @@ namespace storm { STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); bool rewardCollectedInEpoch = true; if (formula.getSubformula().isCumulativeRewardFormula()) { - for (auto const& dim : objectiveDimensions[objIndex]) { + for (auto dim : objectiveDimensions[objIndex]) { if (epochManager.isBottomDimensionEpochClass(epochClass, dim)) { rewardCollectedInEpoch = false; break; @@ -534,7 +534,7 @@ namespace storm { storm::storage::BitVector ecInStates(getProduct().getNumberOfStates(), false); if (considerInitialStates) { - for (auto const& initState : getProduct().getInitialStates()) { + for (auto initState : getProduct().getInitialStates()) { uint64_t transformedInitState = transformProductState(initState, epochClass, memoryStateManager.getInitialMemoryState()); ecInStates.set(transformedInitState, true); } @@ -548,12 +548,12 @@ namespace storm { } STORM_LOG_ASSERT(reachableStates.find(predecessor) != reachableStates.end(), "Could not find reachable states of predecessor epoch class."); storm::storage::BitVector predecessorStates = reachableStates.find(predecessor)->second; - for (auto const& predecessorState : predecessorStates) { + for (auto predecessorState : predecessorStates) { uint64_t predecessorMemoryState = getMemoryState(predecessorState); for (uint64_t choice = getProduct().getTransitionMatrix().getRowGroupIndices()[predecessorState]; choice < getProduct().getTransitionMatrix().getRowGroupIndices()[predecessorState + 1]; ++choice) { bool choiceLeadsToThisClass = false; Epoch const& choiceStep = getSteps()[choice]; - for (auto const& dim : positiveStepDimensions) { + for (auto dim : positiveStepDimensions) { if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) { choiceLeadsToThisClass = true; } @@ -583,7 +583,7 @@ namespace storm { bool choiceLeadsOutsideOfEpoch = false; Epoch const& choiceStep = getSteps()[choice]; - for (auto const& dim : nonBottomDimensions) { + for (auto dim : nonBottomDimensions) { if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) { choiceLeadsOutsideOfEpoch = true; break; @@ -613,7 +613,7 @@ namespace storm { MemoryState memoryStatePrime = memoryState; for (auto const& objDimensions : objectiveDimensions) { - for (auto const& dim : objDimensions) { + for (auto dim : objDimensions) { auto const& dimension = dimensions[dim]; if (dimension.memoryLabel) { bool dimUpperBounded = dimension.boundType == DimensionBoundType::UpperBound; diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index fc2f39099..f5c16001b 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -202,7 +202,7 @@ namespace storm { std::vector permutation; for (auto const& v : quantileFormula.getBoundVariables()) { uint64_t openDim = 0; - for (auto const& dim : getOpenDimensions()) { + for (auto dim : getOpenDimensions()) { if (getVariableForDimension(dim) == v) { permutation.push_back(openDim); break; @@ -244,7 +244,7 @@ namespace storm { storm::storage::BitVector lowerBoundedDimensions(getDimension()); storm::storage::BitVector downwardClosedDimensions(getDimension()); bool hasLowerValueBound = storm::logic::isLowerBound(boundedUntilOp->getComparisonType()); - for (auto const& d : getOpenDimensions()) { + for (auto d : getOpenDimensions()) { if (consideredDimensions.get(d)) { bool hasLowerCostBound = boundedUntilOp->getSubformula().asBoundedUntilFormula().hasLowerBound(d); lowerBoundedDimensions.set(d, hasLowerCostBound); @@ -260,7 +260,7 @@ namespace storm { bool onlyUpperCostBounds = lowerBoundedDimensions.empty(); bool onlyLowerCostBounds = lowerBoundedDimensions == consideredDimensions; if (onlyUpperCostBounds || onlyLowerCostBounds) { - for (auto const& k : consideredDimensions) { + for (auto k : consideredDimensions) { storm::storage::BitVector subQueryDimensions = consideredDimensions; subQueryDimensions.set(k, false); bool subQueryComplement = complementaryQuery != ((onlyUpperCostBounds && hasLowerValueBound) || (onlyLowerCostBounds && !hasLowerValueBound)); @@ -268,7 +268,7 @@ namespace storm { for (auto const& subQueryCostLimit : subQueryResult.first.getGenerator()) { CostLimits initPoint; uint64_t i = 0; - for (auto const& dim : consideredDimensions) { + for (auto dim : consideredDimensions) { if (dim == k) { initPoint.push_back(CostLimit::infinity()); } else { @@ -294,7 +294,7 @@ namespace storm { MultiDimensionalRewardUnfolding rewardUnfolding(model, boundedUntilOp, infinityVariables); if (computeQuantile(env, consideredDimensions, *boundedUntilOp, lowerBoundedDimensions, satCostLimits, unsatCostLimits, rewardUnfolding)) { std::vector scalingFactors; - for (auto const& dim : consideredDimensions) { + for (auto dim : consideredDimensions) { scalingFactors.push_back(rewardUnfolding.getDimension(dim).scalingFactor); } std::pair> result(satCostLimits, scalingFactors); @@ -386,7 +386,7 @@ namespace storm { // Transform candidate cost limits to an appropriate start epoch auto startEpoch = rewardUnfolding.getStartEpoch(true); auto costLimitIt = currentCandidate.begin(); - for (auto const& dim : consideredDimensions) { + for (auto dim : consideredDimensions) { if (lowerBoundedDimensions.get(dim)) { if (costLimitIt->get() > 0) { rewardUnfolding.getEpochManager().setDimensionOfEpoch(startEpoch, dim, costLimitIt->get() - 1); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index c191941b9..e05c83344 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -82,7 +82,7 @@ namespace storm { if (this->isResultForAllStates()) { map_type newMap; - for (auto const& element : filterTruthValues) { + for (auto element : filterTruthValues) { STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results."); newMap.emplace(element, this->getValueVector()[element]); } diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index 5ae744203..deb16069e 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -195,7 +195,7 @@ namespace storm { // b Vector std::vector sccB; sccB.reserve(scc.getNumberOfSetBits()); - for (auto const& row : scc) { + for (auto row : scc) { ValueType bi = globalB[row]; for (auto const& entry : this->A->getRow(row)) { if (!scc.get(entry.getColumn())) { diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index e186b9dd8..548ef2d75 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -311,7 +311,7 @@ namespace storm { // b Vector std::vector sccB; sccB.reserve(sccRows.getNumberOfSetBits()); - for (auto const& row : sccRows) { + for (auto row : sccRows) { ValueType bi = globalB[row]; for (auto const& entry : this->A->getRow(row)) { if (!sccRowGroups.get(entry.getColumn())) { diff --git a/src/storm/storage/FlexibleSparseMatrix.cpp b/src/storm/storage/FlexibleSparseMatrix.cpp index 1ee642c65..76ab951d3 100644 --- a/src/storm/storage/FlexibleSparseMatrix.cpp +++ b/src/storm/storage/FlexibleSparseMatrix.cpp @@ -208,7 +208,7 @@ namespace storm { template storm::storage::SparseMatrix FlexibleSparseMatrix::createSparseMatrix(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) { uint_fast64_t numEntries = 0; - for (auto const& rowIndex : rowConstraint) { + for (auto rowIndex : rowConstraint) { auto const& row = data[rowIndex]; for(auto const& entry : row) { if (columnConstraint.get(entry.getColumn())) { @@ -230,14 +230,14 @@ namespace storm { std::vector oldToNewColumnIndexMapping(getColumnCount(), getColumnCount()); uint_fast64_t newColumnIndex = 0; - for (auto const& oldColumnIndex : columnConstraint) { + for (auto oldColumnIndex : columnConstraint) { oldToNewColumnIndexMapping[oldColumnIndex] = newColumnIndex++; } storm::storage::SparseMatrixBuilder matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, true, !hasTrivialRowGrouping(), numRowGroups); uint_fast64_t currRowIndex = 0; auto rowGroupIndexIt = getRowGroupIndices().begin(); - for (auto const& oldRowIndex : rowConstraint) { + for (auto oldRowIndex : rowConstraint) { if(!hasTrivialRowGrouping() && oldRowIndex >= *rowGroupIndexIt) { matrixBuilder.newRowGroup(currRowIndex); // Skip empty row groups diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 59db79429..63e24c1da 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -56,7 +56,7 @@ namespace storm { template bool Scheduler::isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState) const { - for (auto const& selectedState : selectedStates) { + for (auto selectedState : selectedStates) { auto& schedulerChoice = schedulerChoices[memoryState][selectedState]; if (!schedulerChoice.isDefined()) { return false; diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 05a526702..9fb9996c2 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -726,7 +726,7 @@ namespace storm { template storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraint) const { storm::storage::BitVector result(this->getRowCount(), false); - for (auto const& group : groupConstraint) { + for (auto group : groupConstraint) { uint_fast64_t const endOfGroup = this->getRowGroupIndices()[group + 1]; for (uint_fast64_t row = this->getRowGroupIndices()[group]; row < endOfGroup; ++row) { bool choiceSatisfiesColumnConstraint = true; @@ -1120,7 +1120,7 @@ namespace storm { // Count the number of entries of the resulting matrix uint_fast64_t entryCount = 0; - for (auto const& row : rowsToKeep) { + for (auto row : rowsToKeep) { entryCount += this->getRow(row).getNumberOfEntries(); } @@ -1160,13 +1160,13 @@ namespace storm { SparseMatrix SparseMatrix::filterEntries(storm::storage::BitVector const& rowFilter) const { // Count the number of entries in the resulting matrix. index_type entryCount = 0; - for (auto const& row : rowFilter) { + for (auto row : rowFilter) { entryCount += getRow(row).getNumberOfEntries(); } // Build the resulting matrix. SparseMatrixBuilder builder(getRowCount(), getColumnCount(), entryCount); - for (auto const& row : rowFilter) { + for (auto row : rowFilter) { for (auto const& entry : getRow(row)) { builder.addNextValue(row, entry.getColumn(), entry.getValue()); } diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index 886f01b91..53172816a 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -437,7 +437,7 @@ namespace storm { } std::vector> newHalfspaces; newHalfspaces.reserve(keptConstraints.getNumberOfSetBits()); - for (auto const& row : keptConstraints) { + for (auto row : keptConstraints) { newHalfspaces.emplace_back(storm::adapters::EigenAdapter::toStdVector(EigenVector(A.row(row))), b(row)); } return create(newHalfspaces, boost::none); diff --git a/src/storm/storage/geometry/Polytope.cpp b/src/storm/storage/geometry/Polytope.cpp index 3db106719..7e6f9b3fd 100644 --- a/src/storm/storage/geometry/Polytope.cpp +++ b/src/storm/storage/geometry/Polytope.cpp @@ -74,7 +74,7 @@ namespace storm { std::vector auxiliaryPoints = points; auxiliaryPoints.reserve(auxiliaryPoints.size() * (1 + selectedDimensions.getNumberOfSetBits())); for (auto const& point : points) { - for (auto const& dim : selectedDimensions) { + for (auto dim : selectedDimensions) { auxiliaryPoints.push_back(point); auxiliaryPoints.back()[dim] -= storm::utility::one(); } @@ -83,7 +83,7 @@ namespace storm { // The downward closure is obtained by erasing the halfspaces for which the normal vector is negative for one of the selected dimensions. for (auto& h : auxiliaryHalfspaces) { bool allGreaterEqZero = true; - for (auto const& dim : selectedDimensions) { + for (auto dim : selectedDimensions) { allGreaterEqZero &= (h.normalVector()[dim] >= storm::utility::zero()); } if (allGreaterEqZero){ @@ -122,7 +122,7 @@ namespace storm { verticesOnHalfspace.set(v); } } - for(auto const& v : verticesOnHalfspace) { + for(auto v : verticesOnHalfspace) { neighborsOfVertices[v] |= verticesOnHalfspace; neighborsOfVertices[v].set(v, false); } diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index ce0594bb9..b6529a981 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -228,7 +228,7 @@ namespace storm { //Found candidates. Now swap them to the front. const uint_fast64_t numOfGoodCandidates = goodCandidates.getNumberOfSetBits(); - for ( auto const& goodCandidate : goodCandidates) { + for ( auto goodCandidate : goodCandidates) { if (goodCandidate >= numOfGoodCandidates) { uint_fast64_t notGoodCandidate = *notGoodCandidates.begin(); assert(notGoodCandidate < numOfGoodCandidates); diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index f8b83a348..83bc7ad81 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -84,7 +84,7 @@ namespace storm { for (std::string lhsLabel : this->getStateLabeling().getLabels()) { storm::storage::BitVector const& lhsLabeledStates = this->getStateLabeling().getStates(lhsLabel); storm::storage::BitVector resLabeledStates(resNumStates, false); - for (auto const& lhsState : lhsLabeledStates) { + for (auto lhsState : lhsLabeledStates) { for (uint_fast64_t rhsState = 0; rhsState < rhsNumStates; ++rhsState) { resState = (lhsState * rhsNumStates) + rhsState; resLabeledStates.set(resState, true); @@ -96,7 +96,7 @@ namespace storm { STORM_LOG_THROW(!resultLabeling.containsLabel(rhsLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of two memory structures: State labelings are not disjoint as both structures contain the label " << rhsLabel << "."); storm::storage::BitVector const& rhsLabeledStates = rhs.getStateLabeling().getStates(rhsLabel); storm::storage::BitVector resLabeledStates(resNumStates, false); - for (auto const& rhsState : rhsLabeledStates) { + for (auto rhsState : rhsLabeledStates) { for (uint_fast64_t lhsState = 0; lhsState < lhsNumStates; ++lhsState) { resState = (lhsState * rhsNumStates) + rhsState; resLabeledStates.set(resState, true); diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index e51e85239..f3a3818cc 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -25,7 +25,7 @@ namespace storm { 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()) { + for (auto initState : model.getInitialStates()) { if (initState == initialModelState) { *initMemStateIt = initialMemoryState; break; @@ -49,7 +49,7 @@ namespace storm { storm::storage::BitVector transitionVector(modelTransitions.getEntryCount(), false); if (modelChoices) { - for (auto const& choice : modelChoices.get()) { + for (auto 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()); diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 1f30f23fb..029387288 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -38,7 +38,7 @@ 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()) { + for (auto modelInit : model.getInitialStates()) { initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true); ++memoryInitIt; } @@ -49,7 +49,7 @@ namespace storm { // Compute the mapping to the states of the result uint64_t reachableStateCount = 0; toResultStateMapping = std::vector (model.getNumberOfStates() * memoryStateCount, std::numeric_limits::max()); - for (auto const& reachableState : reachableStates) { + for (auto reachableState : reachableStates) { toResultStateMapping[reachableState] = reachableStateCount; ++reachableStateCount; } @@ -116,7 +116,7 @@ namespace storm { for (uint64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { auto const& memoryTransition = memory.getTransitionMatrix()[memoryState][transitionGoal]; if (memoryTransition) { - for (auto const& modelTransitionIndex : memoryTransition.get()) { + for (auto modelTransitionIndex : memoryTransition.get()) { memorySuccessors[modelTransitionIndex * memoryStateCount + memoryState] = transitionGoal; } } @@ -179,13 +179,13 @@ namespace storm { storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix() { uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResTransitions = 0; - for (auto const& stateIndex : reachableStates) { + for (auto stateIndex : reachableStates) { numResTransitions += model.getTransitionMatrix().getRow(stateIndex / memoryStateCount).getNumberOfEntries(); } storm::storage::SparseMatrixBuilder builder(numResStates, numResStates, numResTransitions, true); uint64_t currentRow = 0; - for (auto const& stateIndex : reachableStates) { + for (auto stateIndex : reachableStates) { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; auto const& modelRow = model.getTransitionMatrix().getRow(modelState); @@ -205,7 +205,7 @@ namespace storm { uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; uint64_t numResTransitions = 0; - for (auto const& stateIndex : reachableStates) { + for (auto stateIndex : reachableStates) { uint64_t modelState = stateIndex / memoryStateCount; for (uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { ++numResChoices; @@ -215,7 +215,7 @@ namespace storm { storm::storage::SparseMatrixBuilder builder(numResChoices, numResStates, numResTransitions, true, true, numResStates); uint64_t currentRow = 0; - for (auto const& stateIndex : reachableStates) { + for (auto stateIndex : reachableStates) { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; builder.newRowGroup(currentRow); @@ -239,7 +239,7 @@ namespace storm { uint64_t numResChoices = 0; uint64_t numResTransitions = 0; bool hasTrivialNondeterminism = true; - for (auto const& stateIndex : reachableStates) { + for (auto stateIndex : reachableStates) { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; storm::storage::SchedulerChoice choice = scheduler->getChoice(modelState, memoryState); @@ -273,7 +273,7 @@ namespace storm { storm::storage::SparseMatrixBuilder builder(numResChoices, numResStates, numResTransitions, true, !hasTrivialNondeterminism, hasTrivialNondeterminism ? 0 : numResStates); uint64_t currentRow = 0; - for (auto const& stateIndex : reachableStates) { + for (auto stateIndex : reachableStates) { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; if (!hasTrivialNondeterminism) { @@ -337,7 +337,7 @@ namespace storm { for (std::string modelLabel : model.getStateLabeling().getLabels()) { if (modelLabel != "init") { storm::storage::BitVector resLabeledStates(numResStates, false); - for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) { + for (auto modelState : model.getStateLabeling().getStates(modelLabel)) { for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { if (isStateReachable(modelState, memoryState)) { resLabeledStates.set(getResultState(modelState, memoryState), true); @@ -350,7 +350,7 @@ namespace storm { for (std::string memoryLabel : memory.getStateLabeling().getLabels()) { STORM_LOG_THROW(!resultLabeling.containsLabel(memoryLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of model and memory structure: State labelings are not disjoint as both structures contain the label " << memoryLabel << "."); storm::storage::BitVector resLabeledStates(numResStates, false); - for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) { + for (auto memoryState : memory.getStateLabeling().getStates(memoryLabel)) { for (uint64_t modelState = 0; modelState < modelStateCount; ++modelState) { if (isStateReachable(modelState, memoryState)) { resLabeledStates.set(getResultState(modelState, memoryState), true); @@ -362,7 +362,7 @@ namespace storm { storm::storage::BitVector initialStates(numResStates, false); auto memoryInitIt = memory.getInitialMemoryStates().begin(); - for (auto const& modelInit : model.getInitialStates()) { + for (auto modelInit : model.getInitialStates()) { initialStates.set(getResultState(modelInit, *memoryInitIt), true); ++memoryInitIt; } diff --git a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp index 16d3f7065..483e15fb2 100644 --- a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp @@ -70,7 +70,7 @@ namespace storm { 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 memStatePrime : memory.getTransitions(memState)) { for (auto const& entry : origTransitions.getRow(origRow)) { builder.addNextValue(row, getProductState(entry.getColumn(), memStatePrime), entry.getValue()); } @@ -90,11 +90,11 @@ namespace storm { // 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)) { + for (auto modelState : model.getStateLabeling().getStates(labelName)) { newStates.set(getProductState(modelState, memory.getInitialState())); } } else { - for (auto const& modelState : model.getStateLabeling().getStates(labelName)) { + for (auto modelState : model.getStateLabeling().getStates(labelName)) { for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { newStates.set(getProductState(modelState, memState)); } diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index 4c3bf0898..45199bd93 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -218,7 +218,7 @@ namespace storm { boost::optional> transitionRewards; if (origRewardModel.hasTransitionRewards()) { storm::storage::SparseMatrixBuilder builder(choiceCount, stateCount, 0, true); - for (auto const& row : resultData.keptChoices) { + for (auto row : resultData.keptChoices) { boost::optional targetValue, sinkValue; for (auto const& entry : origRewardModel.getTransitionRewardMatrix().getRow(row)) { uint_fast64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()]; diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp index 5879cde50..104fa56d0 100644 --- a/src/storm/transformer/MemoryIncorporation.cpp +++ b/src/storm/transformer/MemoryIncorporation.cpp @@ -38,7 +38,7 @@ namespace storm { 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()) { + for (auto initState : model.getInitialStates()) { builder.setInitialMemoryState(initState, goalStates.get(initState) ? 1 : 0); } return builder.build(); diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index db700196f..bdb0e8e91 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -114,7 +114,7 @@ namespace storm { // store them now, before changing them. result.keptActions = keptActions; } - for (auto const& deadlockState : deadlockStates) { + for (auto deadlockState : deadlockStates) { keptActions.set(groupIndices[deadlockState], true); } @@ -148,13 +148,13 @@ namespace storm { assert(deadlockStates.getNumberOfSetBits() == subDeadlockStates.getNumberOfSetBits()); // erase rewards, choice labels, choice origins for (auto& rewModel : components.rewardModels) { - for (auto const& state : subDeadlockStates) { + for (auto state : subDeadlockStates) { rewModel.second.clearRewardAtState(state, components.transitionMatrix); } } if (components.choiceLabeling) { storm::storage::BitVector nonDeadlockChoices(components.transitionMatrix.getRowCount(), true); - for (auto const& state : subDeadlockStates) { + for (auto state : subDeadlockStates) { auto const& choice = components.transitionMatrix.getRowGroupIndices()[state]; nonDeadlockChoices.set(choice, false); } @@ -163,7 +163,7 @@ namespace storm { } } if (components.choiceOrigins) { - for (auto const& state : subDeadlockStates) { + for (auto state : subDeadlockStates) { auto const& choice = components.transitionMatrix.getRowGroupIndices()[state]; components.choiceOrigins.get()->clearOriginOfChoice(choice); } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index ddb1a4eca..3d97bf778 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -39,7 +39,7 @@ namespace storm { // Initialize the stack used for the DFS with the states. std::vector stack; stack.reserve(initialStates.size()); - for (auto const& state : initialStates) { + for (auto state : initialStates) { if (constraintStates.get(state)) { stack.push_back(state); } @@ -173,7 +173,7 @@ namespace storm { storm::storage::BitVector statesWithChoice(transitionMatrix.getRowGroupCount(), false); uint_fast64_t state = 0; - for (auto const& choice : choices) { + for (auto choice : choices) { // Get the correct state while (choice >= transitionMatrix.getRowGroupIndices()[state + 1]) { ++state; @@ -205,7 +205,7 @@ namespace storm { // Only keep the states that can be reached after performing one of the specified choices statesWithChoice &= candidateStates; storm::storage::BitVector choiceTargets(transitionMatrix.getRowGroupCount(), false); - for (auto const& state : statesWithChoice) { + for (auto state : statesWithChoice) { for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { bool choiceStaysInCandidateSet = true; for (auto const& entry : transitionMatrix.getRow(choice)) { @@ -228,7 +228,7 @@ namespace storm { while (!candidateStates.empty()) { // Update the states with a choice that stays within the set of candidates statesWithChoice &= candidateStates; - for (auto const& state : statesWithChoice) { + for (auto state : statesWithChoice) { bool stateHasChoice = false; for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { bool choiceStaysInCandidateSet = true; @@ -271,7 +271,7 @@ namespace storm { storm::storage::BitVector statesInQueue(transitionMatrix.getRowGroupCount()); storm::storage::sparse::state_type currentPosition = 0; - for (auto const& initialState : initialStates) { + for (auto initialState : initialStates) { stateQueue.emplace_back(initialState, 0); statesInQueue.set(initialState); } @@ -446,7 +446,7 @@ namespace storm { void computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); - for (auto const& state : states) { + for (auto state : states) { bool setValue = false; STORM_LOG_ASSERT(nondeterministicChoiceIndices[state+1] - nondeterministicChoiceIndices[state] > 0, "Expected at least one action enabled in state " << state); for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { @@ -473,7 +473,7 @@ namespace storm { void computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler) { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); - for (auto const& state : states) { + for (auto state : states) { bool setValue = false; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool oneSuccessorInStates = false; @@ -552,7 +552,7 @@ namespace storm { void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter) { // set an arbitrary (valid) choice for the psi states. - for (auto const& psiState : psiStates) { + for (auto psiState : psiStates) { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { if (!scheduler.getChoice(psiState, memState).isDefined()) { scheduler.setChoice(0, psiState, memState);