From d863fe4156294db4851cf437e2e866325d9bf7f2 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 17 Feb 2021 19:54:44 +0100
Subject: [PATCH 1/4] Jani Export: Power expressions of integer type need to be
type casted.
---
src/storm/storage/jani/JSONExporter.cpp | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index ee2487002..afeac6427 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -632,8 +632,17 @@ namespace storm {
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
opDecl["left"] = anyToJson(expression.getOperand(0)->accept(*this, data));
opDecl["right"] = anyToJson(expression.getOperand(1)->accept(*this, data));
- return opDecl;
+ if (expression.getOperator() == storm::expressions::OperatorType::Power && expression.getType().isIntegerType()) {
+ // power expressions that have integer type need to be "type casted"
+ ExportJsonType trc;
+ trc["op"] = "trc";
+ trc["exp"] = std::move(opDecl);
+ return trc;
+ } else {
+ return opDecl;
+ }
}
+
boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
ExportJsonType opDecl;
opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
@@ -670,6 +679,7 @@ namespace storm {
opDecl["exp"] = anyToJson(expression.getOperand()->accept(*this, data));
return opDecl;
}
+
boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) {
return ExportJsonType(expression.getValue());
}
From 46462d65568fccd64cbd4046d1952f5c34332916 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 17 Feb 2021 20:55:04 +0100
Subject: [PATCH 2/4] Z3Adapter: Fixing translation of XOR operators -
expression's operator^ is supposed to be power, not xor.
---
src/storm/adapters/Z3ExpressionAdapter.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp
index b84c9ba08..b2c2434e1 100644
--- a/src/storm/adapters/Z3ExpressionAdapter.cpp
+++ b/src/storm/adapters/Z3ExpressionAdapter.cpp
@@ -115,7 +115,7 @@ namespace storm {
case Z3_OP_IFF:
return storm::expressions::iff(this->translateExpression(expr.arg(0)), this->translateExpression(expr.arg(1)));
case Z3_OP_XOR:
- return this->translateExpression(expr.arg(0)) ^ this->translateExpression(expr.arg(1));
+ return storm::expressions::xclusiveor(this->translateExpression(expr.arg(0)), this->translateExpression(expr.arg(1)));
case Z3_OP_NOT:
return !this->translateExpression(expr.arg(0));
case Z3_OP_IMPLIES:
From 481d23b904a74c8dcc1c1c1e04393b51955d91aa Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 17 Feb 2021 20:56:08 +0100
Subject: [PATCH 3/4] Replaced storm::expressions::Expression::operator^ by
storm::expressions::pow. An optional flag indicates if we should allow power
expressions of integer type (PRISM semantics) or whether it is always a real
(JANI semantics).
---
src/storm-parsers/parser/ExpressionCreator.cpp | 2 +-
src/storm-parsers/parser/JaniParser.cpp | 2 +-
src/storm/storage/expressions/Expression.cpp | 11 ++++++-----
src/storm/storage/expressions/Expression.h | 13 +++++++++++--
.../expressions/RationalFunctionToExpression.cpp | 2 +-
src/storm/storage/expressions/Type.cpp | 8 ++++++--
src/storm/storage/expressions/Type.h | 2 +-
src/test/storm/storage/ExpressionTest.cpp | 8 +++++---
8 files changed, 32 insertions(+), 16 deletions(-)
diff --git a/src/storm-parsers/parser/ExpressionCreator.cpp b/src/storm-parsers/parser/ExpressionCreator.cpp
index 13ffea01b..941d3889f 100644
--- a/src/storm-parsers/parser/ExpressionCreator.cpp
+++ b/src/storm-parsers/parser/ExpressionCreator.cpp
@@ -130,7 +130,7 @@ namespace storm {
if (this->createExpressions) {
try {
switch (operatorType) {
- case storm::expressions::OperatorType::Power: return e1 ^ e2; break;
+ case storm::expressions::OperatorType::Power: return storm::expressions::pow(e1, e2, true); break;
case storm::expressions::OperatorType::Modulo: return e1 % e2; break;
default: STORM_LOG_ASSERT(false, "Invalid operation."); break;
}
diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp
index 72399c314..58a478aee 100644
--- a/src/storm-parsers/parser/JaniParser.cpp
+++ b/src/storm-parsers/parser/JaniParser.cpp
@@ -1263,7 +1263,7 @@ namespace storm {
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scope.description);
ensureNumericalType(arguments[1], opstring, 1, scope.description);
- return arguments[0]^arguments[1];
+ return storm::expressions::pow(arguments[0], arguments[1]);
} else if (opstring == "exp") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index 873e21fc2..6c5646c5f 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -283,11 +283,6 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().divide(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Divide)));
}
- Expression operator^(Expression const& first, Expression const& second) {
- assertSameManager(first.getBaseExpression(), second.getBaseExpression());
- return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power)));
- }
-
Expression operator%(Expression const& first, Expression const& second) {
assertSameManager(first.getBaseExpression(), second.getBaseExpression());
return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().power(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Modulo)));
@@ -408,6 +403,12 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Xor)));
}
+ Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType) {
+ assertSameManager(base.getBaseExpression(), exponent.getBaseExpression());
+ return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(base.getBaseExpression().getManager(), base.getType().power(exponent.getType(), allowIntegerType), base.getBaseExpressionPointer(), exponent.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Power)));
+ }
+
+
Expression floor(Expression const& first) {
STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'floor' requires numerical operand.");
return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().floorCeil(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Floor)));
diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h
index 22b07734e..ff64b05d7 100644
--- a/src/storm/storage/expressions/Expression.h
+++ b/src/storm/storage/expressions/Expression.h
@@ -32,7 +32,6 @@ namespace storm {
friend Expression operator-(Expression const& first);
friend Expression operator*(Expression const& first, Expression const& second);
friend Expression operator/(Expression const& first, Expression const& second);
- friend Expression operator^(Expression const& first, Expression const& second);
friend Expression operator%(Expression const& first, Expression const& second);
friend Expression operator&&(Expression const& first, Expression const& second);
friend Expression operator||(Expression const& first, Expression const& second);
@@ -51,6 +50,7 @@ namespace storm {
friend Expression implies(Expression const& first, Expression const& second);
friend Expression iff(Expression const& first, Expression const& second);
friend Expression xclusiveor(Expression const& first, Expression const& second);
+ friend Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType);
friend Expression abs(Expression const& first);
friend Expression truncate(Expression const& first);
friend Expression sign(Expression const& first);
@@ -412,7 +412,6 @@ namespace storm {
Expression operator-(Expression const& first);
Expression operator*(Expression const& first, Expression const& second);
Expression operator/(Expression const& first, Expression const& second);
- Expression operator^(Expression const& first, Expression const& second);
Expression operator&&(Expression const& first, Expression const& second);
Expression operator||(Expression const& first, Expression const& second);
Expression operator!(Expression const& first);
@@ -430,6 +429,16 @@ namespace storm {
Expression implies(Expression const& first, Expression const& second);
Expression iff(Expression const& first, Expression const& second);
Expression xclusiveor(Expression const& first, Expression const& second);
+
+ /*!
+ * The type of the resulting expression is
+ * - integer, if base and exponent are integer expressions and allowIntegerType is true
+ * (in this case it is assumed that exponent is always positive), and
+ * - rational, otherwise.
+ * The integer case is to reflect the PRISM semantics
+ * @see https://github.com/ahartmanns/qcomp/issues/103
+ */
+ Expression pow(Expression const& base, Expression const& exponent, bool allowIntegerType = false);
Expression abs(Expression const& first);
Expression truncate(Expression const& first);
Expression sign(Expression const& first);
diff --git a/src/storm/storage/expressions/RationalFunctionToExpression.cpp b/src/storm/storage/expressions/RationalFunctionToExpression.cpp
index 0bbd08038..54607ecfd 100644
--- a/src/storm/storage/expressions/RationalFunctionToExpression.cpp
+++ b/src/storm/storage/expressions/RationalFunctionToExpression.cpp
@@ -49,7 +49,7 @@ namespace storm {
storm::expressions::Expression nominatorPartExpr = manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->coeff()));
for (auto var : varsFunction) {
- nominatorPartExpr = nominatorPartExpr * (manager->getVariable(var.name())^manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->monomial()->exponentOfVariable(var))));
+ nominatorPartExpr = nominatorPartExpr * storm::expressions::pow(manager->getVariable(var.name()), manager->rational(storm::utility::convertNumber<storm::RationalNumber, storm::RationalFunctionCoefficient>(itr->monomial()->exponentOfVariable(var))));
}
if (varsFunction.size() >= 1) {
result = result + nominatorPartExpr;
diff --git a/src/storm/storage/expressions/Type.cpp b/src/storm/storage/expressions/Type.cpp
index bc92c859a..31882116b 100644
--- a/src/storm/storage/expressions/Type.cpp
+++ b/src/storm/storage/expressions/Type.cpp
@@ -215,10 +215,14 @@ namespace storm {
return std::max(*this, other);
}
- Type Type::power(Type const& other) const {
+ Type Type::power(Type const& other, bool allowIntegerType) const {
STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands.");
STORM_LOG_THROW(!this->isBitVectorType() && !other.isBitVectorType(), storm::exceptions::InvalidTypeException, "Operator requires non-bitvector operands.");
- return std::max(*this, other);
+ if (allowIntegerType) {
+ return std::max(*this, other);
+ } else {
+ return this->getManager().getRationalType();
+ }
}
Type Type::logicalConnective(Type const& other) const {
diff --git a/src/storm/storage/expressions/Type.h b/src/storm/storage/expressions/Type.h
index 58c02f64d..b5cba7fab 100644
--- a/src/storm/storage/expressions/Type.h
+++ b/src/storm/storage/expressions/Type.h
@@ -115,7 +115,7 @@ namespace storm {
Type plusMinusTimes(Type const& other) const;
Type minus() const;
Type divide(Type const& other) const;
- Type power(Type const& other) const;
+ Type power(Type const& other, bool allowIntegerType = false) const;
Type logicalConnective(Type const& other) const;
Type logicalConnective() const;
Type numericalComparison(Type const& other) const;
diff --git a/src/test/storm/storage/ExpressionTest.cpp b/src/test/storm/storage/ExpressionTest.cpp
index beadd6e94..b61d549d5 100644
--- a/src/test/storm/storage/ExpressionTest.cpp
+++ b/src/test/storm/storage/ExpressionTest.cpp
@@ -252,10 +252,12 @@ TEST(Expression, OperatorTest) {
ASSERT_NO_THROW(tempExpression = storm::expressions::ceil(rationalVarExpression));
EXPECT_TRUE(tempExpression.hasIntegerType());
- STORM_SILENT_ASSERT_THROW(tempExpression = trueExpression ^ piExpression, storm::exceptions::InvalidTypeException);
- ASSERT_NO_THROW(tempExpression = threeExpression ^ threeExpression);
+ STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::pow(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
+ ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, true));
EXPECT_TRUE(tempExpression.hasIntegerType());
- ASSERT_NO_THROW(tempExpression = intVarExpression ^ rationalVarExpression);
+ ASSERT_NO_THROW(tempExpression = storm::expressions::pow(threeExpression, threeExpression, false));
+ EXPECT_TRUE(tempExpression.hasRationalType());
+ ASSERT_NO_THROW(tempExpression = storm::expressions::pow(intVarExpression, rationalVarExpression));
EXPECT_TRUE(tempExpression.hasRationalType());
STORM_SILENT_ASSERT_THROW(tempExpression = storm::expressions::modulo(trueExpression, piExpression), storm::exceptions::InvalidTypeException);
From 6d24ea96063425678a1155eb0c035fd6717664c1 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 17 Feb 2021 21:30:54 +0100
Subject: [PATCH 4/4] 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<uint_fast64_t> 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<ValueType>(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<ValueType>();
- 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<ValueType>();
- 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<ValueType>();
- 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<ValueType> transposedMatrix(rateMatrix);
transposedMatrix.makeRowsAbsorbing(psiStates);
std::vector<ValueType> newRates = exitRates;
- for (auto const& state : psiStates) {
+ for (auto state : psiStates) {
newRates[state] = storm::utility::one<ValueType>();
}
@@ -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<ValueType>() / 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<ValueType>());
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<ValueType> 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<ValueType>& matrix, std::vector<std::pair<uint64_t, ValueType>>& oneSteps, std::vector<ValueType> 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<ValueType> rhs;
rhs.reserve(sspMatrix.getRowCount());
- for (auto const& state : statesNotInComponent) {
+ for (auto state : statesNotInComponent) {
ValueType stateValue = storm::utility::zero<ValueType>();
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<ValueType> 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<ValueType>());
@@ -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<ValueType> subMecs(mecTransitions, backwardTransitions, subset);
@@ -389,7 +389,7 @@ namespace storm {
STORM_LOG_WARN_COND(largestUpperBound < storm::utility::convertNumber<ValueType>(1e5), "Found a large upper bound '" << storm::utility::convertNumber<double>(largestUpperBound) << "' in the LP encoding. This might trigger numerical instabilities.");
// create choiceValue variables and assert deterministic ones.
std::vector<storm::expressions::Expression> 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<ValueType>(), 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<storm::expressions::Expression> 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<storm::expressions::Expression> bottomStatesIn;
std::vector<std::vector<storm::expressions::Expression>> 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<storm::expressions::Expression> 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<ValueType>();
}
}
{
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<ValueType>();
}
}
@@ -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<ValueType>();
}
} 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<ValueType>();
}
} 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<uint64_t>::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<ValueType> 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<typename SparseModelType::ValueType> objectiveRewards(data.model->getTransitionMatrix().getRowCount(), storm::utility::zero<typename SparseModelType::ValueType>());
- 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<storm::storage::sparse::state_type, ValueType> 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<ValueType> const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().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<ValueType>();
@@ -267,7 +267,7 @@ namespace storm {
// Set initial states
size_t i = 0;
ValueType initDist = storm::utility::one<ValueType>() / storm::utility::convertNumber<ValueType>(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<storm::storage::sparse::state_type, ValueType> 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<ValueType>::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<ValueType>());
std::vector<ValueType> 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<ValueType>());
std::vector<ValueType> 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<uint64_t> toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits<uint64_t>::max());
std::vector<uint64_t> epochModelStateToInStateMap = epochModel.epochInStates.getNumberOfSetBitsBeforeIndices();
- for (auto const& productState : productInStates) {
+ for (auto productState : productInStates) {
toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[productToEpochModelStateMapping[productState]];
}
productStateToEpochModelInStateMap = std::make_shared<std::vector<uint64_t> 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<uint64_t> 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<storm::logic::Formula const> transitionFormula = storm::logic::Formula::getTrueFormula();
- for (auto const& subObjIndex : memStateBV) {
+ for (auto subObjIndex : memStateBV) {
std::shared_ptr<storm::logic::Formula const> subObjFormula = dimensions[dimensionIndexMap[subObjIndex]].formula->asBoundedUntilFormula().getRightSubformula().asSharedPointer();
if (memStatePrimeBV.get(subObjIndex)) {
subObjFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(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<std::pair<uint64_t, MemoryState>> 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<storm::models::sparse::Model<ValueType>> mc(getProduct());
std::vector<uint64_t> dimensionIndexMap;
- for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) {
+ for (auto globalDimensionIndex : objectiveDimensions[objIndex]) {
dimensionIndexMap.push_back(globalDimensionIndex);
}
std::shared_ptr<storm::logic::Formula const> sinkStatesFormula;
- for (auto const& dim : objectiveDimensions[objIndex]) {
+ for (auto dim : objectiveDimensions[objIndex]) {
auto memLabelFormula = std::make_shared<storm::logic::AtomicLabelFormula>(dimensions[dim].memoryLabel.get());
if (sinkStatesFormula) {
sinkStatesFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(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<uint64_t> 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<ValueType, true> rewardUnfolding(model, boundedUntilOp, infinityVariables);
if (computeQuantile(env, consideredDimensions, *boundedUntilOp, lowerBoundedDimensions, satCostLimits, unsatCostLimits, rewardUnfolding)) {
std::vector<ValueType> scalingFactors;
- for (auto const& dim : consideredDimensions) {
+ for (auto dim : consideredDimensions) {
scalingFactors.push_back(rewardUnfolding.getDimension(dim).scalingFactor);
}
std::pair<CostLimitClosure, std::vector<ValueType>> 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<ValueType> 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<ValueType> 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<typename ValueType>
storm::storage::SparseMatrix<ValueType> FlexibleSparseMatrix<ValueType>::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<uint_fast64_t> oldToNewColumnIndexMapping(getColumnCount(), getColumnCount());
uint_fast64_t newColumnIndex = 0;
- for (auto const& oldColumnIndex : columnConstraint) {
+ for (auto oldColumnIndex : columnConstraint) {
oldToNewColumnIndexMapping[oldColumnIndex] = newColumnIndex++;
}
storm::storage::SparseMatrixBuilder<ValueType> 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 <typename ValueType>
bool Scheduler<ValueType>::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<typename ValueType>
storm::storage::BitVector SparseMatrix<ValueType>::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<ValueType> SparseMatrix<ValueType>::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<ValueType> 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<Halfspace<ValueType>> 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<Point> 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<ValueType>();
}
@@ -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<ValueType>());
}
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<uint64_t> (model.getNumberOfStates() * memoryStateCount, std::numeric_limits<uint64_t>::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<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::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<ValueType> 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<ValueType> 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<ValueType> choice = scheduler->getChoice(modelState, memoryState);
@@ -273,7 +273,7 @@ namespace storm {
storm::storage::SparseMatrixBuilder<ValueType> 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<storm::storage::SparseMatrix<RewardValueType>> transitionRewards;
if (origRewardModel.hasTransitionRewards()) {
storm::storage::SparseMatrixBuilder<RewardValueType> builder(choiceCount, stateCount, 0, true);
- for (auto const& row : resultData.keptChoices) {
+ for (auto row : resultData.keptChoices) {
boost::optional<typename SparseModelType::ValueType> 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<uint_fast64_t> 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<T> const& transitionMatrix, storm::storage::Scheduler<T>& scheduler) {
std::vector<uint_fast64_t> 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<T> const& transitionMatrix, storm::storage::Scheduler<T>& scheduler) {
std::vector<uint_fast64_t> 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<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<T>& scheduler, boost::optional<storm::storage::BitVector> 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);