diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index 80e99295b..fee459534 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -55,7 +55,6 @@ namespace storm { 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; } @@ -168,8 +167,8 @@ namespace storm { std::map getSubEndComponents(storm::storage::SparseMatrix const& mecTransitions) { auto backwardTransitions = mecTransitions.transpose(true); std::map 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; while (!unprocessed.empty()) { auto currentIt = unprocessed.begin(); @@ -212,25 +211,25 @@ namespace storm { for (auto const& mec : mecs) { // Create a submatrix for the current mec as well as a mapping to map back to the original states. - std::vector toGlobalStateIndexMapping; - std::vector toGlobalChoiceIndexMapping; storm::storage::BitVector mecStatesAsBitVector(model.getNumberOfStates(), false); storm::storage::BitVector mecChoicesAsBitVector(model.getNumberOfChoices(), false); for (auto const& stateChoices : mec) { mecStatesAsBitVector.set(stateChoices.first, true); - toGlobalStateIndexMapping.push_back(stateChoices.first); for (auto const& choice : stateChoices.second) { mecChoicesAsBitVector.set(choice, true); - toGlobalChoiceIndexMapping.push_back(choice); } } + std::vector toGlobalStateIndexMapping(mecStatesAsBitVector.begin(), mecStatesAsBitVector.end()); + std::vector toGlobalChoiceIndexMapping(mecChoicesAsBitVector.begin(), mecChoicesAsBitVector.end()); + //std::cout << "mec choices of ec" << ecCounter << ": " << mecChoicesAsBitVector << std::endl; storm::storage::SparseMatrix mecTransitions = model.getTransitionMatrix().getSubmatrix(false, mecChoicesAsBitVector, mecStatesAsBitVector); // Create a variable for each subEC and add it for the corresponding states. // Also assert that not every state takes an ec choice. - auto const& subEcs = getSubEndComponents(mecTransitions); + auto subEcs = getSubEndComponents(mecTransitions); for (auto const& subEc : subEcs) { // 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; for (auto const& localSubEcChoiceIndex : subEc.second) { 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 - storm::expressions::Expression ecVarLowerBound = one - lpModel->getConstant(storm::utility::convertNumber(numSubEcStatesWithMultipleChoices)).simplify(); + storm::expressions::Expression ecVarBound = one - lpModel->getConstant(storm::utility::convertNumber(numSubEcStatesWithMultipleChoices)).simplify(); 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 auto ecVars = createEcVariables(choiceVars); bool hasEndComponents = false; @@ -353,7 +355,6 @@ namespace storm { } 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."); // Compute upper bounds for each state std::vector visitingTimesUpperBounds = DeterministicSchedsObjectiveHelper::computeUpperBoundOnExpectedVisitingTimes(model.getTransitionMatrix(), bottomStates, nonBottomStates, hasEndComponents); @@ -401,6 +402,7 @@ namespace storm { } if (ecValVars[state].isInitialized()) { outs[state].push_back(ecValVars[state]); + bottomStatesIn.push_back(ecValVars[state]); } } @@ -593,9 +595,10 @@ namespace storm { STORM_LOG_TRACE("\tDone solving MILP..."); swLpSolve.stop(); + //std::cout << "writing model to file out.lp"<< std::endl; + //lpModel->writeModelToFile("out.lp"); if (lpModel->isInfeasible()) { infeasableAreas.push_back(polytopeTree.getPolytope()); - lpModel->writeModelToFile("out.lp"); polytopeTree.clear(); } else { STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded."); diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp index 756963a07..aa1a6dd7e 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp @@ -220,7 +220,7 @@ namespace storm { if (!upperResultBounds) { upperResultBounds = computeValueBounds(env, false, model, *objective.formula); 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->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); @@ -234,6 +234,7 @@ namespace storm { } upperBound += expVisits[state] * maxReward; } + upperResultBound = upperBound; } storm::utility::vector::clip(upperResultBounds.get(), objective.lowerResultBound, upperResultBound); } @@ -292,7 +293,7 @@ namespace storm { lpath *= minProb; } 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; for (uint64_t mecChoice = transitions.getRowGroupIndices()[mecState]; mecChoice < transitions.getRowGroupIndices()[mecState + 1]; ++mecChoice) { if (transitions.getRow(mecChoice).getNumberOfEntries() == 1) { @@ -329,7 +330,7 @@ namespace storm { ++subsystemState; } } - assert(subsystemState == subsystemBounds.size()); + return visitingTimesUpperBounds; } diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index b1e7398c2..dda3b2c0f 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -452,6 +452,10 @@ namespace storm { GeometryValueType eps = storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); eps += eps; // The unknown area (box) can actually have size 2*eps + if (!wvChecker) { + lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector()); + } + if (optimizeAndSplitFacet(env, f, eps)) { return; } @@ -464,7 +468,9 @@ namespace storm { } } if (!polytopeTree.isEmpty()) { - lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector()); + if (wvChecker) { + lpChecker->setCurrentWeightVector(f.getHalfspace().normalVector()); + } auto res = lpChecker->check(env, polytopeTree, eps); for (auto const& infeasableArea : res.second) { addUnachievableArea(env, infeasableArea); @@ -496,7 +502,7 @@ namespace storm { point = storm::utility::vector::convertNumericVector(wvChecker->getUnderApproximationOfInitialStateResults()); negateMinObjectives(point); } else { - auto currentArea = negateMinObjectives(overApproximation->intersection(f.getHalfspace().invert())); + auto currentArea = overApproximation->intersection(f.getHalfspace().invert()); auto optionalPoint = lpChecker->check(env, currentArea); if (optionalPoint.is_initialized()) { point = std::move(optionalPoint.get());