From 3a7f89b39660bac78c61f1828c74850e7e953657 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 7 May 2019 18:37:29 +0200 Subject: [PATCH] DeterministicSchedsLpChecker: Added various variants of the encoding. --- .../DeterministicSchedsLpChecker.cpp | 321 ++++++++++++++---- .../DeterministicSchedsLpChecker.h | 2 +- .../DeterministicSchedsObjectiveHelper.cpp | 5 + .../DeterministicSchedsObjectiveHelper.h | 5 + 4 files changed, 267 insertions(+), 66 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index 842580ef6..41cff1408 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -1,12 +1,61 @@ #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h" + +#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" + #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/solver.h" +#include "storm/utility/graph.h" +#include "storm/storage/SparseMatrix.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/MultiObjectiveSettings.h" + +#include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace modelchecker { namespace multiobjective { + + + storm::storage::BitVector encodingSettings() { + storm::storage::BitVector res(64, false); + if (storm::settings::getModule().isMaxStepsSet()) { + res.setFromInt(0, 64, storm::settings::getModule().getMaxSteps()); + } + return res; + } + + bool isMinNegativeEncoding() { + return encodingSettings().get(63); + } + + bool isMaxDiffEncoding() { + bool result = encodingSettings().get(62); + STORM_LOG_ERROR_COND(!result || !isMinNegativeEncoding(), "maxDiffEncoding only works without minnegative encoding."); + return result; + } + + bool choiceVarReduction() { + return encodingSettings().get(61); + } + + bool inOutEncoding() { + return encodingSettings().get(60); + } + + bool assertBottomStateSum() { + bool result = encodingSettings().get(59); + STORM_LOG_ERROR_COND(!result || inOutEncoding(), "Asserting bottom state sum is only relevant for in-out encoding."); + return result; + } + + bool useNonOptimalSolutions() { + bool result = encodingSettings().get(58); + STORM_LOG_ERROR_COND(!result || inOutEncoding(), "Asserting bottom state sum is only relevant for in-out encoding."); + return result; + } template DeterministicSchedsLpChecker::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper) { @@ -43,7 +92,7 @@ namespace storm { // set up objective function for the given weight vector for (uint64_t objIndex = 0; objIndex < initialStateResults.size(); ++objIndex) { currentObjectiveVariables.push_back(lpModel->addUnboundedContinuousVariable("w_" + std::to_string(objIndex), storm::utility::convertNumber(weightVector[objIndex]))); - if (objectiveHelper[objIndex].minimizing()) { + if (objectiveHelper[objIndex].minimizing() && !isMinNegativeEncoding()) { lpModel->addConstraint("", currentObjectiveVariables.back().getExpression() == -initialStateResults[objIndex]); } else { lpModel->addConstraint("", currentObjectiveVariables.back().getExpression() == initialStateResults[objIndex]); @@ -105,7 +154,7 @@ namespace storm { std::vector foundPoints; std::vector infeasableAreas; - checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas); + checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas, 0); swCheck.stop(); std::cout << " done!" << std::endl; @@ -114,13 +163,17 @@ namespace storm { template void DeterministicSchedsLpChecker::initializeLpModel(Environment const& env) { + STORM_LOG_INFO("Initializing LP model with " << model.getNumberOfStates() << " states."); uint64_t numStates = model.getNumberOfStates(); + uint64_t initialState = *model.getInitialStates().begin(); + lpModel = storm::utility::solver::getLpSolver("model"); gurobiLpModel = dynamic_cast*>(lpModel.get()); lpModel->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); initialStateResults.clear(); + auto zero = lpModel->getConstant(storm::utility::zero()); auto one = lpModel->getConstant(storm::utility::one()); // Create choice variables and assert that at least one choice is taken at each state. @@ -132,98 +185,233 @@ namespace storm { choiceVars.emplace_back(); } else { std::vector localChoices; + if (choiceVarReduction()) { + --numChoices; + } for (uint64_t choice = 0; choice < numChoices; ++choice) { localChoices.push_back(lpModel->addBoundedIntegerVariable("c" + std::to_string(state) + "_" + std::to_string(choice), 0, 1).getExpression()); + choiceVars.push_back(localChoices.back()); + } + storm::expressions::Expression localChoicesSum = storm::expressions::sum(localChoices).reduceNesting(); + if (choiceVarReduction()) { + lpModel->addConstraint("", localChoicesSum <= one); + choiceVars.push_back(one - localChoicesSum); + } else { + lpModel->addConstraint("", localChoicesSum == one); } - lpModel->addConstraint("", storm::expressions::sum(localChoices).reduceNesting() == one); - choiceVars.insert(choiceVars.end(), localChoices.begin(), localChoices.end()); } } - for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) { - auto const& schedulerIndependentStates = objectiveHelper[objIndex].getSchedulerIndependentStateValues(); - // Create state variables - std::vector stateVars; - stateVars.reserve(numStates); - for (uint64_t state = 0; state < numStates; ++state) { - auto valIt = schedulerIndependentStates.find(state); - if (valIt == schedulerIndependentStates.end()) { - stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), objectiveHelper[objIndex].getLowerValueBoundAtState(env, state), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression()); - } else { - stateVars.push_back(lpModel->getConstant(valIt->second)); - } - if (state == *model.getInitialStates().begin()) { - initialStateResults.push_back(stateVars.back()); + if (inOutEncoding()) { + storm::storage::BitVector bottomStates(model.getNumberOfStates(), true); + for (auto const& helper : objectiveHelper) { + STORM_LOG_THROW(helper.isTotalRewardObjective(), storm::exceptions::InvalidOperationException, "The given type of encoding is only supported if the objectives can be reduced to total reward objectives."); + storm::storage::BitVector objBottomStates(model.getNumberOfStates(), false); + for (auto const& stateVal : helper.getSchedulerIndependentStateValues()) { + STORM_LOG_THROW(storm::utility::isZero(stateVal.second), storm::exceptions::InvalidOperationException, "Non-zero constant state-values not allowed for this type of encoding."); + objBottomStates.set(stateVal.first, true); } + bottomStates &= objBottomStates; } + storm::storage::BitVector nonBottomStates = ~bottomStates; + STORM_LOG_TRACE("Found " << bottomStates.getNumberOfSetBits() << " bottom states."); + STORM_LOG_ERROR_COND(storm::utility::graph::performProb1A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), model.getBackwardTransitions(), nonBottomStates, bottomStates).full(), "End components not yet treated correctly."); - // Create and assert choice values - auto const& choiceValueOffsets = objectiveHelper[objIndex].getChoiceValueOffsets(); - for (uint64_t state = 0; state < numStates; ++state) { - if (schedulerIndependentStates.find(state) != schedulerIndependentStates.end()) { - continue; + // Compute upper bounds for each state + std::vector visitingTimesUpperBounds; + { + // TODO: this doesn't work if there are end components. + storm::storage::SparseMatrix transitions = model.getTransitionMatrix().getSubmatrix(true, nonBottomStates, nonBottomStates); + std::vector probabilitiesToBottomStates = model.getTransitionMatrix().getConstrainedRowGroupSumVector(nonBottomStates, bottomStates); + auto subsystemBounds = storm::modelchecker::helper::BaierUpperRewardBoundsComputer::computeUpperBoundOnExpectedVisitingTimes(transitions, probabilitiesToBottomStates); + uint64_t subsystemState = 0; + visitingTimesUpperBounds.reserve(bottomStates.size()); + for (uint64_t state = 0; state < bottomStates.size(); ++state) { + if (bottomStates.get(state)) { + visitingTimesUpperBounds.push_back(storm::utility::zero()); + } else { + visitingTimesUpperBounds.push_back(subsystemBounds[subsystemState]); + ++subsystemState; + } } - storm::expressions::Expression stateValue; - uint64_t numChoices = model.getNumberOfChoices(state); - uint64_t choiceOffset = model.getTransitionMatrix().getRowGroupIndices()[state]; - for (uint64_t choice = 0; choice < numChoices; ++choice) { - storm::expressions::Expression choiceValue; - auto valIt = choiceValueOffsets.find(choiceOffset + choice); - if (valIt != choiceValueOffsets.end()) { - choiceValue = lpModel->getConstant(valIt->second); + assert(subsystemState == subsystemBounds.size()); + } + // create choiceValue variables and assert deterministic ones. + std::vector choiceValVars(model.getNumberOfChoices()); + for (auto const& state : nonBottomStates) { + for (uint64_t globalChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; globalChoice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++globalChoice) { + choiceValVars[globalChoice] = lpModel->addBoundedContinuousVariable("y" + std::to_string(globalChoice), storm::utility::zero(), visitingTimesUpperBounds[state]).getExpression(); + if (model.getNumberOfChoices(state) > 1) {; + lpModel->addConstraint("", choiceValVars[globalChoice] <= lpModel->getConstant(visitingTimesUpperBounds[state]) * choiceVars[globalChoice]); } - for (auto const& transition : model.getTransitionMatrix().getRow(state, choice)) { - storm::expressions::Expression transitionValue = lpModel->getConstant(transition.getValue()) * stateVars[transition.getColumn()]; - if (choiceValue.isInitialized()) { - choiceValue = choiceValue + transitionValue; + } + } + // Get 'in' and 'out' expressions + std::vector bottomStatesIn; + std::vector> ins(numStates), outs(numStates); + ins[initialState].push_back(one); + for (auto const& state : nonBottomStates) { + for (uint64_t globalChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; globalChoice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++globalChoice) { + for (auto const& transition : model.getTransitionMatrix().getRow(globalChoice)) { + uint64_t successor = transition.getColumn(); + storm::expressions::Expression exp = lpModel->getConstant(transition.getValue()) * choiceValVars[globalChoice]; + if (bottomStates.get(successor)) { + bottomStatesIn.push_back(exp); } else { - choiceValue = transitionValue; + ins[successor].push_back(exp); } } - choiceValue = choiceValue.simplify().reduceNesting(); - if (numChoices == 1) { - stateValue = choiceValue; - } else { - auto choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), storm::utility::zero(), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression(); - uint64_t globalChoiceIndex = model.getTransitionMatrix().getRowGroupIndices()[state] + choice; - storm::expressions::Expression upperValueBoundAtChoice = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)); - if (objectiveHelper[objIndex].minimizing()) { - lpModel->addConstraint("", choiceValVar + (upperValueBoundAtChoice * (one - choiceVars[globalChoiceIndex])) >= choiceValue); - // Optional: lpModel->addConstraint("", choiceValVar <= choiceValue); + outs[state].push_back(choiceValVars[globalChoice]); + } + } + + // Assert 'in == out' at each state + for (auto const& state : nonBottomStates) { + lpModel->addConstraint("", storm::expressions::sum(ins[state]) == storm::expressions::sum(outs[state])); + + } + if (assertBottomStateSum()) { + lpModel->addConstraint("", storm::expressions::sum(bottomStatesIn) == one); + } + + + // create initial state results for each objective + for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) { + auto choiceValueOffsets = objectiveHelper[objIndex].getChoiceValueOffsets(); + std::vector objValue; + for (auto const& state : nonBottomStates) { + for (uint64_t globalChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; globalChoice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++globalChoice) { + auto choiceValueIt = choiceValueOffsets.find(globalChoice); + if (choiceValueIt != choiceValueOffsets.end()) { + assert(!storm::utility::isZero(choiceValueIt->second)); + objValue.push_back(lpModel->getConstant(choiceValueIt->second) * choiceValVars[globalChoice]); + } + } + } + auto objValueVariable = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex), objectiveHelper[objIndex].getLowerValueBoundAtState(env, initialState), objectiveHelper[objIndex].getUpperValueBoundAtState(env, initialState)); + lpModel->addConstraint("", objValueVariable == storm::expressions::sum(objValue)); + initialStateResults.push_back(objValueVariable); + } + + } else { + // 'classic' backward encoding. + for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) { + auto const& schedulerIndependentStates = objectiveHelper[objIndex].getSchedulerIndependentStateValues(); + // Create state variables + std::vector stateVars; + stateVars.reserve(numStates); + for (uint64_t state = 0; state < numStates; ++state) { + auto valIt = schedulerIndependentStates.find(state); + if (valIt == schedulerIndependentStates.end()) { + if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) { + stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), -objectiveHelper[objIndex].getUpperValueBoundAtState(env, state), -objectiveHelper[objIndex].getLowerValueBoundAtState(env, state)).getExpression()); } else { - lpModel->addConstraint("", choiceValVar <= choiceValue); - lpModel->addConstraint("", choiceValVar <= upperValueBoundAtChoice * choiceVars[globalChoiceIndex]); + stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), objectiveHelper[objIndex].getLowerValueBoundAtState(env, state), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression()); } - if (choice == 0) { - stateValue = choiceValVar; + } else { + if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) { + stateVars.push_back(lpModel->getConstant(-valIt->second)); } else { - stateValue = stateValue + choiceValVar; + stateVars.push_back(lpModel->getConstant(valIt->second)); } - // Alternative encoding: (Then the sum of the choiceVars also has to be >= one (instead of == one) - //storm::expressions::Expression maxDiff = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state) - objectiveHelper[objIndex].getLowerValueBoundAtState(env, state)) * (one - choiceVars[globalChoiceIndex]); - //lpModel->addConstraint("", stateVars[state] - choiceValVar <= maxDiff); - //lpModel->addConstraint("", choiceValVar - stateVars[state] <= maxDiff); + } + if (state == initialState) { + initialStateResults.push_back(stateVars.back()); } } - if (objectiveHelper[objIndex].minimizing()) { - lpModel->addConstraint("", stateVars[state] >= stateValue); - } else { - lpModel->addConstraint("", stateVars[state] <= stateValue); + + // Create and assert choice values + auto const& choiceValueOffsets = objectiveHelper[objIndex].getChoiceValueOffsets(); + for (uint64_t state = 0; state < numStates; ++state) { + if (schedulerIndependentStates.find(state) != schedulerIndependentStates.end()) { + continue; + } + storm::expressions::Expression stateValue; + uint64_t numChoices = model.getNumberOfChoices(state); + uint64_t choiceOffset = model.getTransitionMatrix().getRowGroupIndices()[state]; + storm::expressions::Expression upperValueBoundAtState = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)); + for (uint64_t choice = 0; choice < numChoices; ++choice) { + storm::expressions::Expression choiceValue; + auto valIt = choiceValueOffsets.find(choiceOffset + choice); + if (valIt != choiceValueOffsets.end()) { + if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) { + choiceValue = lpModel->getConstant(-valIt->second); + } else { + choiceValue = lpModel->getConstant(valIt->second); + } + } + for (auto const& transition : model.getTransitionMatrix().getRow(state, choice)) { + storm::expressions::Expression transitionValue = lpModel->getConstant(transition.getValue()) * stateVars[transition.getColumn()]; + if (choiceValue.isInitialized()) { + choiceValue = choiceValue + transitionValue; + } else { + choiceValue = transitionValue; + } + } + choiceValue = choiceValue.simplify().reduceNesting(); + if (numChoices == 1) { + stateValue = choiceValue; + } else { + uint64_t globalChoiceIndex = model.getTransitionMatrix().getRowGroupIndices()[state] + choice; + if (isMaxDiffEncoding()) { + storm::expressions::Expression maxDiff = upperValueBoundAtState * (one - choiceVars[globalChoiceIndex]); + if (objectiveHelper[objIndex].minimizing()) { + lpModel->addConstraint("", stateVars[state] >= choiceValue - maxDiff); + } else { + lpModel->addConstraint("", stateVars[state] <= choiceValue + maxDiff); + } + } + + storm::expressions::Expression choiceValVar; + if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) { + choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), -objectiveHelper[objIndex].getUpperValueBoundAtState(env, state), storm::utility::zero()).getExpression(); + } else { + choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), storm::utility::zero(), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression(); + } + if (objectiveHelper[objIndex].minimizing()) { + if (isMinNegativeEncoding()) { + lpModel->addConstraint("", choiceValVar <= choiceValue); + lpModel->addConstraint("", choiceValVar <= -upperValueBoundAtState * (one - choiceVars[globalChoiceIndex])); + } else { + lpModel->addConstraint("", choiceValVar + (upperValueBoundAtState * (one - choiceVars[globalChoiceIndex])) >= choiceValue); + // Optional: lpModel->addConstraint("", choiceValVar <= choiceValue); + } + } else { + lpModel->addConstraint("", choiceValVar <= choiceValue); + lpModel->addConstraint("", choiceValVar <= upperValueBoundAtState * choiceVars[globalChoiceIndex]); + } + if (choice == 0) { + stateValue = choiceValVar; + } else { + stateValue = stateValue + choiceValVar; + } + } + } + if (objectiveHelper[objIndex].minimizing()) { + if (isMinNegativeEncoding()) { + lpModel->addConstraint("", stateVars[state] <= stateValue + (lpModel->getConstant(storm::utility::convertNumber(numChoices - 1)) * upperValueBoundAtState)); + } else { + lpModel->addConstraint("", stateVars[state] >= stateValue); + } + } else { + lpModel->addConstraint("", stateVars[state] <= stateValue); + } } } } swAux.start(); lpModel->update(); swAux.stop(); + STORM_LOG_INFO("Done initializing LP model."); } template - void DeterministicSchedsLpChecker::checkRecursive(storm::storage::geometry::PolytopeTree & polytopeTree, GeometryValueType const& eps, std::vector& foundPoints, std::vector& infeasableAreas) { + void DeterministicSchedsLpChecker::checkRecursive(storm::storage::geometry::PolytopeTree & polytopeTree, GeometryValueType const& eps, std::vector& foundPoints, std::vector& infeasableAreas, uint64_t const& depth) { std::cout << "."; std::cout.flush(); STORM_LOG_ASSERT(!polytopeTree.isEmpty(), "Tree node is empty"); STORM_LOG_ASSERT(!polytopeTree.getPolytope()->isEmpty(), "Tree node is empty."); - STORM_LOG_TRACE("Checking " << polytopeTree.toString()); + STORM_LOG_TRACE("Checking at depth " << depth << ": " << polytopeTree.toString()); swLpBuild.start(); lpModel->push(); @@ -245,6 +433,7 @@ namespace storm { if (lpModel->isInfeasible()) { infeasableAreas.push_back(polytopeTree.getPolytope()); + lpModel->writeModelToFile("out.lp"); polytopeTree.clear(); } else { STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded."); @@ -253,7 +442,7 @@ namespace storm { newPoint.push_back(storm::utility::convertNumber(lpModel->getContinuousValue(objVar))); } std::vector newPoints = {newPoint}; - if (gurobiLpModel) { + if (gurobiLpModel && useNonOptimalSolutions()) { // gurobi might have other good solutions. for (uint64_t solutionIndex = 0; solutionIndex < gurobiLpModel->getSolutionCount(); ++ solutionIndex) { Point p; @@ -269,7 +458,6 @@ namespace storm { newPoints.push_back(std::move(p)); } } - std::cout << "found " << (newPoints.size() - 1) << " useful points" << std::endl; } GeometryValueType offset = storm::utility::convertNumber(lpModel->getObjectiveValue()); if (gurobiLpModel) { @@ -289,14 +477,14 @@ namespace storm { } swAux.stop(); if (!polytopeTree.isEmpty()) { - checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas); + checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas, depth); } } } else { // Traverse all the children. for (uint64_t childId = 0; childId < polytopeTree.getChildren().size(); ++childId) { uint64_t newPointIndex = foundPoints.size(); - checkRecursive(polytopeTree.getChildren()[childId], eps, foundPoints, infeasableAreas); + checkRecursive(polytopeTree.getChildren()[childId], eps, foundPoints, infeasableAreas, depth + 1); STORM_LOG_ASSERT(polytopeTree.getChildren()[childId].isEmpty(), "expected empty children."); // Make the new points known to the right siblings for (; newPointIndex < foundPoints.size(); ++newPointIndex) { @@ -308,8 +496,11 @@ namespace storm { // All children are empty now, so this node becomes empty. polytopeTree.clear(); } + STORM_LOG_TRACE("Checking DONE at depth " << depth << " with node " << polytopeTree.toString()); + swLpBuild.start(); lpModel->pop(); + lpModel->update(); swLpBuild.stop(); } diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index e22b6d7a8..7c9f7978f 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -48,7 +48,7 @@ namespace storm { private: void initializeLpModel(Environment const& env); - void checkRecursive(storm::storage::geometry::PolytopeTree& polytopeTree, GeometryValueType const& eps, std::vector& foundPoints, std::vector& infeasableAreas); + void checkRecursive(storm::storage::geometry::PolytopeTree& polytopeTree, GeometryValueType const& eps, std::vector& foundPoints, std::vector& infeasableAreas, uint64_t const& depth); ModelType const& model; std::vector> const& objectiveHelper; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp index 734a016d0..b1f9ece62 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp @@ -219,6 +219,11 @@ namespace storm { bool DeterministicSchedsObjectiveHelper::minimizing() const { return storm::solver::minimize(objective.formula->getOptimalityType()); } + + template + bool DeterministicSchedsObjectiveHelper::isTotalRewardObjective() const { + return objective.formula->isRewardOperatorFormula() && objective.formula->getSubformula().isTotalRewardFormula(); + } template class DeterministicSchedsObjectiveHelper>; template class DeterministicSchedsObjectiveHelper>; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h index 9cf85f030..c93ef6086 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h @@ -36,6 +36,11 @@ namespace storm { bool minimizing() const; + /*! + * Returns true if this is a total reward objective + */ + bool isTotalRewardObjective() const; + private: mutable boost::optional> schedulerIndependentStateValues;