From 53402293d619c47be22d538840d8fea21b5f28c1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 16 Feb 2017 15:32:59 +0100 Subject: [PATCH] no maximal end component decomposition for multi-obj model checking when it is not necessary. --- .../modelchecker/multiobjective/pcaa.cpp | 2 +- .../pcaa/SparsePcaaParetoQuery.cpp | 1 + .../pcaa/SparsePcaaPreprocessor.cpp | 22 +++++++++++-------- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 2 ++ .../pcaa/SparsePcaaWeightVectorChecker.cpp | 8 ++++--- 5 files changed, 22 insertions(+), 13 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp index b7ca7cbc4..ff9e84966 100644 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa.cpp @@ -31,7 +31,7 @@ namespace storm { } auto preprocessorResult = SparsePcaaPreprocessor::preprocess(model, formula); - STORM_LOG_DEBUG("Preprocessing done. Result: " << preprocessorResult); + STORM_LOG_INFO("Preprocessing done. Result: " << preprocessorResult); std::unique_ptr> query; switch (preprocessorResult.queryType) { diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 639589592..23da39876 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -81,6 +81,7 @@ namespace storm { return; } STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber(farestDistance)); + std::cout << "Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber(farestDistance) << std::endl; WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector(); this->performRefinementStep(std::move(direction)); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 125e12a1e..889110a56 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -27,7 +27,7 @@ namespace storm { //Invoke preprocessing on the individual objectives for(auto const& subFormula : originalFormula.getSubformulas()){ - STORM_LOG_DEBUG("Preprocessing objective " << *subFormula<< "."); + STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); result.objectives.emplace_back(); PcaaObjective& currentObjective = result.objectives.back(); currentObjective.originalFormula = subFormula; @@ -37,7 +37,6 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); } } - // Set the query type. In case of a quantitative query, also set the index of the objective to be optimized. // Note: If there are only zero (or one) objectives left, we should not consider a pareto query! storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size()); @@ -55,13 +54,13 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievability query), 1 (quantitative query), or " << result.objectives.size() << " (Pareto Query). Got " << numOfObjectivesWithoutThreshold << " instead."); } - + //We can remove the original reward models to save some memory std::set origRewardModels = originalFormula.getReferencedRewardModels(); for (auto const& rewModel : origRewardModels){ result.preprocessedModel.removeRewardModel(rewModel); } - + //Get actions to which a positive or negative reward is assigned for at least one objective result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); @@ -74,11 +73,16 @@ namespace storm { } } } - - auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); - analyzeEndComponents(result, backwardTransitions); - ensureRewardFiniteness(result, backwardTransitions); - + + // Analyze End components and ensure reward finiteness. + // Note that this is only necessary if there is at least one objective with no upper time bound + for (auto const& obj : result.objectives) { + if(!obj.upperTimeBound) { + auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); + analyzeEndComponents(result, backwardTransitions); + ensureRewardFiniteness(result, backwardTransitions); + } + } return result; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 5bc096c93..42bd16b9a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -121,6 +121,7 @@ namespace storm { } overApproximation = overApproximation->intersection(h); STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true)); + std::cout << "Updated OverApproximation to " << overApproximation->toString(true) << std::endl; } template @@ -132,6 +133,7 @@ namespace storm { } underApproximation = storm::storage::geometry::Polytope::createDownwardClosure(paretoPoints); STORM_LOG_DEBUG("Updated UnderApproximation to " << underApproximation->toString(true)); + std::cout << "Updated UnderApproximation to " << underApproximation->toString(true) << std::endl; } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 64d067d1e..fb5c2e6b6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -50,7 +50,7 @@ namespace storm { template void SparsePcaaWeightVectorChecker::check(std::vector const& weightVector) { checkHasBeenCalled=true; - STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVector))); + STORM_LOG_INFO("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVector))); std::vector weightedRewardVector(model.getTransitionMatrix().getRowCount(), storm::utility::zero()); for(auto objIndex : objectivesWithNoUpperTimeBound) { storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); @@ -64,7 +64,7 @@ namespace storm { break; } } - STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(getLowerBoundsOfInitialStateResults()))); + STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(getLowerBoundsOfInitialStateResults()))); // Validate that the results are sufficiently precise ValueType resultingWeightedPrecision = storm::utility::vector::dotProduct(getUpperBoundsOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getLowerBoundsOfInitialStateResults(), weightVector); STORM_LOG_THROW(resultingWeightedPrecision >= storm::utility::zero(), storm::exceptions::UnexpectedException, "The distance between the lower and the upper result is negative."); @@ -146,8 +146,10 @@ namespace storm { std::unique_ptr> solver = solverFactory.create(ecEliminatorResult.matrix); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->setTrackScheduler(true); + std::cout << "invoked minmaxsolver" << std::endl; solver->solveEquations(subResult, subRewardVector); - + std::cout << "minmaxsolver done" << std::endl; + this->weightedResult = std::vector(model.getNumberOfStates()); std::vector optimalChoices(model.getNumberOfStates());