From b258f1e52deaaf480cb8b548124b283c0827874c Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 22 Dec 2016 15:34:12 +0100 Subject: [PATCH] some more warnings gone --- .../modelchecker/abstraction/GameBasedMdpModelChecker.cpp | 2 +- .../modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp | 2 +- .../modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp | 2 +- src/storm/utility/graph.cpp | 8 ++++---- src/storm/utility/graph.h | 2 +- src/storm/utility/solver.cpp | 2 ++ src/test/utility/GraphTest.cpp | 2 +- 7 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 8249fe7d8..a0f9e2999 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -539,7 +539,7 @@ namespace storm { // (2) min/min: compute prob1 using the MDP functions storm::dd::Bdd candidates = game.getReachableStates() && !result.prob0Min.player1States; - storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(game, transitionMatrixBdd, constraintStates, previousQualitativeResult ? previousQualitativeResult.get().prob1Min.player1States : targetStates, candidates); + storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(game, transitionMatrixBdd, previousQualitativeResult ? previousQualitativeResult.get().prob1Min.player1States : targetStates, candidates); // (3) min/min: compute prob1 using the game functions result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MinMinMdp)); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 58c0d09d3..d9cb27a49 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -214,7 +214,7 @@ namespace storm { if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } else { - infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); + infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } infinityStates = !infinityStates && model.getReachableStates(); storm::dd::Bdd maybeStates = (!targetStates && !infinityStates) && model.getReachableStates(); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index be156452d..34ff9c711 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -170,7 +170,7 @@ namespace storm { if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } else { - infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); + infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } infinityStates = !infinityStates && model.getReachableStates(); diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index c821dc7e9..592167496 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -797,7 +797,7 @@ namespace storm { } template - storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { + storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A) { // Initialize environment for backward search. storm::dd::DdManager const& manager = model.getManager(); storm::dd::Bdd lastIterationStates = manager.getBddZero(); @@ -872,7 +872,7 @@ namespace storm { std::pair, storm::dd::Bdd> result; storm::dd::Bdd transitionMatrix = model.getTransitionMatrix().notZero(); result.first = performProb0E(model, transitionMatrix, phiStates, psiStates); - result.second = performProb1A(model, transitionMatrix, phiStates, psiStates, !result.first && model.getReachableStates()); + result.second = performProb1A(model, transitionMatrix, psiStates, !result.first && model.getReachableStates()); return result; } @@ -1399,7 +1399,7 @@ namespace storm { template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); @@ -1431,7 +1431,7 @@ namespace storm { template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 4bbc90042..7f51b20f6 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -482,7 +482,7 @@ namespace storm { * @return A BDD representing all such states. */ template - storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); + storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); /*! * Computes the set of states for which there exists a scheduler that achieves probability one of satisfying diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 8bc28e259..8ea29dbb8 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -55,6 +55,7 @@ namespace storm { case storm::solver::LpSolverType::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); case storm::solver::LpSolverType::Glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); } + return nullptr; } std::unique_ptr LpSolverFactory::create(std::string const& name) const { @@ -80,6 +81,7 @@ namespace storm { case storm::solver::SmtSolverType::Z3: return std::unique_ptr(new storm::solver::Z3SmtSolver(manager)); case storm::solver::SmtSolverType::Mathsat: return std::unique_ptr(new storm::solver::MathsatSmtSolver(manager)); } + return nullptr; } std::unique_ptr Z3SmtSolverFactory::create(storm::expressions::ExpressionManager& manager) const { diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index a9357e42f..1cac1d5cc 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -229,7 +229,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy());