From 16ea224b6aef6ea6b5edc8464144e80e5e61be9e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 1 Oct 2015 12:37:46 +0200
Subject: [PATCH] added flag that indicates which interval bound is to be
 taken. added xerces to the gitignore

Former-commit-id: ee85062515010b1fe59d74c9efb86fe1dcdb0648
---
 .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<typename ValueType>
-            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+            std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<storm::Interval> 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<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 
 #ifdef STORM_HAVE_CARL
-                static std::vector<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
+                static std::vector<ValueType> computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::Interval> const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 #endif
                 
                 static std::vector<ValueType> computeLongRunAverage(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);