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

DeterministicScheds: Various bug fixes.

tempestpy_adaptions
TimQu 6 years ago
parent
19cca3585f
commit
c8dd748943
3 changed files with 29 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 31
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
  2. 7
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp
  3. 10
      src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp

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

@ -55,7 +55,6 @@ namespace storm {
bool useNonOptimalSolutions() { bool useNonOptimalSolutions() {
bool result = encodingSettings().get(58); bool result = encodingSettings().get(58);
STORM_LOG_ERROR_COND(!result || inOutEncoding(), "Asserting bottom state sum is only relevant for in-out encoding.");
return result; return result;
} }
@ -168,8 +167,8 @@ namespace storm {
std::map<storm::storage::BitVector, storm::storage::BitVector> getSubEndComponents(storm::storage::SparseMatrix<ValueType> const& mecTransitions) { std::map<storm::storage::BitVector, storm::storage::BitVector> getSubEndComponents(storm::storage::SparseMatrix<ValueType> const& mecTransitions) {
auto backwardTransitions = mecTransitions.transpose(true); auto backwardTransitions = mecTransitions.transpose(true);
std::map<storm::storage::BitVector, storm::storage::BitVector> unprocessed, processed; std::map<storm::storage::BitVector, storm::storage::BitVector> unprocessed, processed;
storm::storage::BitVector allStates(mecTransitions.getRowGroupCount());
storm::storage::BitVector allChoices(mecTransitions.getRowCount());
storm::storage::BitVector allStates(mecTransitions.getRowGroupCount(), true);
storm::storage::BitVector allChoices(mecTransitions.getRowCount(), true);
unprocessed[allStates] = allChoices; unprocessed[allStates] = allChoices;
while (!unprocessed.empty()) { while (!unprocessed.empty()) {
auto currentIt = unprocessed.begin(); auto currentIt = unprocessed.begin();
@ -212,25 +211,25 @@ namespace storm {
for (auto const& mec : mecs) { for (auto const& mec : mecs) {
// Create a submatrix for the current mec as well as a mapping to map back to the original states. // Create a submatrix for the current mec as well as a mapping to map back to the original states.
std::vector<uint64_t> toGlobalStateIndexMapping;
std::vector<uint64_t> toGlobalChoiceIndexMapping;
storm::storage::BitVector mecStatesAsBitVector(model.getNumberOfStates(), false); storm::storage::BitVector mecStatesAsBitVector(model.getNumberOfStates(), false);
storm::storage::BitVector mecChoicesAsBitVector(model.getNumberOfChoices(), false); storm::storage::BitVector mecChoicesAsBitVector(model.getNumberOfChoices(), false);
for (auto const& stateChoices : mec) { for (auto const& stateChoices : mec) {
mecStatesAsBitVector.set(stateChoices.first, true); mecStatesAsBitVector.set(stateChoices.first, true);
toGlobalStateIndexMapping.push_back(stateChoices.first);
for (auto const& choice : stateChoices.second) { for (auto const& choice : stateChoices.second) {
mecChoicesAsBitVector.set(choice, true); mecChoicesAsBitVector.set(choice, true);
toGlobalChoiceIndexMapping.push_back(choice);
} }
} }
std::vector<uint64_t> toGlobalStateIndexMapping(mecStatesAsBitVector.begin(), mecStatesAsBitVector.end());
std::vector<uint64_t> toGlobalChoiceIndexMapping(mecChoicesAsBitVector.begin(), mecChoicesAsBitVector.end());
//std::cout << "mec choices of ec" << ecCounter << ": " << mecChoicesAsBitVector << std::endl;
storm::storage::SparseMatrix<ValueType> mecTransitions = model.getTransitionMatrix().getSubmatrix(false, mecChoicesAsBitVector, mecStatesAsBitVector); storm::storage::SparseMatrix<ValueType> mecTransitions = model.getTransitionMatrix().getSubmatrix(false, mecChoicesAsBitVector, mecStatesAsBitVector);
// Create a variable for each subEC and add it for the corresponding states. // Create a variable for each subEC and add it for the corresponding states.
// Also assert that not every state takes an ec choice. // Also assert that not every state takes an ec choice.
auto const& subEcs = getSubEndComponents(mecTransitions);
auto subEcs = getSubEndComponents(mecTransitions);
for (auto const& subEc : subEcs) { for (auto const& subEc : subEcs) {
// get the choices of the current EC with some non-zero value (i.e. reward). // get the choices of the current EC with some non-zero value (i.e. reward).
// std::cout << "sub ec choices of ec" << ecCounter << ": " << subEc.second << std::endl;
storm::storage::BitVector subEcChoicesWithValueZero = subEc.second; storm::storage::BitVector subEcChoicesWithValueZero = subEc.second;
for (auto const& localSubEcChoiceIndex : subEc.second) { for (auto const& localSubEcChoiceIndex : subEc.second) {
uint64_t subEcChoice = toGlobalChoiceIndexMapping[localSubEcChoiceIndex]; uint64_t subEcChoice = toGlobalChoiceIndexMapping[localSubEcChoiceIndex];
@ -274,11 +273,15 @@ namespace storm {
} }
} }
// Assert that the ecVar is one iff the sum over the zero-value-choice variables equals the number of states in this ec // Assert that the ecVar is one iff the sum over the zero-value-choice variables equals the number of states in this ec
storm::expressions::Expression ecVarLowerBound = one - lpModel->getConstant(storm::utility::convertNumber<ValueType>(numSubEcStatesWithMultipleChoices)).simplify();
storm::expressions::Expression ecVarBound = one - lpModel->getConstant(storm::utility::convertNumber<ValueType>(numSubEcStatesWithMultipleChoices)).simplify();
if (!ecChoiceVars.empty()) { if (!ecChoiceVars.empty()) {
ecVarLowerBound = ecVarLowerBound + storm::expressions::sum(ecChoiceVars);
ecVarBound = ecVarBound + storm::expressions::sum(ecChoiceVars);
}
if (inOutEncoding()) {
lpModel->addConstraint("", ecVar <= ecVarBound);
} else {
lpModel->addConstraint("", ecVar >= ecVarBound);
} }
lpModel->addConstraint("", ecVar >= ecVarLowerBound);
} }
} }
} }
@ -327,7 +330,6 @@ namespace storm {
} }
} }
} }
// Create ec Variables and assert for each sub-ec that not all choice variables stay there // Create ec Variables and assert for each sub-ec that not all choice variables stay there
auto ecVars = createEcVariables(choiceVars); auto ecVars = createEcVariables(choiceVars);
bool hasEndComponents = false; bool hasEndComponents = false;
@ -353,7 +355,6 @@ namespace storm {
} }
storm::storage::BitVector nonBottomStates = ~bottomStates; storm::storage::BitVector nonBottomStates = ~bottomStates;
STORM_LOG_TRACE("Found " << bottomStates.getNumberOfSetBits() << " bottom states."); 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.");
// Compute upper bounds for each state // Compute upper bounds for each state
std::vector<ValueType> visitingTimesUpperBounds = DeterministicSchedsObjectiveHelper<ModelType>::computeUpperBoundOnExpectedVisitingTimes(model.getTransitionMatrix(), bottomStates, nonBottomStates, hasEndComponents); std::vector<ValueType> visitingTimesUpperBounds = DeterministicSchedsObjectiveHelper<ModelType>::computeUpperBoundOnExpectedVisitingTimes(model.getTransitionMatrix(), bottomStates, nonBottomStates, hasEndComponents);
@ -401,6 +402,7 @@ namespace storm {
} }
if (ecValVars[state].isInitialized()) { if (ecValVars[state].isInitialized()) {
outs[state].push_back(ecValVars[state]); outs[state].push_back(ecValVars[state]);
bottomStatesIn.push_back(ecValVars[state]);
} }
} }
@ -593,9 +595,10 @@ namespace storm {
STORM_LOG_TRACE("\tDone solving MILP..."); STORM_LOG_TRACE("\tDone solving MILP...");
swLpSolve.stop(); swLpSolve.stop();
//std::cout << "writing model to file out.lp"<< std::endl;
//lpModel->writeModelToFile("out.lp");
if (lpModel->isInfeasible()) { if (lpModel->isInfeasible()) {
infeasableAreas.push_back(polytopeTree.getPolytope()); infeasableAreas.push_back(polytopeTree.getPolytope());
lpModel->writeModelToFile("out.lp");
polytopeTree.clear(); polytopeTree.clear();
} else { } else {
STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded."); STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded.");

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

@ -220,7 +220,7 @@ namespace storm {
if (!upperResultBounds) { if (!upperResultBounds) {
upperResultBounds = computeValueBounds(env, false, model, *objective.formula); upperResultBounds = computeValueBounds(env, false, model, *objective.formula);
auto upperResultBound = objective.upperResultBound; auto upperResultBound = objective.upperResultBound;
if (storm::utility::vector::hasInfinityEntry(upperResultBounds.get())) {
if (!upperResultBound.is_initialized() && storm::utility::vector::hasInfinityEntry(upperResultBounds.get())) {
STORM_LOG_THROW(objective.formula->isRewardOperatorFormula(), storm::exceptions::NotSupportedException, "The upper bound for objective " << *objective.originalFormula << " is infinity at some state. This is only supported for reachability rewards / total rewards."); STORM_LOG_THROW(objective.formula->isRewardOperatorFormula(), storm::exceptions::NotSupportedException, "The upper bound for objective " << *objective.originalFormula << " is infinity at some state. This is only supported for reachability rewards / total rewards.");
STORM_LOG_THROW(objective.formula->getSubformula().isTotalRewardFormula() || objective.formula->getSubformula().isEventuallyFormula(), storm::exceptions::NotSupportedException, "The upper bound for objective " << *objective.originalFormula << " is infinity at some state. This is only supported for reachability rewards / total rewards."); STORM_LOG_THROW(objective.formula->getSubformula().isTotalRewardFormula() || objective.formula->getSubformula().isEventuallyFormula(), storm::exceptions::NotSupportedException, "The upper bound for objective " << *objective.originalFormula << " is infinity at some state. This is only supported for reachability rewards / total rewards.");
auto rewards = getTotalRewardVector(model, *objective.formula); auto rewards = getTotalRewardVector(model, *objective.formula);
@ -234,6 +234,7 @@ namespace storm {
} }
upperBound += expVisits[state] * maxReward; upperBound += expVisits[state] * maxReward;
} }
upperResultBound = upperBound;
} }
storm::utility::vector::clip(upperResultBounds.get(), objective.lowerResultBound, upperResultBound); storm::utility::vector::clip(upperResultBounds.get(), objective.lowerResultBound, upperResultBound);
} }
@ -292,7 +293,7 @@ namespace storm {
lpath *= minProb; lpath *= minProb;
} }
STORM_LOG_ASSERT(!storm::utility::isZero(lpath), "unexpected value of lpath"); STORM_LOG_ASSERT(!storm::utility::isZero(lpath), "unexpected value of lpath");
uint64_t mecState = mecElimination.oldToNewStateMapping[mec.begin()->first];
uint64_t mecState = modelToSubsystemStateMapping.get()[mec.begin()->first];
bool foundEntry = false; bool foundEntry = false;
for (uint64_t mecChoice = transitions.getRowGroupIndices()[mecState]; mecChoice < transitions.getRowGroupIndices()[mecState + 1]; ++mecChoice) { for (uint64_t mecChoice = transitions.getRowGroupIndices()[mecState]; mecChoice < transitions.getRowGroupIndices()[mecState + 1]; ++mecChoice) {
if (transitions.getRow(mecChoice).getNumberOfEntries() == 1) { if (transitions.getRow(mecChoice).getNumberOfEntries() == 1) {
@ -329,7 +330,7 @@ namespace storm {
++subsystemState; ++subsystemState;
} }
} }
assert(subsystemState == subsystemBounds.size());
return visitingTimesUpperBounds;
} }

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

