From e70f7716fe6402232637446fe85456ee9c1bdb10 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 10 Feb 2017 17:29:37 +0100 Subject: [PATCH] Fixed minor pcaa bugs that were introduced due to recent changes --- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 16 +-- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 116 +++++++++--------- 2 files changed, 65 insertions(+), 67 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index b1c29d25b..df2864b34 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -358,14 +358,10 @@ namespace storm { // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b); auto newScheduler = minMax.solver->getScheduler(); - if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) { + if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives optimalChoicesAtCurrentEpoch = newScheduler->getChoices(); - auto objIndex = *consideredObjectives.begin(); - PS.objectiveSolutionVectors[objIndex] = PS.weightedSolutionVector; - if(!storm::utility::isOne(weightVector[objIndex])) { - storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[objIndex], storm::utility::one()/weightVector[objIndex]); - } + PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector; } else { // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed if(linEq.solver == nullptr || newScheduler->getChoices() != optimalChoicesAtCurrentEpoch) { @@ -407,13 +403,9 @@ namespace storm { storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector); MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues); storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector); - if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) { + if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives - auto objIndex = *consideredObjectives.begin(); - MS.objectiveSolutionVectors[objIndex] = MS.weightedSolutionVector; - if(!storm::utility::isOne(weightVector[objIndex])) { - storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[objIndex], storm::utility::one()/weightVector[objIndex]); - } + MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector; } else { for(auto objIndex : consideredObjectives) { MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 6a353d580..64d067d1e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -158,65 +158,71 @@ namespace storm { template void SparsePcaaWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { - - if(objectivesWithNoUpperTimeBound.getNumberOfSetBits()==1) { - auto objIndex = *objectivesWithNoUpperTimeBound.begin(); - objectiveResults[objIndex] = weightedResult; - if(!storm::utility::isZero(weightVector[objIndex])) { - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one()/weightVector[objIndex]); - } + if(objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { + objectiveResults[*objectivesWithNoUpperTimeBound.begin()] = weightedResult; for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) { - if(objIndex != objIndex2) { + if(*objectivesWithNoUpperTimeBound.begin() != objIndex2) { objectiveResults[objIndex2] = std::vector(model.getNumberOfStates(), storm::utility::zero()); } } - } else { - storm::storage::SparseMatrix deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); - storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); - std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); - storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - - // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far. - // Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i. - std::vector weightedSumOfUncheckedObjectives = weightedResult; - ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound); - - for(uint_fast64_t const& objIndex : storm::utility::vector::getSortedIndices(weightVector)) { - if(objectivesWithNoUpperTimeBound.get(objIndex)){ - offsetsToLowerBound[objIndex] = storm::utility::zero(); - offsetsToUpperBound[objIndex] = storm::utility::zero(); - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); - storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); - // As target states, we pick the states from which no reward is reachable. - storm::storage::BitVector targetStates = ~storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); - - // Compute the estimate for this objective - if(!storm::utility::isZero(weightVector[objIndex])) { - objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one() / sumOfWeightsOfUncheckedObjectives); - } - - // Make sure that the objectiveResult is initialized in some way - objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero()); - - // Invoke the linear equation solver - objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(deterministicMatrix, - deterministicBackwardTransitions, - deterministicStateRewards, - targetStates, - false, //no qualitative checking, - linearEquationSolverFactory, - objectiveResults[objIndex]); - // Update the estimate for the next objectives. - if(!storm::utility::isZero(weightVector[objIndex])) { - storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]); - sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex]; - } - } else { - objectiveResults[objIndex] = std::vector(model.getNumberOfStates(), storm::utility::zero()); - } - } - } + } else { + storm::storage::SparseMatrix deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); + storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); + std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); + storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; + + // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far. + // Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i. + std::vector weightedSumOfUncheckedObjectives = weightedResult; + ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound); + + for (uint_fast64_t const &objIndex : storm::utility::vector::getSortedIndices(weightVector)) { + if (objectivesWithNoUpperTimeBound.get(objIndex)) { + offsetsToLowerBound[objIndex] = storm::utility::zero(); + offsetsToUpperBound[objIndex] = storm::utility::zero(); + storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); + storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); + // As maybestates we pick the states from which a state with reward is reachable + storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); + + // Compute the estimate for this objective + if (!storm::utility::isZero(weightVector[objIndex])) { + objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; + storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one() / sumOfWeightsOfUncheckedObjectives); + } + // Make sure that the objectiveResult is initialized correctly + objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero()); + + if (!maybeStates.empty()) { + storm::storage::SparseMatrix submatrix = deterministicMatrix.getSubmatrix( + true, maybeStates, maybeStates, true); + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + + // Prepare solution vector and rhs of the equation system. + std::vector x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates); + std::vector b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates); + + // Now solve the resulting equation system. + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + solver->solveEquations(x, b); + + // Set the result for this objective accordingly + storm::utility::vector::setVectorValues(objectiveResults[objIndex], maybeStates, x); + storm::utility::vector::setVectorValues(objectiveResults[objIndex], ~maybeStates, storm::utility::zero()); + } + + // Update the estimate for the next objectives. + if (!storm::utility::isZero(weightVector[objIndex])) { + storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]); + sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex]; + } + } else { + objectiveResults[objIndex] = std::vector(model.getNumberOfStates(), storm::utility::zero()); + } + } + } } template