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

DeterministicSchedsLpChecker: Added various variants of the encoding.

tempestpy_adaptions
Tim Quatmann 6 years ago
parent
7ab409fd2a
commit
3a7f89b396
4 changed files with 267 additions and 66 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. 321
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
  2. 2
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
  3. 5
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp
  4. 5
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h

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

@ -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<storm::settings::modules::MultiObjectiveSettings>().isMaxStepsSet()) {
res.setFromInt(0, 64, storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().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 <typename ModelType, typename GeometryValueType>
DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> 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<ValueType>(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<Point> foundPoints;
std::vector<Polytope> 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 <typename ModelType, typename GeometryValueType>
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::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<ValueType>("model");
gurobiLpModel = dynamic_cast<storm::solver::GurobiLpSolver<ValueType>*>(lpModel.get());
lpModel->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
initialStateResults.clear();
auto zero = lpModel->getConstant(storm::utility::zero<ValueType>());
auto one = lpModel->getConstant(storm::utility::one<ValueType>());
// 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<storm::expressions::Expression> 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<storm::expressions::Expression> 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<ValueType> visitingTimesUpperBounds;
{
// TODO: this doesn't work if there are end components.
storm::storage::SparseMatrix<ValueType> transitions = model.getTransitionMatrix().getSubmatrix(true, nonBottomStates, nonBottomStates);
std::vector<ValueType> probabilitiesToBottomStates = model.getTransitionMatrix().getConstrainedRowGroupSumVector(nonBottomStates, bottomStates);
auto subsystemBounds = storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ValueType>::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<ValueType>());
} 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<storm::expressions::Expression> 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<ValueType>(), 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<storm::expressions::Expression> bottomStatesIn;
std::vector<std::vector<storm::expressions::Expression>> 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<ValueType>(), 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<storm::expressions::Expression> 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<storm::expressions::Expression> 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<ValueType>()).getExpression();
} else {
choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), storm::utility::zero<ValueType>(), 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<ValueType>(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 <typename ModelType, typename GeometryValueType>
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::checkRecursive(storm::storage::geometry::PolytopeTree <GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas) {
void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::checkRecursive(storm::storage::geometry::PolytopeTree <GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& 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<GeometryValueType>(lpModel->getContinuousValue(objVar)));
}
std::vector<Point> 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<GeometryValueType>(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();
}

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

@ -48,7 +48,7 @@ namespace storm {
private:
void initializeLpModel(Environment const& env);
void checkRecursive(storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas);
void checkRecursive(storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas, uint64_t const& depth);
ModelType const& model;
std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper;

5
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp
View File

@ -219,6 +219,11 @@ namespace storm {
bool DeterministicSchedsObjectiveHelper<ModelType>::minimizing() const {
return storm::solver::minimize(objective.formula->getOptimalityType());
}
template <typename ModelType>
bool DeterministicSchedsObjectiveHelper<ModelType>::isTotalRewardObjective() const {
return objective.formula->isRewardOperatorFormula() && objective.formula->getSubformula().isTotalRewardFormula();
}
template class DeterministicSchedsObjectiveHelper<storm::models::sparse::Mdp<double>>;
template class DeterministicSchedsObjectiveHelper<storm::models::sparse::Mdp<storm::RationalNumber>>;

5
src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h
View File

@ -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<std::map<uint64_t, ValueType>> schedulerIndependentStateValues;

Write Preview
Loading…
Cancel
Save