diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index 0f91bfc7e..fbc2744a2 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -122,10 +122,9 @@ namespace storm { boost::optional result; if (!lpModel->isInfeasible()) { STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded."); - result = Point(); - for (auto const& objVar : currentObjectiveVariables) { - result->push_back(storm::utility::convertNumber(lpModel->getContinuousValue(objVar))); - } + swValidate.start(); + result = validateCurrentModel(env); + swValidate.stop(); } lpModel->pop(); return result; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index 10237d308..ff11d54a4 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -26,7 +26,6 @@ namespace storm { typedef typename std::vector Point; DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectiveHelper); - ~DeterministicSchedsLpChecker(); /*! * Specifies the current direction. @@ -37,7 +36,7 @@ namespace storm { * Optimizes in the currently given direction * @return some optimal point found in that direction. */ - boost::optional check(storm::Environment const& env, Polytope area); + boost::optional check(storm::Environment const& env, Polytope overapproximation); /*! * Optimizes in the currently given direction, recursively checks for points in the given area. @@ -45,6 +44,12 @@ namespace storm { */ std::pair, std::vector> check(storm::Environment const& env, storm::storage::geometry::PolytopeTree& polytopeTree, Point const& eps); + /*! + * Returns usage statistics in a human readable format. + * @param prefix will be prepended to each line + */ + std::string getStatistics(std::string const& prefix = "") const; + private: bool processEndComponents(std::vector>& ecVars); void initializeLpModel(Environment const& env); @@ -65,11 +70,10 @@ namespace storm { std::vector currentWeightVector; storm::utility::Stopwatch swInit; - storm::utility::Stopwatch swCheck; - storm::utility::Stopwatch swCheckVertices; - storm::utility::Stopwatch swLpSolve; - storm::utility::Stopwatch swLpBuild; - storm::utility::Stopwatch swAux; + storm::utility::Stopwatch swCheckWeightVectors; + storm::utility::Stopwatch swCheckAreas; + storm::utility::Stopwatch swValidate; + uint64_t numLpQueries; }; }