From eac273506891b17f101b7853cdb8818b0377b6bc Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 22 Dec 2016 14:39:18 +0100 Subject: [PATCH] fixed more warnings --- .../jit/ExplicitJitJaniModelBuilder.cpp | 2 +- .../permissivesched/PermissiveSchedulers.cpp | 4 ++-- src/storm/solver/SmtSolver.cpp | 4 ++-- src/storm/solver/SmtlibSmtSolver.cpp | 12 ++++++------ .../storage/dd/sylvan/InternalSylvanAdd.cpp | 2 +- .../VariableSetPredicateSplitter.cpp | 2 +- src/storm/storage/jani/JSONExporter.cpp | 2 +- src/storm/utility/graph.cpp | 18 +----------------- src/storm/utility/graph.h | 16 ---------------- src/storm/utility/stateelimination.cpp | 4 ++-- 10 files changed, 17 insertions(+), 49 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 7c215dfbe..b3edd7e73 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -2405,7 +2405,7 @@ namespace storm { } template - std::vector getParameters(storm::jani::Model const&, std::shared_ptr>> cache) { + std::vector getParameters(storm::jani::Model const&, std::shared_ptr>>) { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "This function must not be called for this type."); } diff --git a/src/storm/permissivesched/PermissiveSchedulers.cpp b/src/storm/permissivesched/PermissiveSchedulers.cpp index 0ce53c61d..1a7e7061b 100644 --- a/src/storm/permissivesched/PermissiveSchedulers.cpp +++ b/src/storm/permissivesched/PermissiveSchedulers.cpp @@ -21,7 +21,7 @@ namespace storm { auto backwardTransitions = mdp.getBackwardTransitions(); storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); - storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(mdp,backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); + storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); MilpPermissiveSchedulerComputation> comp(*solver, mdp, goalstates, sinkstates); @@ -48,7 +48,7 @@ namespace storm { auto backwardTransitions = mdp.getBackwardTransitions(); storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); - storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); + storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); std::shared_ptr expressionManager = std::make_shared(); auto solver = storm::utility::solver::getSmtSolver(*expressionManager); diff --git a/src/storm/solver/SmtSolver.cpp b/src/storm/solver/SmtSolver.cpp index b9e2605dc..16c16a104 100644 --- a/src/storm/solver/SmtSolver.cpp +++ b/src/storm/solver/SmtSolver.cpp @@ -68,7 +68,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of unsatisfiable cores."); } - void SmtSolver::setInterpolationGroup(uint_fast64_t group) { + void SmtSolver::setInterpolationGroup(uint_fast64_t) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); } @@ -84,7 +84,7 @@ namespace storm { return manager; } - bool SmtSolver::setTimeout(uint_fast64_t milliseconds) { + bool SmtSolver::setTimeout(uint_fast64_t) { return false; } diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index cf894d310..e6295993e 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -27,15 +27,15 @@ namespace storm { // Intentionally left empty. } - bool SmtlibSmtSolver::SmtlibModelReference::getBooleanValue(storm::expressions::Variable const& variable) const { + bool SmtlibSmtSolver::SmtlibModelReference::getBooleanValue(storm::expressions::Variable const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - int_fast64_t SmtlibSmtSolver::SmtlibModelReference::getIntegerValue(storm::expressions::Variable const& variable) const { + int_fast64_t SmtlibSmtSolver::SmtlibModelReference::getIntegerValue(storm::expressions::Variable const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - double SmtlibSmtSolver::SmtlibModelReference::getRationalValue(storm::expressions::Variable const& variable) const { + double SmtlibSmtSolver::SmtlibModelReference::getRationalValue(storm::expressions::Variable const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } @@ -82,7 +82,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - void SmtlibSmtSolver::add(storm::expressions::Expression const& assertion) { + void SmtlibSmtSolver::add(storm::expressions::Expression const&) { STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions"); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } @@ -172,13 +172,13 @@ namespace storm { #endif } - SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::set const& assumptions) { + SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::set const&) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } #ifndef WINDOWS - SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { + SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::initializer_list const&) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } #endif diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 4a23680d8..eecfe55bb 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -446,7 +446,7 @@ namespace storm { } template - InternalAdd InternalAdd::constrain(InternalAdd const& constraint) const { + InternalAdd InternalAdd::constrain(InternalAdd const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } diff --git a/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp index 3e3da7650..ca15221af 100644 --- a/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp +++ b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp @@ -103,7 +103,7 @@ namespace storm { return boost::any(); } - boost::any VariableSetPredicateSplitter::visit(BinaryNumericalFunctionExpression const& expression, boost::any const&) { + boost::any VariableSetPredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) { return boost::any(); } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index ea6de1ba2..491605c35 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -262,7 +262,7 @@ namespace storm { } - boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const { + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const&, boost::any const&) const { // modernjson::json opDecl; // if(f.()) { // auto bound = f.getBound(); diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index f219cd9a5..c821dc7e9 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -193,7 +193,7 @@ namespace storm { } template - storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { + storm::storage::BitVector performProb1(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const&, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0); statesWithProbability1.complement(); return statesWithProbability1; @@ -488,11 +488,6 @@ namespace storm { return statesWithProbability0; } - template - storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - return performProb0A(backwardTransitions, phiStates, psiStates); - } - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { size_t numberOfStates = phiStates.size(); @@ -1187,11 +1182,6 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); -#ifdef STORM_HAVE_CARL - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); -#endif - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1255,8 +1245,6 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1313,8 +1301,6 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1364,8 +1350,6 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 63b7ead8b..4bbc90042 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -304,22 +304,6 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - /*! - * Computes the sets of states that have probability 0 of satisfying phi until psi under all - * possible resolutions of non-determinism in a non-deterministic model. Stated differently, - * this means that these states have probability 0 of satisfying phi until psi even if the - * scheduler tries to maximize this probability. - * - * @param model The model whose graph structure to search. - * @param backwardTransitions The reversed transition relation of the model. - * @param phiStates The set of all states satisfying phi. - * @param psiStates The set of all states satisfying psi. - * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. - * @param maximalSteps The maximal number of steps to reach the psi states. - * @return A bit vector that represents all states with probability 0. - */ - template - storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; /*! * Computes the sets of states that have probability 1 of satisfying phi until psi under at least * one possible resolution of non-determinism in a non-deterministic model. Stated differently, diff --git a/src/storm/utility/stateelimination.cpp b/src/storm/utility/stateelimination.cpp index 77178b8f1..70804fabb 100644 --- a/src/storm/utility/stateelimination.cpp +++ b/src/storm/utility/stateelimination.cpp @@ -49,7 +49,7 @@ namespace storm { } template - uint_fast64_t estimateComplexity(ValueType const& value) { + uint_fast64_t estimateComplexity(ValueType const&) { return 1; } @@ -91,7 +91,7 @@ namespace storm { } template - uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const& oneStepProbabilities) { + uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector const&) { return backwardTransitions.getRow(state).size() * transitionMatrix.getRow(state).size(); }