@ -452,6 +452,10 @@ namespace storm {
GeometryValueType eps = storm::utility::convertNumber<GeometryValueType>(env.modelchecker().multi().getPrecision()); GeometryValueType eps = storm::utility::convertNumber<GeometryValueType>(env.modelchecker().multi().getPrecision());
eps += eps; // The unknown area (box) can actually have size 2*eps eps += eps; // The unknown area (box) can actually have size 2*eps
if (!wvChecker) {
lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector());
}
if (optimizeAndSplitFacet(env, f, eps)) { if (optimizeAndSplitFacet(env, f, eps)) {
return; return;
} }
@ -464,7 +468,9 @@ namespace storm {
} }
} }
if (!polytopeTree.isEmpty()) { if (!polytopeTree.isEmpty()) {
lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector());
if (wvChecker) {
lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector());
}
auto res = lpChecker->check(env, polytopeTree, eps); auto res = lpChecker->check(env, polytopeTree, eps);
for (auto const& infeasableArea : res.second) { for (auto const& infeasableArea : res.second) {
addUnachievableArea(env, infeasableArea); addUnachievableArea(env, infeasableArea);
@ -496,7 +502,7 @@ namespace storm {
point = storm::utility::vector::convertNumericVector<GeometryValueType>(wvChecker->getUnderApproximationOfInitialStateResults()); point = storm::utility::vector::convertNumericVector<GeometryValueType>(wvChecker->getUnderApproximationOfInitialStateResults());
negateMinObjectives(point); negateMinObjectives(point);
} else { } else {
auto currentArea = negateMinObjectives(overApproximation->intersection(f.getHalfspace().invert()));
auto currentArea = overApproximation->intersection(f.getHalfspace().invert());
auto optionalPoint = lpChecker->check(env, currentArea); auto optionalPoint = lpChecker->check(env, currentArea);
if (optionalPoint.is_initialized()) { if (optionalPoint.is_initialized()) {
point = std::move(optionalPoint.get()); point = std::move(optionalPoint.get());

Write Preview
Loading…
Cancel
Save