From d06c92c10aa7118944415607b0b5b15fb973da8b Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 1 Oct 2015 13:51:20 +0200 Subject: [PATCH] Revert "Revert "added flag that indicates which interval bound is to be taken. added xerces to the gitignore"" This reverts commit dfd2cda38079b42f7d9fb8cc582790df09791fd3 [formerly 4be9f6f8c80c71f452171a496123a66dc159f772]. Former-commit-id: 4510017c6a13d61827351b0b43ba8c01ff98637d --- .gitignore | 1 + src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 4 ++-- src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.gitignore b/.gitignore index 03286848f..bd4e15887 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,7 @@ resources/3rdparty/gtest-1.7.0/ resources/3rdparty/eigen/ resources/3rdparty/gmm-4.2/ resources/3rdparty/cudd-2.5.0/ +resources/3rdparty/xercesc-3.1.2/ #Visual Studio files *.[Oo]bj *.user diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 71a8f81e2..f6cf8ab23 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -192,7 +192,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template - std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Only compute the result if the reward model is not empty. STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); return computeReachabilityRewardsHelper(dir, transitionMatrix, backwardTransitions, \ @@ -201,7 +201,7 @@ namespace storm { result.reserve(rowCount); std::vector subIntervalVector = intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); for (auto const& interval : subIntervalVector) { - result.push_back(dir == OptimizationDirection::Minimize ? interval.lower() : interval.upper()); + result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper()); } return result; }, \ diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index d9e168da8..da9867af6 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -48,7 +48,7 @@ namespace storm { static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); #ifdef STORM_HAVE_CARL - static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); #endif static std::vector computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory);