remove some warnings (#538)

* remove some warnings --------- Co-authored-by: Matthias Volk <[email protected]> Co-authored-by: Matthias Volk <[email protected]>
moves-rwth · May 24, 2024 · c066774 · c066774
1 parent f8d1340
commit c066774
Show file tree

Hide file tree

Showing 26 changed files with 94 additions and 83 deletions.
diff --git a/src/storm-gamebased-ar/abstraction/MenuGameRefiner.cpp b/src/storm-gamebased-ar/abstraction/MenuGameRefiner.cpp
@@ -1145,11 +1145,11 @@ struct ExplicitDijkstraQueueElementLess {
 template<typename ValueType>
 void performDijkstraStep(std::set<ExplicitDijkstraQueueElement<ValueType>, ExplicitDijkstraQueueElementLess<ValueType>>& dijkstraQueue,
                          bool probabilityDistances, std::vector<ValueType>& distances, std::vector<std::pair<uint64_t, uint64_t>>& predecessors,
-                         bool generatePredecessors, bool lower, uint64_t currentState, ValueType const& currentDistance, bool isPivotState,
-                         storm::storage::ExplicitGameStrategyPair const& strategyPair, storm::storage::ExplicitGameStrategyPair const& otherStrategyPair,
-                         std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Grouping,
-                         storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& targetStates,
-                         storm::storage::BitVector const& relevantStates) {
+                         bool generatePredecessors, bool lower, uint64_t currentState, ValueType const& currentDistance, [[maybe_unused]] bool isPivotState,
+                         storm::storage::ExplicitGameStrategyPair const& strategyPair,
+                         [[maybe_unused]] storm::storage::ExplicitGameStrategyPair const& otherStrategyPair, std::vector<uint64_t> const& player1Labeling,
+                         [[maybe_unused]] std::vector<uint64_t> const& player2Grouping, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
+                         [[maybe_unused]] storm::storage::BitVector const& targetStates, storm::storage::BitVector const& relevantStates) {
     if (strategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
         uint64_t player2Successor = strategyPair.getPlayer1Strategy().getChoice(currentState);
         uint64_t player2Choice = strategyPair.getPlayer2Strategy().getChoice(player2Successor);
@@ -1352,10 +1352,11 @@ boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePr
 
 template<storm::dd::DdType Type, typename ValueType>
 bool MenuGameRefiner<Type, ValueType>::refine(storm::gbar::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Odd const& odd,
-                                              storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping,
-                                              std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling,
-                                              storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates,
-                                              storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult,
+                                              storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
+                                              [[maybe_unused]] std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling,
+                                              std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates,
+                                              storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates,
+                                              ExplicitQualitativeGameResultMinMax const& qualitativeResult,
                                               storage::ExplicitGameStrategyPair const& minStrategyPair,
                                               storage::ExplicitGameStrategyPair const& maxStrategyPair) const {
     STORM_LOG_ASSERT(constraintStates.full(), "Constraint states are ignored. Likely buggy.");
@@ -1439,10 +1440,10 @@ bool MenuGameRefiner<Type, ValueType>::refine(storm::gbar::abstraction::MenuGame
 
 template<storm::dd::DdType Type, typename ValueType>
 bool MenuGameRefiner<Type, ValueType>::refine(storm::gbar::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Odd const& odd,
-                                              storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping,
-                                              std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling,
-                                              storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates,
-                                              storm::storage::BitVector const& targetStates,
+                                              storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
+                                              [[maybe_unused]] std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling,
+                                              std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates,
+                                              storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates,
                                               ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult,
                                               storage::ExplicitGameStrategyPair const& minStrategyPair,
                                               storage::ExplicitGameStrategyPair const& maxStrategyPair) const {

diff --git a/src/storm-pomdp/analysis/IterativePolicySearch.cpp b/src/storm-pomdp/analysis/IterativePolicySearch.cpp
@@ -417,10 +417,14 @@ bool IterativePolicySearch<ValueType>::analyze(uint64_t k, storm::storage::BitVe
 
         updated.set(observation);
     }
+
+#ifndef NDEBUG
     for (auto const& state : targetStates) {
         STORM_LOG_ASSERT(winningRegion.isWinning(pomdp.getObservation(state), getOffsetFromObservation(state, pomdp.getObservation(state))),
                          "Target state " << state << " , observation " << pomdp.getObservation(state) << " is not reflected as winning.");
     }
+#endif
+
     stats.winningRegionUpdatesTimer.stop();
 
     uint64_t maximalNrActions = 0;

diff --git a/src/storm/adapters/SpotAdapter.h b/src/storm/adapters/SpotAdapter.h
@@ -0,0 +1,24 @@
+#pragma once
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_SPOT
+#if defined(__clang__)
+#pragma clang diagnostic push
+#elif defined(__GNUC__)
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Wdeprecated-declarations"
+#endif
+
+#include "spot/tl/formula.hh"
+#include "spot/tl/parse.hh"
+#include "spot/twaalgos/dot.hh"
+#include "spot/twaalgos/hoa.hh"
+#include "spot/twaalgos/totgba.hh"
+#include "spot/twaalgos/translate.hh"
+
+#if defined(__clang__)
+#pragma clang diagnostic pop
+#elif defined(__GNUC__)
+#pragma GCC diagnostic pop
+#endif
+#endif
diff --git a/src/storm/automata/HOAConsumerDA.h b/src/storm/automata/HOAConsumerDA.h
@@ -168,7 +168,7 @@ class HOAConsumerDA : public HOAConsumerDAHeader {
      * Called by the parser to notify the consumer that the definition for state `stateId`
      * has ended [multiple].
      */
-    virtual void notifyEndOfState(unsigned int stateId) {
+    virtual void notifyEndOfState(unsigned int /*stateId*/) {
         helper->endOfState();
     }
 

diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp
@@ -1,4 +1,5 @@
 #include "storm/automata/LTL2DeterministicAutomaton.h"
+#include "storm/adapters/SpotAdapter.h"
 #include "storm/automata/DeterministicAutomaton.h"
 
 #include "storm/exceptions/ExpressionEvaluationException.h"
@@ -9,14 +10,6 @@
 
 #include <sys/wait.h>
 
-#ifdef STORM_HAVE_SPOT
-#include "spot/tl/formula.hh"
-#include "spot/tl/parse.hh"
-#include "spot/twaalgos/hoa.hh"
-#include "spot/twaalgos/totgba.hh"
-#include "spot/twaalgos/translate.hh"
-#endif
-
 namespace storm {
 namespace automata {
 
@@ -58,6 +51,8 @@ std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2daSpot(s
     return da;
 
 #else
+    (void)f;
+    (void)dnf;
     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Spot support.");
 #endif
 }

diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -179,7 +179,7 @@ void DdJaniModelBuilder<Type, ValueType>::Options::addLabel(std::string const& l
 template<storm::dd::DdType Type, typename ValueType>
 class ParameterCreator {
    public:
-    void create(storm::jani::Model const& model, storm::adapters::AddExpressionAdapter<Type, ValueType>& rowExpressionAdapter) {
+    void create(storm::jani::Model const& /*model*/, storm::adapters::AddExpressionAdapter<Type, ValueType>& /*rowExpressionAdapter*/) {
         // Intentionally left empty: no support for parameters for this data type.
     }
 

diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp
@@ -36,7 +36,7 @@ namespace builder {
 template<storm::dd::DdType Type, typename ValueType>
 class ParameterCreator {
    public:
-    void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter<Type, ValueType>& rowExpressionAdapter) {
+    void create(storm::prism::Program const& /*program*/, storm::adapters::AddExpressionAdapter<Type, ValueType>& /*rowExpressionAdapter*/) {
         // Intentionally left empty: no support for parameters for this data type.
     }
 

diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -1389,7 +1389,7 @@ std::shared_ptr<storm::storage::sparse::ChoiceOrigins> JaniNextStateGenerator<Va
 }
 
 template<typename ValueType, typename StateType>
-storm::storage::BitVector JaniNextStateGenerator<ValueType, StateType>::evaluateObservationLabels(CompressedState const& state) const {
+storm::storage::BitVector JaniNextStateGenerator<ValueType, StateType>::evaluateObservationLabels(CompressedState const& /*state*/) const {
     STORM_LOG_WARN("There are no observation labels in JANI currenty");
     return storm::storage::BitVector(0);
 }

diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp
@@ -315,7 +315,7 @@ void NextStateGenerator<ValueType, StateType>::extendStateInformation(storm::jso
 
 template<typename ValueType, typename StateType>
 std::shared_ptr<storm::storage::sparse::ChoiceOrigins> NextStateGenerator<ValueType, StateType>::generateChoiceOrigins(
-    std::vector<boost::any>& dataForChoiceOrigins) const {
+    std::vector<boost::any>& /*dataForChoiceOrigins*/) const {
     STORM_LOG_ERROR_COND(!options.isBuildChoiceOriginsSet(), "Generating choice origins is not supported for the considered model format.");
     return nullptr;
 }
@@ -335,7 +335,7 @@ std::map<std::string, storm::storage::PlayerIndex> NextStateGenerator<ValueType,
 }
 
 template<typename ValueType, typename StateType>
-void NextStateGenerator<ValueType, StateType>::remapStateIds(std::function<StateType(StateType const&)> const& remapping) {
+void NextStateGenerator<ValueType, StateType>::remapStateIds(std::function<StateType(StateType const&)> const& /*remapping*/) {
     if (overlappingGuardStates != boost::none) {
         STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
                         "Remapping of Ids during model building is not supported for overlapping guard statements.");

diff --git a/src/storm/generator/TransientVariableInformation.cpp b/src/storm/generator/TransientVariableInformation.cpp
@@ -40,7 +40,7 @@ TransientVariableData<VariableType>::TransientVariableData(storm::expressions::V
 
 template<typename VariableType>
 TransientVariableData<VariableType>::TransientVariableData(storm::expressions::Variable const& variable, VariableType const& defaultValue, bool global)
-    : variable(variable), defaultValue(defaultValue) {
+    : variable(variable), defaultValue(defaultValue), global(global) {
     // Intentionally left empty.
 }
 

diff --git a/src/storm/logic/ComparisonType.h b/src/storm/logic/ComparisonType.h
@@ -29,6 +29,8 @@ inline ComparisonType invert(ComparisonType t) {
             return ComparisonType::Less;
     }
     STORM_LOG_ASSERT(false, "Unknown ComparisonType");
+    // Wrong, but this code should not be reachable. Still, GCC issues a warning.
+    return t;
 }
 
 inline ComparisonType invertPreserveStrictness(ComparisonType t) {
@@ -43,6 +45,8 @@ inline ComparisonType invertPreserveStrictness(ComparisonType t) {
             return ComparisonType::LessEqual;
     }
     STORM_LOG_ASSERT(false, "Unknown ComparisonType");
+    // Wrong, but this code should not be reachable. Still, GCC issues a warning.
+    return t;
 }
 
 std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);

diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp
@@ -36,7 +36,6 @@
 #include "storm/storage/dd/Bdd.h"
 
 #include <boost/core/typeinfo.hpp>
-#include <storm/models/symbolic/MarkovAutomaton.h>
 
 namespace storm {
 namespace modelchecker {

diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -266,7 +266,7 @@ std::vector<ValueType> SparseCtmcCslHelper::computeBoundedUntilProbabilities(
 }
 
 template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
-std::vector<ValueType> SparseCtmcCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
+std::vector<ValueType> SparseCtmcCslHelper::computeBoundedUntilProbabilities(Environment const&, storm::solver::SolveGoal<ValueType>&&,
                                                                              storm::storage::SparseMatrix<ValueType> const&,
                                                                              storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&,
                                                                              storm::storage::BitVector const&, std::vector<ValueType> const&, bool, double,
@@ -363,7 +363,7 @@ std::vector<ValueType> SparseCtmcCslHelper::computeInstantaneousRewards(Environm
 }
 
 template<typename ValueType, typename RewardModelType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
-std::vector<ValueType> SparseCtmcCslHelper::computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
+std::vector<ValueType> SparseCtmcCslHelper::computeInstantaneousRewards(Environment const&, storm::solver::SolveGoal<ValueType>&&,
                                                                         storm::storage::SparseMatrix<ValueType> const&, std::vector<ValueType> const&,
                                                                         RewardModelType const&, double) {
     STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing instantaneous rewards is unsupported for this value type.");
@@ -436,7 +436,7 @@ std::vector<ValueType> SparseCtmcCslHelper::computeCumulativeRewards(Environment
 }
 
 template<typename ValueType, typename RewardModelType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
-std::vector<ValueType> SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal,
+std::vector<ValueType> SparseCtmcCslHelper::computeCumulativeRewards(Environment const&, storm::solver::SolveGoal<ValueType>&&,
                                                                      storm::storage::SparseMatrix<ValueType> const&, std::vector<ValueType> const&,
                                                                      RewardModelType const&, double) {
     STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing cumulative rewards is unsupported for this value type.");

diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -714,10 +714,11 @@ std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbab
 }
 
 template<typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
-std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(
-    Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
-    std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates,
-    storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair) {
+std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const&, storm::solver::SolveGoal<ValueType>&&,
+                                                                                        storm::storage::SparseMatrix<ValueType> const&,
+                                                                                        std::vector<ValueType> const&, storm::storage::BitVector const&,
+                                                                                        storm::storage::BitVector const&, storm::storage::BitVector const&,
+                                                                                        std::pair<double, double> const&) {
     STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type.");
 }
 

diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp
@@ -15,9 +15,7 @@
 
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 
-namespace storm {
-namespace modelchecker {
-namespace helper {
+namespace storm::modelchecker::helper {
 
 template<typename ValueType>
 SparseDeterministicStepBoundedHorizonHelper<ValueType>::SparseDeterministicStepBoundedHorizonHelper() {
@@ -85,8 +83,4 @@ std::vector<ValueType> SparseDeterministicStepBoundedHorizonHelper<ValueType>::c
 template class SparseDeterministicStepBoundedHorizonHelper<double>;
 template class SparseDeterministicStepBoundedHorizonHelper<storm::RationalNumber>;
 template class SparseDeterministicStepBoundedHorizonHelper<storm::RationalFunction>;
-}  // namespace helper
-}  // namespace modelchecker
-}  // namespace storm
-// Created by Sebastian Junges on 8/20/20.
-//
+}  // namespace storm::modelchecker::helper
diff --git a/...checker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp b/...checker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp
@@ -242,7 +242,7 @@ void SparseDeterministicVisitingTimesHelper<ValueType>::createNonBsccStateVector
 
 template<>
 std::vector<storm::RationalFunction> SparseDeterministicVisitingTimesHelper<storm::RationalFunction>::computeUpperBounds(
-    storm::storage::BitVector const& stateSetAsBitvector) const {
+    storm::storage::BitVector const& /*stateSetAsBitvector*/) const {
     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
                     "Computing upper bounds for expected visiting times over rational functions is not supported.");
 }

diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
@@ -120,7 +120,8 @@ std::pair<bool, ValueType> SparseDeterministicInfiniteHorizonHelper<ValueType>::
 
 template<>
 storm::RationalFunction SparseDeterministicInfiniteHorizonHelper<storm::RationalFunction>::computeLraForBsccVi(
-    Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, storm::storage::StronglyConnectedComponent const& bscc) {
+    Environment const& /*env*/, ValueGetter const& /*stateValueGetter*/, ValueGetter const& /*actionValueGetter*/,
+    storm::storage::StronglyConnectedComponent const& /*bscc*/) {
     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The requested Method for LRA computation is not supported for parametric models.");
 }
 template<typename ValueType>
@@ -645,8 +646,8 @@ std::vector<ValueType> computeUpperBoundsForExpectedVisitingTimes(storm::storage
 }
 
 template<>
-std::vector<storm::RationalFunction> computeUpperBoundsForExpectedVisitingTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& nonBsccMatrix,
-                                                                                std::vector<storm::RationalFunction> const& toBsccProbabilities) {
+std::vector<storm::RationalFunction> computeUpperBoundsForExpectedVisitingTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& /*nonBsccMatrix*/,
+                                                                                std::vector<storm::RationalFunction> const& /*toBsccProbabilities*/) {
     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
                     "Computing upper bounds for expected visiting times over rational functions is not supported.");
 }

diff --git a/src/storm/modelchecker/lexicographic/spotHelper/spotProduct.cpp b/src/storm/modelchecker/lexicographic/spotHelper/spotProduct.cpp
@@ -7,14 +7,7 @@
 #include "storm/logic/Formulas.h"
 #include "storm/models/sparse/Mdp.h"
 
-#ifdef STORM_HAVE_SPOT
-#include "spot/tl/formula.hh"
-#include "spot/tl/parse.hh"
-#include "spot/twaalgos/dot.hh"
-#include "spot/twaalgos/hoa.hh"
-#include "spot/twaalgos/totgba.hh"
-#include "spot/twaalgos/translate.hh"
-#endif
+#include "storm/adapters/SpotAdapter.h"
 
 namespace storm::modelchecker::helper::lexicographic::spothelper {