From 4ca76283197601b2664cf0e06eb1d604ec89144e Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 4 Jun 2016 18:13:26 +0200 Subject: [PATCH] bug fixes and improved debug output Former-commit-id: 9007c0acac45acff75aa2f0207dfd89dc7fb7ea4 --- ...SparseMultiObjectiveModelCheckerHelper.cpp | 11 +++++-- ...seWeightedObjectivesModelCheckerHelper.cpp | 33 +++++++++++-------- 2 files changed, 29 insertions(+), 15 deletions(-) diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp index 28eb326bd..0ecbdfb24 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp @@ -4,6 +4,7 @@ #include "src/models/sparse/Mdp.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/utility/constants.h" +#include "src/utility/vector.h" #include "src/exceptions/UnexpectedException.h" @@ -99,7 +100,7 @@ namespace storm { void SparseMultiObjectiveModelCheckerHelper::updateOverApproximation(Point const& newPoint, WeightVector const& newWeightVector) { storm::storage::geometry::Halfspace h(newWeightVector, storm::utility::vector::dotProduct(newWeightVector, newPoint)); overApproximation = overApproximation->intersection(h); - STORM_LOG_DEBUG("Updated OverApproximation to polytope " << overApproximation->toString(true)); + STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true)); } template @@ -110,6 +111,12 @@ namespace storm { paretoPointsVec.push_back(paretoPoint.first); } + STORM_LOG_WARN("REMOVE ADDING ADDITIONAL VERTICES AS SOON AS HYPRO WORKS FOR DEGENERATED POLYTOPES"); + Point p1 = {-1, 0}; + Point p2 = {0, -1}; + paretoPointsVec.push_back(p1); + paretoPointsVec.push_back(p2); + boost::optional upperBounds; if(!paretoPointsVec.empty()){ //Get the pointwise maximum of the pareto points @@ -126,7 +133,7 @@ namespace storm { } underApproximation = storm::storage::geometry::Polytope::create(paretoPointsVec)->downwardClosure(upperBounds); - STORM_LOG_DEBUG("Updated UnderApproximation to polytope " << overApproximation->toString(true)); + STORM_LOG_DEBUG("Updated UnderApproximation to " << underApproximation->toString(true)); } #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp b/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp index 7015a12e2..55d5262ca 100644 --- a/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp @@ -18,16 +18,24 @@ namespace storm { template SparseWeightedObjectivesModelCheckerHelper::SparseWeightedObjectivesModelCheckerHelper(Information const& info) : info(info), checkHasBeenCalled(false) , objectiveResults(info.objectives.size()){ - - + //Intentionally left empty } template void SparseWeightedObjectivesModelCheckerHelper::check(std::vector const& weightVector) { - + STORM_LOG_DEBUG("Checking weighted objectives with weight vector " << std::endl << "\t" << weightVector); unboundedWeightedPhase(weightVector); + STORM_LOG_DEBUG("Unbounded weighted phase resulted in " << std::endl << "\t Result: " << weightedResult << std::endl << "\t Scheduler: " << scheduler); unboundedIndividualPhase(weightVector); + STORM_LOG_DEBUG("Unbounded individual phase resulted in..."); + for(uint_fast64_t objIndex = 0; objIndex < info.objectives.size(); ++objIndex) { + STORM_LOG_DEBUG("\t objective " << objIndex << ":" << objectiveResults[objIndex]); + } boundedPhase(weightVector); + STORM_LOG_DEBUG("Bounded phase resulted in..."); + for(uint_fast64_t objIndex = 0; objIndex < info.objectives.size(); ++objIndex) { + STORM_LOG_DEBUG("\t objective " << objIndex << ":" << objectiveResults[objIndex]); + } checkHasBeenCalled=true; } @@ -60,13 +68,7 @@ namespace storm { // TODO check for +/- infty reward... - - //Testing.. - storm::storage::BitVector test(64); - test.set(63); - std::cout << "Test set index with 0: " << test.getNextSetIndex(0) << std::endl; - std::cout << "Test set index with 63: " << test.getNextSetIndex(63) << std::endl; - std::cout << "Test set index with 64: " << test.getNextSetIndex(64) << std::endl; + //std::cout << "weighted reward vector is " << storm::utility::vector::toString(weightedRewardVector) << std::endl; storm::storage::BitVector actionsWithRewards = storm::utility::vector::filter(weightedRewardVector, [&] (ValueType const& value) -> bool {return !storm::utility::isZero(value);}); storm::storage::BitVector statesWithRewards(info.preprocessedModel.getNumberOfStates(), false); @@ -95,17 +97,17 @@ namespace storm { info.preprocessedModel.getBackwardTransitions(), storm::storage::BitVector(info.preprocessedModel.getNumberOfStates(), true), statesWithRewards); - this->weightedResult = std::vector(info.preprocessedModel.getNumberOfStates()); this->scheduler = storm::storage::TotalScheduler(info.preprocessedModel.getNumberOfStates()); storm::storage::SparseMatrix submatrix = info.preprocessedModel.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false); std::vector b(submatrix.getRowCount()); - storm::utility::vector::selectVectorValues(b, maybeStates, weightedRewardVector); + storm::utility::vector::selectVectorValues(b, maybeStates, info.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), weightedRewardVector); std::vector x(submatrix.getRowGroupCount(), storm::utility::zero()); storm::utility::solver::MinMaxLinearEquationSolverFactory solverFactory; std::unique_ptr> solver = solverFactory.create(submatrix, true); + solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->solveEquationSystem(x, b); storm::utility::vector::setVectorValues(this->weightedResult, maybeStates, x); @@ -117,7 +119,6 @@ namespace storm { ++currentSubState; } // Note that the choices for the ~maybeStates are arbitrary as no states with rewards are reachable any way. - } template @@ -128,16 +129,22 @@ namespace storm { std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); storm::utility::solver::LinearEquationSolverFactory linearEquationSolverFactory; //TODO check if all but one entry of weightVector is zero + //Also only compute values for objectives with weightVector != zero, + //one check can be omitted as the result can be computed back from the weighed result and the results from the remaining objectives for(uint_fast64_t objIndex = 0; objIndex < weightVector.size(); ++objIndex) { if(!info.objectives[objIndex].stepBound){ storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), info.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), info.preprocessedModel.getRewardModel(info.objectives[objIndex].rewardModelName).getStateActionRewardVector()); + //std::cout << "stateActionRewardVector for objective " << objIndex << " is " << storm::utility::vector::toString(info.preprocessedModel.getRewardModel(info.objectives[objIndex].rewardModelName).getStateActionRewardVector()) << std::endl; + //std::cout << "deterministic state rewards for objective " << objIndex << " are " << storm::utility::vector::toString(deterministicStateRewards) << std::endl; + storm::storage::BitVector statesWithRewards = storm::utility::vector::filter(deterministicStateRewards, [&] (ValueType const& value) -> bool {return !storm::utility::isZero(value);}); // As target states, we take the states from which no reward is reachable. STORM_LOG_WARN("TODO: target state selection is currently only valid for reachability properties..."); //TODO: we should be able to give some hint to the solver.. storm::storage::BitVector targetStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); + targetStates.complement(); objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(deterministicMatrix, deterministicBackwardTransitions, deterministicStateRewards,