diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h index be0729729..29ab6c613 100644 --- a/src/adapters/SymbolicModelAdapter.h +++ b/src/adapters/SymbolicModelAdapter.h @@ -157,7 +157,6 @@ private: for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); - bool initialValue = booleanVariable.getInitialValue()->getValueAsBool(nullptr); *initialStates *= *cuddUtility->getConstantEncoding(1, variableToRowDecisionDiagramVariableMap[booleanVariable.getName()]); } for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { @@ -187,7 +186,6 @@ private: } bool changed; - int iter = 0; do { changed = false; *newReachableStates = *reachableStates * *systemAdd01; diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 027369182..de9c6b057 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -169,7 +169,6 @@ namespace storm { * @return A mapping from labels to variable indices. */ static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { - int error = 0; std::stringstream variableNameBuffer; std::unordered_map resultingMap; for (auto const& label : relevantLabels) { @@ -190,7 +189,6 @@ namespace storm { * @return A mapping from states to a list of choice variable indices. */ static std::pair>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map> resultingMap; @@ -219,7 +217,6 @@ namespace storm { * @return A mapping from initial states to choice variable indices. */ static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -245,7 +242,6 @@ namespace storm { * @return A mapping from states to the index of the corresponding probability variables. */ static std::pair, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -269,7 +265,6 @@ namespace storm { * @return The index of the variable for the probability of the virtual initial state. */ static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& solver, bool maximizeProbability = false) { - int error = 0; std::stringstream variableNameBuffer; variableNameBuffer << "pinit"; @@ -285,7 +280,6 @@ namespace storm { * @return A mapping from problematic states to the index of the corresponding variables. */ static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -329,7 +323,6 @@ namespace storm { * @return A mapping from problematic choices to the index of the corresponding variables. */ static std::pair, uint_fast64_t, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { - int error = 0; std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map, uint_fast64_t, PairHash> resultingMap; @@ -539,7 +532,6 @@ namespace storm { */ static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; - int error = 0; for (auto state : stateInformation.relevantStates) { std::vector coefficients; std::vector variables; diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 1f9250c10..22b6ab13f 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -123,7 +123,7 @@ namespace storm { } // Then compute how many rows the new matrix is going to have. - uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; + //uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates() + 1); diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index e343526f2..e122fcb16 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -110,8 +110,6 @@ namespace storm { glp_set_row_name(this->lp, nextConstraintIndex, name.c_str()); // Determine the type of the constraint and add it properly. - bool isUpperBound = boundType == LESS || boundType == LESS_EQUAL; - bool isStrict = boundType == LESS || boundType == GREATER; switch (boundType) { case LESS: glp_set_row_bnds(this->lp, nextConstraintIndex, GLP_UP, 0, rightHandSideValue - storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index f81f4267a..c7ef52247 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -152,7 +152,6 @@ namespace storm { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. - std::vector* swap = nullptr; std::vector* currentX = &x; bool multiplyResultProvided = true; diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp index 29829f535..1b408d740 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp +++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp @@ -59,7 +59,6 @@ namespace storm { newX = new std::vector(x.size()); xMemoryProvided = false; } - std::vector* swap = nullptr; uint_fast64_t iterations = 0; bool converged = false; diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index d55b4e2e5..d26ad0344 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -106,7 +106,6 @@ namespace storm { void NativeLinearEquationSolver::performMatrixVectorMultiplication(storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. - std::vector* swap = nullptr; std::vector* currentX = &x; bool multiplyResultProvided = true; diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.cpp b/src/solver/NativeNondeterministicLinearEquationSolver.cpp index 5dc25f2c1..7f88258f1 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.cpp +++ b/src/solver/NativeNondeterministicLinearEquationSolver.cpp @@ -54,7 +54,6 @@ namespace storm { newX = new std::vector(x.size()); xMemoryProvided = false; } - std::vector* swap = nullptr; uint_fast64_t iterations = 0; bool converged = false; diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index b4b282e0b..6907c45be 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -200,7 +200,6 @@ namespace storm { } BitVector& BitVector::operator&=(BitVector const& other) { - uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size()); std::vector::iterator it = bucketVector.begin(); for (std::vector::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) { @@ -224,7 +223,6 @@ namespace storm { } BitVector& BitVector::operator|=(BitVector const& other) { - uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size()); std::vector::iterator it = bucketVector.begin(); for (std::vector::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) { diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 0f8d0acfa..6955ec053 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -743,7 +743,6 @@ namespace storm { const_iterator it = this->begin(); const_iterator ite; typename std::vector::const_iterator rowIterator = rowIndications.begin(); - typename std::vector::const_iterator rowIteratorEnd = rowIndications.end(); typename std::vector::iterator resultIterator = result.begin(); typename std::vector::iterator resultIteratorEnd = result.end(); diff --git a/src/utility/vector.h b/src/utility/vector.h index dd3bb2a1f..82913a902 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -94,7 +94,6 @@ namespace storm { */ template void selectVectorValues(std::vector& vector, std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGrouping, std::vector const& values) { - uint_fast64_t oldPosition = 0; for (uint_fast64_t i = 0; i < vector.size(); ++i) { vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]]; }