From 3714fc3bf2a40d740ca8cb9f7ec86ff576ead757 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 11:44:31 +0200 Subject: [PATCH 01/13] MinMaxSolverEnvironment: Removed unused method declarations. --- src/storm/environment/solver/MinMaxSolverEnvironment.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index 3f54f0fa9..b0a19d8c4 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -25,8 +25,6 @@ namespace storm { void setRelativeTerminationCriterion(bool value); storm::solver::MultiplicationStyle const& getMultiplicationStyle() const; void setMultiplicationStyle(storm::solver::MultiplicationStyle value); - bool isForceBoundsSet() const; - void setForceBounds(bool value); bool isSymmetricUpdatesSet() const; void setSymmetricUpdates(bool value); @@ -37,7 +35,6 @@ namespace storm { storm::RationalNumber precision; bool considerRelativeTerminationCriterion; storm::solver::MultiplicationStyle multiplicationStyle; - bool forceBounds; bool symmetricUpdates; }; } From 3836fd42c00c95c5b37641f90e952f34852b52c6 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 11:44:51 +0200 Subject: [PATCH 02/13] utility/vector: Added hasZeroEntry and hasInfinityEntry --- src/storm/utility/vector.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 53e89cacc..153f74a36 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -1155,6 +1155,16 @@ namespace storm { bool hasNonZeroEntry(std::vector const& v){ return std::any_of(v.begin(), v.end(), [](T value){return !storm::utility::isZero(value);}); } + + template + bool hasZeroEntry(std::vector const& v){ + return std::any_of(v.begin(), v.end(), [](T value){return storm::utility::isZero(value);}); + } + + template + bool hasInfinityEntry(std::vector const& v){ + return std::any_of(v.begin(), v.end(), [](T value){return storm::utility::isInfinity(value);}); + } inline std::set getVariables(std::vector const& vector) { std::set result; From 60ae342677d2167263fa9f599b5bd78620aaf0b6 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 2 May 2019 15:29:11 +0200 Subject: [PATCH 03/13] NativePolytope: Fixed affineTransformation of the universal polytope. --- src/storm/storage/geometry/NativePolytope.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index 2d35368d1..4e634f20a 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -285,7 +285,6 @@ namespace storm { template std::shared_ptr> NativePolytope::affineTransformation(std::vector const& matrix, Point const& vector) const { STORM_LOG_THROW(!matrix.empty(), storm::exceptions::InvalidArgumentException, "Invoked affine transformation with a matrix without rows."); - StormEigen::Index rows = matrix.size(); StormEigen::Index columns = matrix.front().size(); EigenMatrix eigenMatrix(rows, columns); @@ -296,6 +295,9 @@ namespace storm { StormEigen::FullPivLU luMatrix( eigenMatrix ); STORM_LOG_THROW(luMatrix.isInvertible(), storm::exceptions::NotImplementedException, "Affine Transformation of native polytope only implemented if the transformation matrix is invertable"); + if (isUniversal()) { + return std::make_shared>(std::vector>()); + } EigenMatrix newA = A * luMatrix.inverse(); EigenVector newb = b + (newA * eigenVector); return std::make_shared>(emptyStatus, std::move(newA), std::move(newb)); From bce641319fcd2cab5f013181c7fb652ebd202397 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 2 May 2019 15:29:40 +0200 Subject: [PATCH 04/13] Fixed computation of maximal total expected rewards for MDPs with end components. --- .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 3aff389fa..d8bb7dc32 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -783,7 +783,7 @@ namespace storm { newRew0AStates.set(ecElimResult.oldToNewStateMapping[oldRew0AState]); } - return computeReachabilityRewardsHelper(env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(true), + MDPSparseModelCheckingHelperReturnType result = computeReachabilityRewardsHelper(env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(true), [&] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result; std::vector oldChoiceRewards = rewardModel.getTotalRewardVector(transitionMatrix); @@ -813,6 +813,11 @@ namespace storm { } return newChoicesWithoutReward; }); + + std::vector resultInEcQuotient = std::move(result.values); + result.values.resize(ecElimResult.oldToNewStateMapping.size()); + storm::utility::vector::selectVectorValues(result.values, ecElimResult.oldToNewStateMapping, resultInEcQuotient); + return result; } } } From 15dadf1bc305c1f785cf35c0e6461ca5eb6c3d6f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 6 May 2019 11:18:32 +0200 Subject: [PATCH 05/13] Fixed imprecision in comparison for MA --- src/storm/models/sparse/MarkovAutomaton.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index dad398ea6..9d6869d84 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -5,6 +5,7 @@ #include "storm/solver/stateelimination/StateEliminator.h" #include "storm/storage/FlexibleSparseMatrix.h" #include "storm/utility/constants.h" +#include "storm/utility/ConstantsComparator.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" #include "storm/utility/graph.h" @@ -137,6 +138,7 @@ namespace storm { this->exitRates.reserve(this->getNumberOfStates()); } + storm::utility::ConstantsComparator comparator; for (uint_fast64_t state = 0; state< this->getNumberOfStates(); ++state) { uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state]; if (this->markovianStates.get(state)) { @@ -151,13 +153,13 @@ namespace storm { ++row; } else { if (assertRates) { - STORM_LOG_THROW(storm::utility::isZero(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0."); + STORM_LOG_THROW(comparator.isZero(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0."); } else { this->exitRates.push_back(storm::utility::zero()); } } for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { - STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ")."); + STORM_LOG_THROW(comparator.isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ")."); } } } From e7454cd494fa4b17942f7d6690c07aa74170aa9b Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 6 May 2019 10:56:53 +0200 Subject: [PATCH 06/13] ArgumentValidators: added factory for UnsignedIntRangeValidatorIncluding --- src/storm/settings/ArgumentValidators.cpp | 4 ++++ src/storm/settings/ArgumentValidators.h | 1 + 2 files changed, 5 insertions(+) diff --git a/src/storm/settings/ArgumentValidators.cpp b/src/storm/settings/ArgumentValidators.cpp index 8e108b454..1e9c56db3 100644 --- a/src/storm/settings/ArgumentValidators.cpp +++ b/src/storm/settings/ArgumentValidators.cpp @@ -129,6 +129,10 @@ namespace storm { return createRangeValidatorExcluding(lowerBound, upperBound); } + std::shared_ptr> ArgumentValidatorFactory::createUnsignedRangeValidatorIncluding(uint64_t lowerBound, uint64_t upperBound) { + return createRangeValidatorIncluding(lowerBound, upperBound); + } + std::shared_ptr> ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(double lowerBound, double upperBound) { return createRangeValidatorExcluding(lowerBound, upperBound); } diff --git a/src/storm/settings/ArgumentValidators.h b/src/storm/settings/ArgumentValidators.h index 93ced6f26..6f8d73101 100644 --- a/src/storm/settings/ArgumentValidators.h +++ b/src/storm/settings/ArgumentValidators.h @@ -70,6 +70,7 @@ namespace storm { public: static std::shared_ptr> createIntegerRangeValidatorExcluding(int_fast64_t lowerBound, int_fast64_t upperBound); static std::shared_ptr> createUnsignedRangeValidatorExcluding(uint64_t lowerBound, uint64_t upperBound); + static std::shared_ptr> createUnsignedRangeValidatorIncluding(uint64_t lowerBound, uint64_t upperBound); static std::shared_ptr> createDoubleRangeValidatorExcluding(double lowerBound, double upperBound); static std::shared_ptr> createDoubleRangeValidatorIncluding(double lowerBound, double upperBound); From 4c911791e1b335c808b2a29136e566a17d5a842b Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 6 May 2019 10:58:05 +0200 Subject: [PATCH 07/13] NativePolytope: Improved clean() operation on empty polytopes. --- src/storm/storage/geometry/NativePolytope.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index 4e634f20a..f90fadb73 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -400,6 +400,9 @@ namespace storm { template std::shared_ptr> NativePolytope::clean() { + if (isEmpty()) { + return create(boost::none, {}); + } return create(boost::none, getVertices()); } From cc02383591667e4974a3b4e586cd307e965987ed Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 6 May 2019 11:01:12 +0200 Subject: [PATCH 08/13] GurobiLpSolver: Improved interface by * adding settings MIPFocus (to switch between solving strategies) and ConcurrentMIP (to spawn multiple MIP solvers) * allowing to set the desired and get the achieved gap between lower- and upper bound when solving MIP models * retrieving other solutions found during optimization. --- src/storm/settings/modules/GurobiSettings.cpp | 16 +- src/storm/settings/modules/GurobiSettings.h | 17 ++ src/storm/solver/GurobiLpSolver.cpp | 178 +++++++++++++++++- src/storm/solver/GurobiLpSolver.h | 23 ++- 4 files changed, 231 insertions(+), 3 deletions(-) diff --git a/src/storm/settings/modules/GurobiSettings.cpp b/src/storm/settings/modules/GurobiSettings.cpp index 4f35e085a..094382d27 100644 --- a/src/storm/settings/modules/GurobiSettings.cpp +++ b/src/storm/settings/modules/GurobiSettings.cpp @@ -15,6 +15,8 @@ namespace storm { const std::string GurobiSettings::integerToleranceOption = "inttol"; const std::string GurobiSettings::threadsOption = "threads"; const std::string GurobiSettings::outputOption = "output"; + const std::string GurobiSettings::mipFocusOption = "mipfocus"; + const std::string GurobiSettings::concurrentMipThreadsOption = "concurrentmip"; GurobiSettings::GurobiSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build()); @@ -22,6 +24,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, mipFocusOption, true, "The high level solution strategy used to solve MILPs.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of the strategy.").setDefaultValueUnsignedInteger(0).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorIncluding(0, 3)).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, concurrentMipThreadsOption, true, "The number of MIP solvers Gurobi spawns in parallel. Shall not be larger then the number of threads.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of parallel solvers.").setDefaultValueUnsignedInteger(1).addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedGreaterEqualValidator(1)).build()).build()); } bool GurobiSettings::isIntegerToleranceSet() const { @@ -44,11 +50,19 @@ namespace storm { return this->getOption(outputOption).getHasOptionBeenSet(); } + uint_fast64_t GurobiSettings::getMIPFocus() const { + return this->getOption(mipFocusOption).getArgumentByName("value").getValueAsUnsignedInteger(); + } + + uint_fast64_t GurobiSettings::getNumberOfConcurrentMipThreads() const { + return this->getOption(concurrentMipThreadsOption).getArgumentByName("value").getValueAsUnsignedInteger(); + } + bool GurobiSettings::check() const { if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) { STORM_LOG_WARN_COND(storm::settings::getModule().getLpSolver() == storm::solver::LpSolverType::Gurobi, "Gurobi is not selected as the preferred LP solver, so setting options for Gurobi might have no effect."); } - + STORM_LOG_WARN_COND(getNumberOfConcurrentMipThreads() <= getNumberOfThreads(), "Requested more concurrent MILP solvers then the available threads for Gurobi." ); return true; } diff --git a/src/storm/settings/modules/GurobiSettings.h b/src/storm/settings/modules/GurobiSettings.h index c91cf96f3..0151f6714 100644 --- a/src/storm/settings/modules/GurobiSettings.h +++ b/src/storm/settings/modules/GurobiSettings.h @@ -45,6 +45,21 @@ namespace storm { */ uint_fast64_t getNumberOfThreads() const; + /*! + * Retrieves the selected high-level solution strategy for MILPs. + * + * @return The high-level solution strategy. + */ + uint_fast64_t getMIPFocus() const; + + + /*! + * Retrieves the number of MIP solvers, Gurobi spawns in parallel. + * + * @return The number of MIP solvers Gurobi spawns in parallel.. + */ + uint_fast64_t getNumberOfConcurrentMipThreads() const; + /*! * Retrieves whether the output option was set. * @@ -62,6 +77,8 @@ namespace storm { static const std::string integerToleranceOption; static const std::string threadsOption; static const std::string outputOption; + static const std::string mipFocusOption; + static const std::string concurrentMipThreadsOption; }; } // namespace modules diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index 3e0db5333..cd556c936 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/src/storm/solver/GurobiLpSolver.cpp @@ -76,7 +76,13 @@ namespace storm { // Enable the following line to restrict Gurobi to one thread only. error = GRBsetintparam(env, "Threads", storm::settings::getModule().getNumberOfThreads()); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter Threads (" << GRBgeterrormsg(env) << ", error code " << error << ")."); - + + error = GRBsetintparam(env, "MIPFocus", storm::settings::getModule().getMIPFocus()); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter MIPFocus (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + error = GRBsetintparam(env, "ConcurrentMIP", storm::settings::getModule().getNumberOfConcurrentMipThreads()); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter ConcurrentMIP (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + // Enable the following line to force Gurobi to be as precise about the binary variables as required by the given precision option. error = GRBsetdblparam(env, "IntFeasTol", storm::settings::getModule().getIntegerTolerance()); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ")."); @@ -175,6 +181,7 @@ namespace storm { template void GurobiLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + STORM_LOG_TRACE("Adding constraint " << name << " to GurobiLpSolver:" << std::endl << "\t" << constraint); STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression."); STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator."); @@ -436,6 +443,132 @@ namespace storm { } } + template + void GurobiLpSolver::setMaximalSolutionCount(uint64_t value) { + int error = GRBsetintparam(GRBgetenv(model), "PoolSolutions", value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter PoolSolutions (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + } + + template + uint64_t GurobiLpSolver::getSolutionCount() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to GurobiLpSolver::getSolutionCount: model has not been optimized."); + int result = -1; + int error = GRBgetintattr(model, "SolCount", &result); + STORM_LOG_THROW(error == 0 && result >= 0, storm::exceptions::InvalidStateException, "Unable to get solution count or invalid number of solutions."); + return result; + } + + template + ValueType GurobiLpSolver::getContinuousValue(storm::expressions::Variable const& variable, uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + auto variableIndexPair = this->variableToIndexMap.find(variable); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, variableIndexPair->second, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + return storm::utility::convertNumber(value); + } + + template + int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable, uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + auto variableIndexPair = this->variableToIndexMap.find(variable); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, variableIndexPair->second, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + STORM_LOG_THROW(std::abs(static_cast(value) - value) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + + return static_cast(value); + } + + template + bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable, uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + auto variableIndexPair = this->variableToIndexMap.find(variable); + STORM_LOG_THROW(variableIndexPair != this->variableToIndexMap.end(), storm::exceptions::InvalidAccessException, "Accessing value of unknown variable '" << variable.getName() << "'."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattrelement(model, GRB_DBL_ATTR_Xn, variableIndexPair->second, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + if (value > 0.5) { + STORM_LOG_THROW(std::abs(static_cast(value) - 1) <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + } else { + STORM_LOG_THROW(value <= storm::settings::getModule().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in Gurobi solution (" << value << ")."); + } + + return static_cast(value); + } + + template + ValueType GurobiLpSolver::getObjectiveValue(uint64_t const& solutionIndex) const { + if (!this->isOptimal()) { + STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); + STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unoptimized model (" << GRBgeterrormsg(env) << ")."); + } + STORM_LOG_ASSERT(solutionIndex < getSolutionCount(), "Invalid solution index."); + + double value = 0; + int error = GRBsetintparam(GRBgetenv(model), GRB_INT_PAR_SOLUTIONNUMBER, solutionIndex); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi solution index (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + error = GRBgetdblattr(model, GRB_DBL_ATTR_POOLOBJVAL, &value); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + + return storm::utility::convertNumber(value); + } + + template + void GurobiLpSolver::setMaximalMILPGap(ValueType const& gap, bool relative) { + int error = -1; + if (relative) { + error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAP, storm::utility::convertNumber(gap)); + } else { + error = GRBsetdblparam(GRBgetenv(model), GRB_DBL_PAR_MIPGAPABS, storm::utility::convertNumber(gap)); + } + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi MILP GAP (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + } + + template + ValueType GurobiLpSolver::getMILPGap(bool relative) const { + double relativeGap; + int error = GRBgetdblattr(model, GRB_DBL_ATTR_MIPGAP, &relativeGap); + STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi MILP GAP (" << GRBgeterrormsg(env) << ", error code " << error << ")."); + auto result = storm::utility::convertNumber(relativeGap); + if (relative) { + return result; + } else { + return result * getObjectiveValue(); + } + } #else template @@ -577,6 +710,49 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } + template + void GurobiLpSolver::setMaximalSolutionCount(uint64_t) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + uint64_t GurobiLpSolver::getSolutionCount() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getContinuousValue(storm::expressions::Variable const&, uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const&, uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const&, uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getObjectiveValue(uint64_t const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + + template + void GurobiLpSolver::setMaximalMILPGap(ValueType const&, bool) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getMILPGap(bool) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of storm with Gurobi support."; + } + + + #endif template class GurobiLpSolver; template class GurobiLpSolver; diff --git a/src/storm/solver/GurobiLpSolver.h b/src/storm/solver/GurobiLpSolver.h index 955e4c5ff..5947ad600 100644 --- a/src/storm/solver/GurobiLpSolver.h +++ b/src/storm/solver/GurobiLpSolver.h @@ -99,7 +99,6 @@ namespace storm { virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override; virtual bool getBinaryValue(storm::expressions::Variable const& name) const override; virtual ValueType getObjectiveValue() const override; - // Methods to print the LP problem to a file. virtual void writeModelToFile(std::string const& filename) const override; @@ -107,6 +106,28 @@ namespace storm { virtual void push() override; virtual void pop() override; + + // Methods to retrieve values of sub-optimal solutions found along the way. + void setMaximalSolutionCount(uint64_t value); // How many solutions will be stored (at max) + uint64_t getSolutionCount() const; // How many solutions have been found + ValueType getContinuousValue(storm::expressions::Variable const& name, uint64_t const& solutionIndex) const; + int_fast64_t getIntegerValue(storm::expressions::Variable const& name, uint64_t const& solutionIndex) const; + bool getBinaryValue(storm::expressions::Variable const& name, uint64_t const& solutionIndex) const; + ValueType getObjectiveValue(uint64_t const& solutionIndex) const; + + /*! + * Specifies the maximum difference between lower- and upper objective bounds that triggers termination. + * That means a solution is considered optimal if + * upperBound - lowerBound < gap * (relative ? |upperBound| : 1). + * Only relevant for programs with integer/boolean variables. + */ + void setMaximalMILPGap(ValueType const& gap, bool relative); + + /*! + * Returns the obtained gap after a call to optimize() + */ + ValueType getMILPGap(bool relative) const; + private: /*! * Sets some properties of the Gurobi environment according to parameters given by the options. From 70112b7315bec504a61b65077f83f1d71f40df65 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 6 May 2019 18:03:48 +0200 Subject: [PATCH 09/13] Fixed a name clash that sometimes occurred when compiling Storm on macOS with TBB. --- src/storm/adapters/RationalFunctionAdapter.h | 31 ++++++++++++++++++++ src/storm/analysis/GraphConditions.h | 15 ++-------- 2 files changed, 33 insertions(+), 13 deletions(-) diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h index f403103f5..39490d81e 100644 --- a/src/storm/adapters/RationalFunctionAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -9,6 +9,27 @@ #include #include +// Some header files on macOS (included via INTEL TBB) might #define TRUE and FALSE, which in carl/formula/Formula.h are used as FormulaTypes. +// Hence, we temporarily #undef these: +#ifdef TRUE +#define STORM_TEMP_TRUE TRUE +#undef TRUE +#endif +#ifdef FALSE +#define STORM_TEMP_FALSE FALSE +#undef FALSE +#endif +#include +// Restore TRUE / FALSE macros. +#ifdef STORM_TEMP_TRUE +#define TRUE STORM_TEMP_TRUE +#undef STORM_TEMP_TRUE +#endif +#ifdef STORM_TEMP_FALSE +#define FALSE STORM_TEMP_FALSE +#undef STORM_TEMP_FALSE +#endif + namespace carl { // Define hash values for all polynomials and rational function. template @@ -57,5 +78,15 @@ namespace storm { typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; + + template + struct ConstraintType { + typedef void* val; + }; + + template + struct ConstraintType::value>::type> { + typedef carl::Formula val; + }; } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index a901dfa68..04b5d7774 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -4,21 +4,10 @@ #include #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" -#include namespace storm { namespace analysis { - template - struct ConstraintType { - typedef void* val; - }; - - template - struct ConstraintType::value>::type> { - typedef carl::Formula val; - }; - /** * Class to collect constraints on parametric Markov chains. */ @@ -26,11 +15,11 @@ namespace storm { class ConstraintCollector { private: // A set of constraints that says that the DTMC actually has valid probability distributions in all states. - std::unordered_set::val> wellformedConstraintSet; + std::unordered_set::val> wellformedConstraintSet; // A set of constraints that makes sure that the underlying graph of the model does not change depending // on the parameter values. - std::unordered_set::val> graphPreservingConstraintSet; + std::unordered_set::val> graphPreservingConstraintSet; // A set of variables std::set variableSet; From 7881512a17fd4bf0bc4abe95c47007f34adafb3f Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 6 May 2019 18:21:08 +0200 Subject: [PATCH 10/13] Removed ConstraintType definition out of RationalFunctionAdapter to make things more consistent. --- src/storm/adapters/RationalFunctionAdapter.h | 10 +--------- src/storm/analysis/GraphConditions.h | 15 +++++++++++++-- 2 files changed, 14 insertions(+), 11 deletions(-) diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h index 39490d81e..e41869b5b 100644 --- a/src/storm/adapters/RationalFunctionAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -78,15 +78,7 @@ namespace storm { typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; - - template - struct ConstraintType { - typedef void* val; - }; - template - struct ConstraintType::value>::type> { - typedef carl::Formula val; - }; + typedef carl::Formula RationalFunctionConstraint; } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 04b5d7774..f9f119fc1 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -8,6 +8,17 @@ namespace storm { namespace analysis { + + template + struct ConstraintType { + typedef void* val; + }; + + template + struct ConstraintType::value>::type> { + typedef storm::RationalFunctionConstraint val; + }; + /** * Class to collect constraints on parametric Markov chains. */ @@ -15,11 +26,11 @@ namespace storm { class ConstraintCollector { private: // A set of constraints that says that the DTMC actually has valid probability distributions in all states. - std::unordered_set::val> wellformedConstraintSet; + std::unordered_set::val> wellformedConstraintSet; // A set of constraints that makes sure that the underlying graph of the model does not change depending // on the parameter values. - std::unordered_set::val> graphPreservingConstraintSet; + std::unordered_set::val> graphPreservingConstraintSet; // A set of variables std::set variableSet; From dd1d53046c4e4a4a860090881912a8f195fba389 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 7 May 2019 09:58:20 +0200 Subject: [PATCH 11/13] utility/constants.cpp: Fixing unknown 'isnan' --- src/storm/utility/constants.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 050955956..b1944c267 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -52,7 +52,7 @@ namespace storm { template<> bool isNan(double const& value) { - return isnan(value); + return std::isnan(value); } bool isAlmostZero(double const& a) { From fe658ee78700c5b184c44e7a74058f0bdc8e8a53 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 7 May 2019 10:36:58 +0200 Subject: [PATCH 12/13] Reverting the previous fix since the jit builder wasn't happy about the carl/formula/Formula.h include. --- src/storm/adapters/RationalFunctionAdapter.h | 23 -------------------- src/storm/analysis/GraphConditions.h | 3 ++- 2 files changed, 2 insertions(+), 24 deletions(-) diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h index e41869b5b..f403103f5 100644 --- a/src/storm/adapters/RationalFunctionAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -9,27 +9,6 @@ #include #include -// Some header files on macOS (included via INTEL TBB) might #define TRUE and FALSE, which in carl/formula/Formula.h are used as FormulaTypes. -// Hence, we temporarily #undef these: -#ifdef TRUE -#define STORM_TEMP_TRUE TRUE -#undef TRUE -#endif -#ifdef FALSE -#define STORM_TEMP_FALSE FALSE -#undef FALSE -#endif -#include -// Restore TRUE / FALSE macros. -#ifdef STORM_TEMP_TRUE -#define TRUE STORM_TEMP_TRUE -#undef STORM_TEMP_TRUE -#endif -#ifdef STORM_TEMP_FALSE -#define FALSE STORM_TEMP_FALSE -#undef STORM_TEMP_FALSE -#endif - namespace carl { // Define hash values for all polynomials and rational function. template @@ -78,7 +57,5 @@ namespace storm { typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; - - typedef carl::Formula RationalFunctionConstraint; } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index f9f119fc1..00c0d5101 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -4,6 +4,7 @@ #include #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" +#include namespace storm { namespace analysis { @@ -16,7 +17,7 @@ namespace storm { template struct ConstraintType::value>::type> { - typedef storm::RationalFunctionConstraint val; + typedef carl::Formula val; }; /** From 3a11a4b3eb8377a1316e47af3d4219f0edeaaf56 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 7 May 2019 10:37:59 +0200 Subject: [PATCH 13/13] Introducing a TBB adapter that #undefs TRUE and FALSE. --- .../3rdparty/gmm-5.2/include/gmm/gmm_blas.h | 2 +- src/storm-cli-utilities/cli.cpp | 5 ++- src/storm/adapters/IntelTbbAdapter.h | 32 +++++++++++++++++++ src/storm/settings/modules/CoreSettings.cpp | 1 + src/storm/solver/GmmxxMultiplier.cpp | 1 + src/storm/solver/NativeMultiplier.cpp | 1 + src/storm/storage/SparseMatrix.cpp | 7 ---- src/storm/storage/SparseMatrix.h | 1 + src/storm/utility/VectorHelper.cpp | 3 +- src/storm/utility/vector.h | 6 +--- 10 files changed, 41 insertions(+), 18 deletions(-) create mode 100644 src/storm/adapters/IntelTbbAdapter.h diff --git a/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h b/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h index 19e58f755..4fbe070d3 100644 --- a/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h +++ b/resources/3rdparty/gmm-5.2/include/gmm/gmm_blas.h @@ -44,7 +44,7 @@ #ifdef STORM_HAVE_INTELTBB #include // This fixes a potential dependency ordering problem between GMM and TBB -#include "tbb/tbb.h" +#include "storm/adapters/IntelTbbAdapter.h" #include #endif diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index e79971cbc..e4a929445 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -17,9 +17,8 @@ // Includes for the linked libraries and versions header. -#ifdef STORM_HAVE_INTELTBB -# include "tbb/tbb_stddef.h" -#endif +#include "storm/adapters/IntelTbbAdapter.h" + #ifdef STORM_HAVE_GLPK # include "glpk.h" #endif diff --git a/src/storm/adapters/IntelTbbAdapter.h b/src/storm/adapters/IntelTbbAdapter.h new file mode 100644 index 000000000..fb4d7eb72 --- /dev/null +++ b/src/storm/adapters/IntelTbbAdapter.h @@ -0,0 +1,32 @@ +#pragma once + +// To detect whether the usage of TBB is possible, this include is neccessary +#include "storm-config.h" + + +/* On macOS, TBB includes the header + * /Library/Developer/CommandLineTools/SDKs/MacOSX10.14.sdk/usr/include/mach/boolean.h + * which #defines macros TRUE and FALSE. Since these also occur as identifiers, we #undef them after including TBB. + * We still issue a warning in case these macros have been defined before. +*/ + +#ifdef TRUE +#warning "Undefining previously defined macro 'TRUE'." +#endif + +#ifdef FALSE +#warning "Undefining previously defined macro 'FALSE'." +#endif + +#ifdef STORM_HAVE_INTELTBB +#include "tbb/tbb.h" +#include "tbb/tbb_stddef.h" +#endif + +#ifdef TRUE +#undef TRUE +#endif + +#ifdef FALSE +#undef FALSE +#endif diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 3925012e3..baf474d1c 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -9,6 +9,7 @@ #include "storm/solver/SolverSelectionOptions.h" #include "storm/storage/dd/DdType.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/utility/macros.h" #include "storm/exceptions/IllegalArgumentValueException.h" diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index 95abf61fb..59d71af8e 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -2,6 +2,7 @@ #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/storage/SparseMatrix.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index 7dd2457df..b8c6c3549 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -10,6 +10,7 @@ #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 2ca0c823c..cdeaaf9a2 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1,12 +1,5 @@ #include -// To detect whether the usage of TBB is possible, this include is neccessary -#include "storm-config.h" - -#ifdef STORM_HAVE_INTELTBB -#include "tbb/tbb.h" -#endif - #include "storm/storage/sparse/StateType.h" #include "storm/storage/SparseMatrix.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index d33eda907..dbdd4086d 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -16,6 +16,7 @@ #include "storm/utility/macros.h" #include "storm/utility/constants.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/IntelTbbAdapter.h" // Forward declaration for adapter classes. namespace storm { diff --git a/src/storm/utility/VectorHelper.cpp b/src/storm/utility/VectorHelper.cpp index ca40c8844..352910dd1 100644 --- a/src/storm/utility/VectorHelper.cpp +++ b/src/storm/utility/VectorHelper.cpp @@ -5,8 +5,7 @@ #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" - -#include "storm-config.h" +#include "storm/adapters/IntelTbbAdapter.h" #include "storm/utility/vector.h" diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 153f74a36..82d698dde 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -1,16 +1,12 @@ #ifndef STORM_UTILITY_VECTOR_H_ #define STORM_UTILITY_VECTOR_H_ -#include "storm-config.h" -#ifdef STORM_HAVE_INTELTBB -#include "tbb/tbb.h" -#endif - #include #include #include #include #include +#include #include