sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

LpChecker: Only build the LP model if it is actually needed.

main
Tim Quatmann 6 years ago
parent
533206974b
commit
78237e8bb1
5 changed files with 37 additions and 28 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 39
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
  2. 6
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
  3. 14
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp
  4. 2
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h
  5. 2
      src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp

39
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
View File

@ -24,24 +24,28 @@ namespace storm {
namespace multiobjective {
template <typename ModelType, typename GeometryValueType>
DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper), numLpQueries(0) {
if (env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) {
flowEncoding = true;
for (auto const& helper : objectiveHelper) {
if (!helper.isTotalRewardObjective()) {
flowEncoding = false;
DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper), numLpQueries(0) {
// intentionally left empty
}
template <typename ModelType, typename GeometryValueType>
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initialize(Environment const& env) {
if (!lpModel) {
if (env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) {
flowEncoding = true;
for (auto const& helper : objectiveHelper) {
if (!helper.isTotalRewardObjective()) {
flowEncoding = false;
}
}
} else {
flowEncoding = env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow;
}
} else {
flowEncoding = env.modelchecker().multi().getEncodingType() == storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow;
STORM_PRINT_AND_LOG("Using " << (flowEncoding ? "flow" : "classical") << " encoding." << std::endl);
swInit.start();
initializeLpModel(env);
swInit.stop();
}
STORM_LOG_INFO_COND(flowEncoding, "Using classical encoding.");
STORM_LOG_INFO_COND(!flowEncoding, "Using flow encoding.");
swAll.start();
swInit.start();
initializeLpModel(env);
swInit.stop();
swAll.stop();
}
template <typename ModelType, typename GeometryValueType>
@ -57,8 +61,9 @@ namespace storm {
}
template <typename ModelType, typename GeometryValueType>
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::setCurrentWeightVector(std::vector<GeometryValueType> const& weightVector) {
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::setCurrentWeightVector(Environment const& env, std::vector<GeometryValueType> const& weightVector) {
swAll.start();
initialize(env);
STORM_LOG_ASSERT(weightVector.size() == objectiveHelper.size(), "Setting a weight vector with invalid number of entries.");
if (!currentWeightVector.empty()) {
// Pop information of the current weight vector.
@ -86,6 +91,7 @@ namespace storm {
template <typename ModelType, typename GeometryValueType>
boost::optional<std::vector<GeometryValueType>> DeterministicSchedsLpChecker<ModelType, GeometryValueType>::check(storm::Environment const& env, Polytope overapproximation) {
swAll.start();
initialize(env);
STORM_LOG_ASSERT(!currentWeightVector.empty(), "Checking invoked before specifying a weight vector.");
STORM_LOG_TRACE("Checking a vertex...");
lpModel->push();
@ -114,6 +120,7 @@ namespace storm {
template <typename ModelType, typename GeometryValueType>
std::pair<std::vector<std::vector<GeometryValueType>>, std::vector<std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>>>> DeterministicSchedsLpChecker<ModelType, GeometryValueType>::check(storm::Environment const& env, storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, Point const& eps) {
swAll.start();
initialize(env);
STORM_LOG_INFO("Checking " << polytopeTree.toString());
STORM_LOG_ASSERT(!currentWeightVector.empty(), "Checking invoked before specifying a weight vector.");
if (polytopeTree.isEmpty()) {

6
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
View File

@ -25,12 +25,12 @@ namespace storm {
typedef typename std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> Polytope;
typedef typename std::vector<GeometryValueType> Point;
DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper);
DeterministicSchedsLpChecker(ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper);
/*!
* Specifies the current direction.
*/
void setCurrentWeightVector(std::vector<GeometryValueType> const& weightVector);
void setCurrentWeightVector(Environment const& env, std::vector<GeometryValueType> const& weightVector);
/*!
* Optimizes in the currently given direction
@ -51,6 +51,8 @@ namespace storm {
std::string getStatistics(std::string const& prefix = "") const;
private:
void initialize(Environment const& env);
bool processEndComponents(std::vector<std::vector<storm::expressions::Expression>>& ecVars);
void initializeLpModel(Environment const& env);

14
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp
View File

@ -280,13 +280,13 @@ namespace storm {
}
template <class SparseModelType, typename GeometryValueType>
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) {
DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : model(preprocessorResult.preprocessedModel), objectives(preprocessorResult.objectives) {
originalModelInitialState = *preprocessorResult.originalModel.getInitialStates().begin();
objectiveHelper.reserve(objectives.size());
for (auto const& obj : objectives) {
objectiveHelper.emplace_back(*model, obj);
}
lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(env, *model, objectiveHelper);
lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(*model, objectiveHelper);
if (preprocessorResult.containsOnlyTotalRewardFormulas()) {
wvChecker = storm::modelchecker::multiobjective::WeightVectorCheckerFactory<SparseModelType>::create(preprocessorResult);
} else {
@ -346,8 +346,8 @@ namespace storm {
}
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
STORM_PRINT_AND_LOG("#STATS " << paretoPoints.size() << " Pareto points" << std::endl);
STORM_PRINT_AND_LOG("#STATS " << unachievableAreas.size() << " unachievable Areas" << std::endl);
STORM_PRINT_AND_LOG("#STATS " << overApproximation->getHalfspaces().size() << " unachievable Halfspaces" << std::endl);
STORM_PRINT_AND_LOG("#STATS " << unachievableAreas.size() << " unachievable areas" << std::endl);
STORM_PRINT_AND_LOG("#STATS " << overApproximation->getHalfspaces().size() << " unachievable halfspaces" << std::endl);
STORM_PRINT_AND_LOG(lpChecker->getStatistics("#STATS "));
}
@ -449,7 +449,7 @@ namespace storm {
point = storm::utility::vector::convertNumericVector<GeometryValueType>(wvChecker->getUnderApproximationOfInitialStateResults());
negateMinObjectives(point);
} else {
lpChecker->setCurrentWeightVector(weightVector);
lpChecker->setCurrentWeightVector(env, weightVector);
auto optionalPoint = lpChecker->check(env, negateMinObjectives(this->overApproximation));
STORM_LOG_THROW(optionalPoint.is_initialized(), storm::exceptions::UnexpectedException, "Unable to find a point in the current overapproximation.");
point = std::move(optionalPoint.get());
@ -494,7 +494,7 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType>
void DeterministicSchedsParetoExplorer<SparseModelType, GeometryValueType>::processFacet(Environment const& env, Facet& f) {
if (!wvChecker) {
lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector());
lpChecker->setCurrentWeightVector(env, f.getHalfspace().normalVector());
}
if (optimizeAndSplitFacet(env, f)) {
@ -510,7 +510,7 @@ namespace storm {
}
if (!polytopeTree.isEmpty()) {
if (wvChecker) {
lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector());
lpChecker->setCurrentWeightVector(env, f.getHalfspace().normalVector());
}
auto res = lpChecker->check(env, polytopeTree, eps);
for (auto const& infeasableArea : res.second) {

2
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h
View File

@ -126,7 +126,7 @@ namespace storm {
};
DeterministicSchedsParetoExplorer(Environment const& env, preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
DeterministicSchedsParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
virtual std::unique_ptr<CheckResult> check(Environment const& env);

2
src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
View File

@ -53,7 +53,7 @@ namespace storm {
{
if (env.modelchecker().multi().isSchedulerRestrictionSet()) {
STORM_LOG_THROW(preprocessorResult.queryType == preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto, storm::exceptions::NotImplementedException, "Currently, only Pareto queries with scheduler restrictions are implemented.");
auto explorer = DeterministicSchedsParetoExplorer<SparseModelType, storm::RationalNumber>(env, preprocessorResult);
auto explorer = DeterministicSchedsParetoExplorer<SparseModelType, storm::RationalNumber>(preprocessorResult);
result = explorer.check(env);
if (env.modelchecker().multi().isExportPlotSet()) {
explorer.exportPlotOfCurrentApproximation(env);

Write Preview
Loading…
Cancel
Save