diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index 70289b5da..919328b9a 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -34,7 +34,7 @@ namespace storm { template std::unique_ptr SparseMdpMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { - auto preprocessedData = helper::SparseMdpMultiObjectivePreprocessingHelper::preprocess(checkTask.getFormula(), this->getModel()); + auto preprocessedData = helper::SparseMultiObjectivePreprocessor::preprocess(checkTask.getFormula(), this->getModel()); std::cout << std::endl; std::cout << "Preprocessing done." << std::endl; preprocessedData.printToStream(std::cout); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp index f90cc6d01..65b2c3123 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp @@ -18,8 +18,8 @@ namespace storm { template typename SparseMultiObjectiveHelper::ReturnType SparseMultiObjectiveHelper::check(PreprocessorData const& data) { ReturnType result; - result.overApproximation = storm::storage::geometry::Polytope::createUniversalPolytope(); - result.underApproximation = storm::storage::geometry::Polytope::createEmptyPolytope(); + result.overApproximation() = storm::storage::geometry::Polytope::createUniversalPolytope(); + result.underApproximation() = storm::storage::geometry::Polytope::createEmptyPolytope(); uint_fast64_t numOfObjectivesWithoutThreshold = 0; for(auto const& obj : data.objectives) { @@ -50,22 +50,17 @@ namespace storm { } storm::storage::BitVector individualObjectivesToBeChecked(data.objectives.size(), true); - bool converged=false; SparseMultiObjectiveWeightVectorChecker weightVectorChecker(data); do { - WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation, individualObjectivesToBeChecked); - refineResult(separatingVector, weightVectorChecker, result); - // Check for convergence - if(!checkIfThresholdsAreSatisfied(overApproximation, thresholds, strictThresholds)){ - result.thresholdsAreAchievable = false; - converged=true; + WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation(), individualObjectivesToBeChecked); + performRefinementStep(separatingVector, data.produceSchedulers, weightVectorChecker, result); + if(!checkIfThresholdsAreSatisfied(result.overApproximation(), thresholds, strictThresholds)){ + result.setThresholdsAreAchievable(false); } - if(checkIfThresholdsAreSatisfied(underApproximation, thresholds, strictThresholds)){ - result.thresholdsAreAchievable = true; - converged=true; + if(checkIfThresholdsAreSatisfied(result.underApproximation(), thresholds, strictThresholds)){ + result.setThresholdsAreAchievable(true); } - converged |= (storm::settings::getModule().isMaxIterationsSet() && result.iterations.size() >= storm::settings::getModule().getMaxIterations()); - } while(!converged); + } while(!result.isThresholdsAreAchievableSet() && !maxStepsPerformed(result)); } template @@ -96,68 +91,61 @@ namespace storm { storm::storage::BitVector individualObjectivesToBeChecked(data.objectives.size(), true); individualObjectivesToBeChecked.set(optimizingObjIndex, false); SparseMultiObjectiveWeightVectorChecker weightVectorChecker(data); - bool converged=false; do { - WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation, individualObjectivesToBeChecked); - refineResult(separatingVector, weightVectorChecker, result); + WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation(), individualObjectivesToBeChecked); + performRefinementStep(separatingVector, data.produceSchedulers, weightVectorChecker, result); //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded - thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], iterations.back().point[optimizingObjIndex]); - if(!checkIfThresholdsAreSatisfied(overApproximation, thresholds, strictThresholds)){ - result.thresholdsAreAchievable = false; - converged=true; + thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], result.refinementSteps().back().getPoint()[optimizingObjIndex]); + if(!checkIfThresholdsAreSatisfied(result.overApproximation(), thresholds, strictThresholds)){ + result.setThresholdsAreAchievable(false); } - if(checkIfThresholdsAreSatisfied(underApproximation, thresholds, strictThresholds)){ - result.thresholdsAreAchievable = true; - converged=true; + if(checkIfThresholdsAreSatisfied(result.underApproximation(), thresholds, strictThresholds)){ + result.setThresholdsAreAchievable(true); } - } while(!converged); - if(*result.thresholdsAreAchievable) { + } while(!result.isThresholdsAreAchievableSet() && !maxStepsPerformed(result)); + if(result.getThresholdsAreAchievable()) { STORM_LOG_DEBUG("Found a solution that satisfies the objective thresholds."); individualObjectivesToBeChecked.clear(); // Improve the found solution. // Note that we do not have to care whether a threshold is strict anymore, because the resulting optimum should be // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds. - converged = false; - do { - std::pair optimizationRes = underApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); + while(true) { + std::pair optimizationRes = result.underApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty."); thresholds[optimizingObjIndex] = optimizationRes.first[optimizingObjIndex]; - STORM_LOG_DEBUG("Best solution found so far is " << storm::utility::convertNumber(thresholds[optimizingObjIndex]) << "."); + result.setNumericalResult(thresholds[optimizingObjIndex]); + STORM_LOG_DEBUG("Best solution found so far is " << result.template getNumericalResult() << "."); //Compute an upper bound for the optimum and check for convergence - optimizationRes = overApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); + optimizationRes = result.overApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); if(optimizationRes.second) { - result.precisionOfResult = optimizationRes.first[optimizingObjIndex]; - thresholds[optimizingObjIndex]; - STORM_LOG_DEBUG("Solution can be improved by at most " << storm::utility::convertNumber(*result.precisionOfResult)); - if(storm::utility::convertNumber(*result.precisionOfResult) < storm::settings::getModule().getPrecision()) { - result.numericalResult = thresholds[optimizingObjIndex]; - result.optimumIsAchievable = checkIfThresholdsAreSatisfied(underApproximation, thresholds, strictThresholds); - converged=true; - } + result.setPrecisionOfResult(optimizationRes.first[optimizingObjIndex] - thresholds[optimizingObjIndex]); + STORM_LOG_DEBUG("Solution can be improved by at most " << result.template getPrecisionOfResult()); } - converged |= (storm::settings::getModule().isMaxIterationsSet() && result.iterations.size() >= storm::settings::getModule().getMaxIterations()); - if(!converged) { - WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation, individualObjectivesToBeChecked); - refineResult(separatingVector, weightVectorChecker, result); + if(targetPrecisionReached(result) || maxStepsPerformed(result)) { + result.setOptimumIsAchievable(checkIfThresholdsAreSatisfied(result.underApproximation(), thresholds, strictThresholds)); + break; } - } while(!converged); + WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation(), individualObjectivesToBeChecked); + performRefinementStep(separatingVector, data.produceSchedulers, weightVectorChecker, result); + } } } template void SparseMultiObjectiveHelper::paretoQuery(PreprocessorData const& data, ReturnType& result) { + SparseMultiObjectiveWeightVectorChecker weightVectorChecker(data); //First consider the objectives individually - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { + for(uint_fast64_t objIndex = 0; objIndex()); direction[objIndex] = storm::utility::one(); - refineResult(direction, weightVectorChecker, result); + performRefinementStep(direction, data.produceSchedulers, weightVectorChecker, result); } - bool converged=false; - do { + while(true) { // Get the halfspace of the underApproximation with maximal distance to a vertex of the overApproximation - std::vector> underApproxHalfspaces = result.underApproximation->getHalfspaces(); - std::vector overApproxVertices = result.overApproximation->getVertices(); + std::vector> underApproxHalfspaces = result.underApproximation()->getHalfspaces(); + std::vector overApproxVertices = result.overApproximation()->getVertices(); uint_fast64_t farestHalfspaceIndex = underApproxHalfspaces.size(); RationalNumberType farestDistance = storm::utility::zero(); for(uint_fast64_t halfspaceIndex = 0; halfspaceIndex < underApproxHalfspaces.size(); ++halfspaceIndex) { @@ -169,32 +157,18 @@ namespace storm { } } } - STORM_LOG_DEBUG("Farest distance between under- and overApproximation is " << storm::utility::convertNumber(farestDistance)); - if(storm::utility::convertNumber(farestDistance) < storm::settings::getModule().getPrecision()) { - result.precisionOfResult = farestDistance; - converged = true; - } - converged |= (storm::settings::getModule().isMaxIterationsSet() && result.iterations.size() >= storm::settings::getModule().getMaxIterations()); - if(!converged) { - WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector(); - refineResult(direction, weightVectorChecker, result); + result.setPrecisionOfResult(farestDistance); + STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is " << result.template getPrecisionOfResult()); + if(targetPrecisionReached(result) || maxStepsPerformed(result)) { + break; } - } while(!converged); - } - - - template - void SparseMultiObjectiveHelper::refineResult(WeightVector const& direction, SparseWeightedObjectivesModelCheckerHelper const& weightedObjectivesChecker, ReturnType& result) { - weightedObjectivesChecker.check(storm::utility::vector::convertNumericVector(direction)); - STORM_LOG_DEBUG("Result with weighted objectives is " << weightedObjectivesChecker.getInitialStateResultOfObjectives()); - result.iterations.emplace_back(direction, storm::utility::vector::convertNumericVector(weightedObjectivesChecker.getInitialStateResultOfObjectives()), weightedObjectivesChecker.getScheduler()); - - updateOverApproximation(result.iterations.back().point, result.iterations.back().weightVector); - updateUnderApproximation(); + WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector(); + performRefinementStep(direction, data.produceSchedulers, weightVectorChecker, result); + } } template - typename SparseMultiObjectiveHelper::WeightVector SparseMultiObjectiveHelper::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) const { + typename SparseMultiObjectiveHelper::WeightVector SparseMultiObjectiveHelper::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) { STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::convertNumericVector(pointToBeSeparated) << "."); if(underApproximation->isEmpty()) { @@ -206,62 +180,74 @@ namespace storm { return result; } - // Reaching this point means that the underApproximation contains halfspaces. - // The seperating vector has to be the normal vector of one of these halfspaces. + // Reaching this point means that the underApproximation contains halfspaces. The seperating vector has to be the normal vector of one of these halfspaces. // We pick one with maximal distance to the given point. However, weight vectors that correspond to checking individual objectives take precedence. std::vector> halfspaces = underApproximation->getHalfspaces(); - uint_fast64_t farestHalfspaceIndex = 0; - // Note that we are looking for a halfspace that does not contain the point. Thus, the returned distances are negative. - RationalNumberType farestDistance = -halfspaces[farestHalfspaceIndex].euclideanDistance(pointToBeSeparated); - storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero(halfspaces[farestHalfspaceIndex].normalVector()); - bool foundSeparatingSingleObjectiveVector = nonZeroVectorEntries.getNumberOfSetBits()==1 && individualObjectivesToBeChecked.get(nonZeroVectorEntries.getNextSetIndex(0)) && farestDistance>storm::utility::zero(); - - for(uint_fast64_t halfspaceIndex = 1; halfspaceIndex < halfspaces.size(); ++halfspaceIndex) { + uint_fast64_t farestHalfspaceIndex = halfspaces.size(); + RationalNumberType farestDistance = -storm::utility::one(); + bool foundSeparatingSingleObjectiveVector = false; + for(uint_fast64_t halfspaceIndex = 0; halfspaceIndex < halfspaces.size(); ++halfspaceIndex) { + // Note that we are looking for a halfspace that does not contain the point. Thus, the returned distances are negated. RationalNumberType distance = -halfspaces[halfspaceIndex].euclideanDistance(pointToBeSeparated); - nonZeroVectorEntries = ~storm::utility::vector::filterZero(halfspaces[farestHalfspaceIndex].normalVector()); - bool isSeparatingSingleObjectiveVector = nonZeroVectorEntries.getNumberOfSetBits() == 1 && individualObjectivesToBeChecked.get(nonZeroVectorEntries.getNextSetIndex(0)) && distance>storm::utility::zero(); - // Check if this halfspace is 'better' than the current one - if((!foundSeparatingSingleObjectiveVector && isSeparatingSingleObjectiveVector ) || (foundSeparatingSingleObjectiveVector==isSeparatingSingleObjectiveVector && distance>farestDistance)) { - foundSeparatingSingleObjectiveVector |= isSeparatingSingleObjectiveVector; - farestHalfspaceIndex = halfspaceIndex; - farestDistance = distance; + if(distance >= storm::utility::zero()) { + storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero(halfspaces[halfspaceIndex].normalVector()); + bool isSingleObjectiveVector = nonZeroVectorEntries.getNumberOfSetBits() == 1 && individualObjectivesToBeChecked.get(nonZeroVectorEntries.getNextSetIndex(0)); + // Check if this halfspace is better than the current one + if((!foundSeparatingSingleObjectiveVector && isSingleObjectiveVector ) || (foundSeparatingSingleObjectiveVector==isSingleObjectiveVector && distance>farestDistance)) { + foundSeparatingSingleObjectiveVector = foundSeparatingSingleObjectiveVector || isSingleObjectiveVector; + farestHalfspaceIndex = halfspaceIndex; + farestDistance = distance; + } } } if(foundSeparatingSingleObjectiveVector) { - nonZeroVectorEntries = ~storm::utility::vector::filterZero(halfspaces[farestHalfspaceIndex].normalVector()); + storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero(halfspaces[farestHalfspaceIndex].normalVector()); individualObjectivesToBeChecked.set(nonZeroVectorEntries.getNextSetIndex(0), false); } - STORM_LOG_THROW(farestDistance>=storm::utility::zero(), storm::exceptions::UnexpectedException, "There is no seperating vector."); + STORM_LOG_THROW(farestHalfspaceIndex(halfspaces[farestHalfspaceIndex].normalVector()) << "."); return halfspaces[farestHalfspaceIndex].normalVector(); } template - void SparseMultiObjectiveHelper::updateOverApproximation(std::vector const& iterations, std::shared_ptr>& overApproximation) { - storm::storage::geometry::Halfspace h(iterations.back().weightVector, storm::utility::vector::dotProduct(iterations.back().weightVector, iterations.back().point)); + void SparseMultiObjectiveHelper::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker& weightVectorChecker, ReturnType& result) { + weightVectorChecker.check(storm::utility::vector::convertNumericVector(direction)); + STORM_LOG_DEBUG("weighted objectives checker result is " << weightVectorChecker.getInitialStateResultOfObjectives()); + if(saveScheduler) { + result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives(), weightVectorChecker.getScheduler()); + } else { + result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives()); + } + updateOverApproximation(result.refinementSteps(), result.overApproximation()); + updateUnderApproximation(result.refinementSteps(), result.underApproximation()); + } + + template + void SparseMultiObjectiveHelper::updateOverApproximation(std::vector const& refinementSteps, std::shared_ptr>& overApproximation) { + storm::storage::geometry::Halfspace h(refinementSteps.back().getWeightVector(), storm::utility::vector::dotProduct(refinementSteps.back().getWeightVector(), refinementSteps.back().getPoint())); // Due to numerical issues, it might be the case that the updated overapproximation does not contain the underapproximation, // e.g., when the new point is strictly contained in the underapproximation. Check if this is the case. RationalNumberType maximumOffset = h.offset(); - for(auto const& iteration : iterations){ - maximumOffset = std::max(maximumOffset, storm::utility::vector::dotProduct(h.normalVector(), iteration.point)); + for(auto const& step : refinementSteps){ + maximumOffset = std::max(maximumOffset, storm::utility::vector::dotProduct(h.normalVector(), step.getPoint())); } if(maximumOffset > h.offset()){ // We correct the issue by shifting the halfspace such that it contains the underapproximation h.offset() = maximumOffset; - STORM_LOG_WARN("Numerical issues: The overapproximation would not contain the underapproximation. Hence, a halfspace is shifted by " << storm::utility::convertNumber(h.euclideanDistance(iterations.back().point)) << "."); + STORM_LOG_WARN("Numerical issues: The overapproximation would not contain the underapproximation. Hence, a halfspace is shifted by " << storm::utility::convertNumber(h.euclideanDistance(refinementSteps.back().getPoint())) << "."); } overApproximation = overApproximation->intersection(h); STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true)); } template - void SparseMultiObjectiveHelper::updateUnderApproximation(std::vector const& iterations, std::shared_ptr>& underApproximation) { + void SparseMultiObjectiveHelper::updateUnderApproximation(std::vector const& refinementSteps, std::shared_ptr>& underApproximation) { std::vector paretoPointsVec; - paretoPointsVec.reserve(iterations.size()); - for(auto const& iteration : iterations) { - paretoPointsVec.push_back(iterations.point); + paretoPointsVec.reserve(refinementSteps.size()); + for(auto const& step : refinementSteps) { + paretoPointsVec.push_back(step.getPoint()); } STORM_LOG_WARN("REMOVE ADDING ADDITIONAL VERTICES AS SOON AS HYPRO WORKS FOR DEGENERATED POLYTOPES"); @@ -299,7 +285,7 @@ namespace storm { } template - bool SparseMultiObjectiveHelper::checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) const { + bool SparseMultiObjectiveHelper::checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) { std::vector> halfspaces = polytope->getHalfspaces(); for(auto const& h : halfspaces) { RationalNumberType distance = h.distance(thresholds); @@ -319,6 +305,20 @@ namespace storm { return true; } + template + bool SparseMultiObjectiveHelper::targetPrecisionReached(ReturnType& result) { + result.setTargetPrecisionReached(result.isPrecisionOfResultSet() && + result.getPrecisionOfResult() < storm::utility::convertNumber(storm::settings::getModule().getPrecision())); + return result.getTargetPrecisionReached(); + } + + template + bool SparseMultiObjectiveHelper::maxStepsPerformed(ReturnType& result) { + result.setMaxStepsPerformed(storm::settings::getModule().isMaxStepsSet() && + result.refinementSteps().size() >= storm::settings::getModule().getMaxSteps()); + return result.getMaxStepsPerformed(); + } + #ifdef STORM_HAVE_CARL template class SparseMultiObjectiveHelper, storm::RationalNumber>; #endif diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h index f6263ace3..0d13bdb00 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h @@ -2,6 +2,8 @@ #define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_ #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h" #include "src/modelchecker/multiObjective/helper/SparseMultiObjectiveWeightVectorChecker.h" #include "src/storage/geometry/Polytope.h" #include "src/storage/TotalScheduler.h" @@ -14,13 +16,13 @@ namespace storm { template class SparseMultiObjectiveHelper { public: - typedef SpaseMultiObjectivePreprocessorReturnType PreprocessorData; - typedef SpaseMultiObjectiveHelperReturnType ReturnType; + typedef SparseMultiObjectivePreprocessorReturnType PreprocessorData; + typedef SparseMultiObjectiveHelperReturnType ReturnType; + typedef SparseMultiObjectiveHelperRefinementStep RefinementStep; typedef std::vector Point; typedef std::vector WeightVector; - static ReturnType check(PreprocessorData const& data); private: @@ -28,11 +30,6 @@ namespace storm { static void achievabilityQuery(PreprocessorData const& data, ReturnType& result); static void numericalQuery(PreprocessorData const& data, ReturnType& result); static void paretoQuery(PreprocessorData const& data, ReturnType& result); - - /* - * Refines the current result w.r.t. the given direction vector - */ - static void refineResult(WeightVector const& direction, SparseWeightedObjectivesModelCheckerHelper const& weightedObjectivesChecker, ReturnType& result); /* * Returns a weight vector w that separates the under approximation from the given point p, i.e., @@ -42,22 +39,47 @@ namespace storm { * @param underapproximation the current under approximation * @param objectivesToBeCheckedIndividually stores for each objective whether it still makes sense to check for this objective individually (i.e., with weight vector given by w_{objIndex} = 1 ) */ - static WeightVector findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) const; + static WeightVector findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked); + + /* + * Refines the current result w.r.t. the given direction vector + */ + static void performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker& weightVectorChecker, ReturnType& result); /* - * Updates the over- and under approximation, respectively + * Updates the overapproximation after a refinement step has been performed * - * @param iterations the iterations performed so far. iterations.back() should be the newest iteration, whose information is not yet included in the approximation. - * @param over/underApproximation the current over/underApproximation that will be updated + * @param refinementSteps the steps performed so far. The last entry should be the newest step, whose information is not yet included in the approximation. + * @param overApproximation the current overApproximation that will be updated */ - static void updateOverApproximation(std::vector const& iterations, std::shared_ptr>& overApproximation); - static void updateUnderApproximation(std::vector const& iterations, std::shared_ptr>& underApproximation); + static void updateOverApproximation(std::vector const& refinementSteps, std::shared_ptr>& overApproximation); + + /* + * Updates the underapproximation after a refinement step has been performed + * + * @param refinementSteps the steps performed so far. The last entry should be the newest step, whose information is not yet included in the approximation. + * @param underApproximation the current underApproximation that will be updated + */ + static void updateUnderApproximation(std::vector const& refinementSteps, std::shared_ptr>& underApproximation); /* * Returns true iff there is a point in the given polytope that satisfies the given thresholds. * It is assumed that the given polytope contains the downward closure of its vertices. */ - static bool checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) const; + static bool checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds); + + /* + * Returns whether the desired precision (as given in the settings) is reached by the current result. + * If the given result does not specify a precisionOfResult, false is returned. + * Also sets the result.targetPrecisionReached flag accordingly. + */ + static bool targetPrecisionReached(ReturnType& result); + + /* + * Returns whether a maximum number of refinement steps is given in the settings and this threshold has been reached. + * Also sets the result.maxStepsPerformed flag accordingly. + */ + static bool maxStepsPerformed(ReturnType& result); }; } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h new file mode 100644 index 000000000..3c42c0060 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h @@ -0,0 +1,58 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_ + +#include +#include + +#include "src/storage/TotalScheduler.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + class SparseMultiObjectiveHelperRefinementStep { + + public: + SparseMultiObjectiveHelperRefinementStep(std::vector const& weightVector, std::vector const& point, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) { + //Intentionally left empty + } + + SparseMultiObjectiveHelperRefinementStep(std::vector&& weightVector, std::vector&& point, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) { + //Intentionally left empty + } + + SparseMultiObjectiveHelperRefinementStep(std::vector const& weightVector, std::vector const& point) : weightVector(weightVector), point(point) { + //Intentionally left empty + } + + SparseMultiObjectiveHelperRefinementStep(std::vector&& weightVector, std::vector&& point) : weightVector(weightVector), point(point) { + //Intentionally left empty + } + + std::vector const& getWeightVector() const { + return weightVector; + } + + std::vector const& getPoint() const { + return point; + } + + bool hasScheduler() const { + return static_cast(scheduler); + } + + storm::storage::TotalScheduler const& getScheduler() const { + return scheduler.get(); + } + + private: + std::vector const weightVector; + std::vector const point; + boost::optional const scheduler; + }; + } + } +} + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h index 2c6e18d40..3a2bd80f2 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h @@ -3,51 +3,129 @@ #include #include -#include #include +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h" #include "src/storage/geometry/Polytope.h" -#include "src/storage/TotalScheduler.h" +#include "src/utility/macros.h" + +#include "src/exceptions/InvalidStateException.h" namespace storm { namespace modelchecker { namespace helper { - + template - struct SparseMultiObjectiveHelperReturnType { - - struct Iteration { - Iteration (std::vector const& weightVector, std::vector const& point, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) { - //Intentionally left empty - } - - Iteration (std::vector&& weightVector, std::vector&& point, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) { - //Intentionally left empty - } - - std::vector weightVector; - std::vector point; - storm::storage::TotalScheduler scheduler; + class SparseMultiObjectiveHelperReturnType { + + public: + std::vector>& refinementSteps() { + return steps; + } + std::vector> const& refinementSteps() const { + return steps; } - //Stores the results for the individual iterations - std::vector iterations; + std::shared_ptr>& overApproximation() { + return overApprox; + } + std::shared_ptr> const& overApproximation() const { + return overApprox; + } - //Stores an over/ under approximation of the set of achievable values - std::shared_ptr> overApproximation; - std::shared_ptr> underApproximation; + std::shared_ptr>& underApproximation() { + return underApprox; + } + std::shared_ptr> const& underApproximation() const { + return underApprox; + } - // Stores the result of an achievability query (if applicable) - // For a numerical query, stores whether there is one feasible solution - boost::optional thresholdsAreAchievable; + void setThresholdsAreAchievable(bool value) { + thresholdsAreAchievable = value ? Tribool::TT : Tribool::FF; + } + bool isThresholdsAreAchievableSet() const { + return thresholdsAreAchievable != Tribool::INDETERMINATE; + } + bool getThresholdsAreAchievable() const { + STORM_LOG_THROW(isThresholdsAreAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether thresholds are acheivable: value not set."); + return thresholdsAreAchievable == Tribool::TT; + } + + void setNumericalResult(RationalNumberType value) { + numericalResult = value; + } + bool isNumericalResultSet() const { + return static_cast(numericalResult); + } + template + TargetValueType getNumericalResult() const { + return storm::utility::convertNumber(numericalResult.get()); + } + + void setOptimumIsAchievable(bool value) { + optimumIsAchievable = value ? Tribool::TT : Tribool::FF; + } + bool isOptimumIsAchievableSet() const { + return optimumIsAchievable != Tribool::INDETERMINATE; + } + bool getOptimumIsAchievableAchievable() const { + STORM_LOG_THROW(isOptimumIsAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether the computed optimum is acheivable: value not set."); + return optimumIsAchievable == Tribool::TT; + } + + void setPrecisionOfResult(RationalNumberType value) { + precisionOfResult = value; + } + bool isPrecisionOfResultSet() const { + return static_cast(precisionOfResult); + } + template + TargetValueType getPrecisionOfResult() const { + return storm::utility::convertNumber(precisionOfResult.get()); + } + + void setTargetPrecisionReached(bool value) { + targetPrecisionReached = value; + } + bool getTargetPrecisionReached() const { + return targetPrecisionReached; + } - //Stores the result of a numerical query (if applicable) + void setMaxStepsPerformed(bool value) { + maxStepsPerformed = value; + } + bool getMaxStepsPerformed() const { + return maxStepsPerformed; + } + + private: + + enum class Tribool { FF, TT, INDETERMINATE }; + + //Stores the results for the individual iterations + std::vector> steps; + //Stores an overapproximation of the set of achievable values + std::shared_ptr> overApprox; + //Stores an underapproximation of the set of achievable values + std::shared_ptr> underApprox; + + // Stores the result of an achievability query (if applicable). + // For a numerical query, stores whether there is one feasible solution. + Tribool thresholdsAreAchievable = Tribool::INDETERMINATE; + + //Stores the result of a numerical query (if applicable). boost::optional numericalResult; - boost::optional optimumIsAchievable; //True if there is an actual scheduler that induces the computed supremum (i.e., supremum == maximum) + //For numerical queries, this is true iff there is an actual scheduler that induces the computed supremum (i.e., supremum == maximum) + Tribool optimumIsAchievable = Tribool::INDETERMINATE; //Stores the achieved precision for numerical and pareto queries boost::optional precisionOfResult; + //Stores whether the precision of the result is sufficient (only applicable to numerical and pareto queries) + bool targetPrecisionReached; + + //Stores whether the computation was aborted due to performing too many refinement steps + bool maxStepsPerformed; }; } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h index e9e198778..4a5dcc367 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h @@ -15,7 +15,7 @@ namespace storm { namespace helper { template - struct SparseMultiObjectiveModelCheckerInformation { + struct SparseMultiObjectivePreprocessorReturnType { typedef typename SparseModelType::ValueType ValueType; typedef typename SparseModelType::RewardModelType RewardModelType; @@ -53,7 +53,7 @@ namespace storm { } }; - SparseMultiObjectiveModelCheckerInformation(SparseModelType const& model) : preprocessedModel(model), originalModel(model) { + SparseMultiObjectivePreprocessorReturnType(SparseModelType const& model) : preprocessedModel(model), originalModel(model) , produceSchedulers(false) { //Intentionally left empty } @@ -82,7 +82,7 @@ namespace storm { SparseModelType const& originalModel; std::vector newToOldStateIndexMapping; std::vector objectives; - + bool produceSchedulers; }; } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index 14a20f23c..bbd3f0b0c 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp @@ -1,9 +1,9 @@ -#include "src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h" +#include "src/adapters/CarlAdapter.h" #include "src/models/sparse/Mdp.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" -#include "src/solver/LinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h" #include "src/transformer/NeutralECRemover.h" #include "src/utility/graph.h" @@ -18,52 +18,53 @@ namespace storm { template - SparseWeightedObjectivesModelCheckerHelper::SparseWeightedObjectivesModelCheckerHelper(Information const& info) : info(info), checkHasBeenCalled(false) , objectiveResults(info.objectives.size()){ + SparseMultiObjectiveWeightVectorChecker::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), checkHasBeenCalled(false) , objectiveResults(data.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); + void SparseMultiObjectiveWeightVectorChecker::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); + //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]); + //STORM_LOG_DEBUG("Unbounded individual phase resulted in..."); + for(uint_fast64_t objIndex = 0; objIndex < data.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]); + // STORM_LOG_DEBUG("Bounded phase resulted in..."); + for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { + // STORM_LOG_DEBUG("\t objective " << objIndex << ":" << objectiveResults[objIndex]); } checkHasBeenCalled=true; } template - std::vector::ValueType> SparseWeightedObjectivesModelCheckerHelper::getInitialStateResultOfObjectives() const { + template + std::vector SparseMultiObjectiveWeightVectorChecker::getInitialStateResultOfObjectives() const { STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); - STORM_LOG_ASSERT(info.preprocessedModel.getInitialStates().getNumberOfSetBits()==1, "The considered model has multiple initial states"); - std::vector res; + STORM_LOG_ASSERT(data.preprocessedModel.getInitialStates().getNumberOfSetBits()==1, "The considered model has multiple initial states"); + std::vector res; res.reserve(objectiveResults.size()); for(auto const& objResult : objectiveResults) { - res.push_back(objResult[*info.preprocessedModel.getInitialStates().begin()]); + res.push_back(storm::utility::convertNumber(objResult[*data.preprocessedModel.getInitialStates().begin()])); } return res; } template - storm::storage::TotalScheduler const& SparseWeightedObjectivesModelCheckerHelper::getScheduler() const { + storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker::getScheduler() const { STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); return scheduler; } template - void SparseWeightedObjectivesModelCheckerHelper::unboundedWeightedPhase(std::vector const& weightVector) { - std::vector weightedRewardVector(info.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); + void SparseMultiObjectiveWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightVector) { + std::vector weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); for(uint_fast64_t objIndex = 0; objIndex < weightVector.size(); ++objIndex) { - if(!info.objectives[objIndex].stepBound){ - storm::utility::vector::addScaledVector(weightedRewardVector, info.preprocessedModel.getRewardModel(info.objectives[objIndex].rewardModelName).getStateActionRewardVector(), weightVector[objIndex]); + if(!data.objectives[objIndex].stepBound){ + storm::utility::vector::addScaledVector(weightedRewardVector, data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector(), weightVector[objIndex]); } } @@ -72,7 +73,7 @@ namespace storm { //std::cout << "weighted reward vector is " << storm::utility::vector::toString(weightedRewardVector) << std::endl; // Remove end components in which no reward is earned - auto removerResult = storm::transformer::NeutralECRemover::transform(info.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(info.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true)); + auto removerResult = storm::transformer::NeutralECRemover::transform(data.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true)); std::vector subResult(removerResult.matrix.getRowGroupCount()); @@ -81,10 +82,10 @@ namespace storm { solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->solveEquationSystem(subResult, removerResult.vector); - this->weightedResult = std::vector(info.preprocessedModel.getNumberOfStates()); - this->scheduler = storm::storage::TotalScheduler(info.preprocessedModel.getNumberOfStates()); - storm::storage::BitVector statesWithUndefinedScheduler(info.preprocessedModel.getNumberOfStates(), false); - for(uint_fast64_t state = 0; state < info.preprocessedModel.getNumberOfStates(); ++state) { + this->weightedResult = std::vector(data.preprocessedModel.getNumberOfStates()); + this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates()); + storm::storage::BitVector statesWithUndefinedScheduler(data.preprocessedModel.getNumberOfStates(), false); + for(uint_fast64_t state = 0; state < data.preprocessedModel.getNumberOfStates(); ++state) { uint_fast64_t stateInReducedModel = removerResult.oldToNewStateMapping[state]; // Check if the state exists in the reduced model if(stateInReducedModel < removerResult.matrix.getRowGroupCount()) { @@ -92,9 +93,9 @@ namespace storm { // Check if the chosen row originaly belonged to the current state uint_fast64_t chosenRowInReducedModel = removerResult.matrix.getRowGroupIndices()[stateInReducedModel] + solver->getScheduler().getChoice(stateInReducedModel); uint_fast64_t chosenRowInOriginalModel = removerResult.newToOldRowMapping[chosenRowInReducedModel]; - if(chosenRowInOriginalModel >= info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state] && - chosenRowInOriginalModel < info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) { - this->scheduler.setChoice(state, chosenRowInOriginalModel - info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]); + if(chosenRowInOriginalModel >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state] && + chosenRowInOriginalModel < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) { + this->scheduler.setChoice(state, chosenRowInOriginalModel - data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]); } else { statesWithUndefinedScheduler.set(state); } @@ -108,17 +109,17 @@ namespace storm { for(auto state : statesWithUndefinedScheduler) { // Try to find a choice that stays inside the EC (i.e., for which all successors are represented by the same state in the reduced model) // And at least one successor has a defined scheduler. - // This way, a scheduler is chosen that leads (with probability one) to the state from which the EC can be left + // This way, a scheduler is chosen that leads (with probability one) to the state of the EC for which the scheduler is defined uint_fast64_t stateInReducedModel = removerResult.oldToNewStateMapping[state]; - for(uint_fast64_t row = info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { + for(uint_fast64_t row = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { bool rowStaysInEC = true; bool rowLeadsToDefinedScheduler = false; - for(auto const& entry : info.preprocessedModel.getTransitionMatrix().getRow(row)) { + for(auto const& entry : data.preprocessedModel.getTransitionMatrix().getRow(row)) { rowStaysInEC &= ( stateInReducedModel == removerResult.oldToNewStateMapping[entry.getColumn()]); rowLeadsToDefinedScheduler |= !statesWithUndefinedScheduler.get(entry.getColumn()); } if(rowStaysInEC && rowLeadsToDefinedScheduler) { - this->scheduler.setChoice(state, row - info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]); + this->scheduler.setChoice(state, row - data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]); statesWithUndefinedScheduler.set(state, false); } } @@ -127,9 +128,9 @@ namespace storm { } template - void SparseWeightedObjectivesModelCheckerHelper::unboundedIndividualPhase(std::vector const& weightVector) { + void SparseMultiObjectiveWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { - storm::storage::SparseMatrix deterministicMatrix = info.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); + storm::storage::SparseMatrix deterministicMatrix = data.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true); storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); storm::utility::solver::LinearEquationSolverFactory linearEquationSolverFactory; @@ -137,11 +138,11 @@ namespace storm { //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){ + if(!data.objectives[objIndex].stepBound){ - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), info.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), info.preprocessedModel.getRewardModel(info.objectives[objIndex].rewardModelName).getStateActionRewardVector()); + storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getRewardModel(data.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 << "stateActionRewardVector for objective " << objIndex << " is " << storm::utility::vector::toString(data.preprocessedModel.getRewardModel(data.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::filterZero(deterministicStateRewards); @@ -161,14 +162,17 @@ namespace storm { } template - void SparseWeightedObjectivesModelCheckerHelper::boundedPhase(std::vector const& weightVector) { + void SparseMultiObjectiveWeightVectorChecker::boundedPhase(std::vector const& weightVector) { STORM_LOG_WARN("bounded properties not yet implemented"); } - template class SparseWeightedObjectivesModelCheckerHelper>; - + template class SparseMultiObjectiveWeightVectorChecker>; + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; +#ifdef STORM_HAVE_CARL + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; +#endif } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h index f6b2600bd..2488a8e42 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h @@ -21,9 +21,9 @@ namespace storm { public: typedef typename SparseModelType::ValueType ValueType; typedef typename SparseModelType::RewardModelType RewardModelType; - typedef SparseMultiObjectiveModelCheckerInformation Information; + typedef SparseMultiObjectivePreprocessorReturnType PreprocessorData; - SparseWeightedObjectivesModelCheckerHelper(Information const& info); + SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data); /*! * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives @@ -37,7 +37,8 @@ namespace storm { * Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown. */ // The results of the individual objectives at the initial state of the given model - std::vector getInitialStateResultOfObjectives() const; + template + std::vector getInitialStateResultOfObjectives() const; // A scheduler that induces the optimal values storm::storage::TotalScheduler const& getScheduler() const; @@ -69,7 +70,7 @@ namespace storm { void boundedPhase(std::vector const& weightVector); // stores the considered information of the multi-objective model checking problem - Information const& info; + PreprocessorData const& data; // becomes true after the first call of check(..) bool checkHasBeenCalled; diff --git a/src/settings/modules/MultiObjectiveSettings.cpp b/src/settings/modules/MultiObjectiveSettings.cpp index d37eaec3b..02e04e762 100644 --- a/src/settings/modules/MultiObjectiveSettings.cpp +++ b/src/settings/modules/MultiObjectiveSettings.cpp @@ -13,15 +13,15 @@ namespace storm { const std::string MultiObjectiveSettings::moduleName = "multiobjective"; const std::string MultiObjectiveSettings::exportResultFileOptionName = "resultfile"; const std::string MultiObjectiveSettings::precisionOptionName = "precision"; - const std::string MultiObjectiveSettings::maxIterationsOptionName = "maxiterations"; + const std::string MultiObjectiveSettings::maxStepsOptionName = "maxsteps"; MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportResultFileOptionName, true, "Saves the result as LaTeX document.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "A path to a file where the result should be saved.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.") .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision. Default is 1e-04.").setDefaultValueDouble(1e-04).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maxIterationsOptionName, true, "Aborts the computation after the given number of iterations (= computed pareto optimal points).") - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of iterations to be performed.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).") + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build()); } bool MultiObjectiveSettings::exportResultToFile() const { @@ -36,12 +36,12 @@ namespace storm { return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } - bool MultiObjectiveSettings::isMaxIterationsSet() const { - return this->getOption(maxIterationsOptionName).getHasOptionBeenSet(); + bool MultiObjectiveSettings::isMaxStepsSet() const { + return this->getOption(maxStepsOptionName).getHasOptionBeenSet(); } - uint_fast64_t MultiObjectiveSettings::getMaxIterations() const { - return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsUnsignedInteger(); + uint_fast64_t MultiObjectiveSettings::getMaxSteps() const { + return this->getOption(maxStepsOptionName).getArgumentByName("value").getValueAsUnsignedInteger(); } } // namespace modules diff --git a/src/settings/modules/MultiObjectiveSettings.h b/src/settings/modules/MultiObjectiveSettings.h index 207d9fb8a..42c7d92bd 100644 --- a/src/settings/modules/MultiObjectiveSettings.h +++ b/src/settings/modules/MultiObjectiveSettings.h @@ -37,19 +37,19 @@ namespace storm { double getPrecision() const; /*! - * Retrieves whether or not a threshold for the number of performed iterations is given. + * Retrieves whether or not a threshold for the number of performed refinement steps is given. * - * @return True if a threshold for the number of performed iterations is given. + * @return True if a threshold for the number of performed refinement steps is given. */ - bool isMaxIterationsSet() const; + bool isMaxStepsSet() const; /*! - * Retrieves The maximum number of iterations that should be performed (if given). + * Retrieves The maximum number of refinement steps that should be performed (if given). * - * @return the maximum number of iterations that should be performed (if given). + * @return the maximum number of refinement steps that should be performed (if given). */ - uint_fast64_t getMaxIterations() const; + uint_fast64_t getMaxSteps() const; const static std::string moduleName; @@ -57,7 +57,7 @@ namespace storm { private: const static std::string exportResultFileOptionName; const static std::string precisionOptionName; - const static std::string maxIterationsOptionName; + const static std::string maxStepsOptionName; }; } // namespace modules diff --git a/src/transformer/NeutralECRemover.h b/src/transformer/NeutralECRemover.h index 00a94385a..52de167e8 100644 --- a/src/transformer/NeutralECRemover.h +++ b/src/transformer/NeutralECRemover.h @@ -89,7 +89,7 @@ namespace storm { result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, emptyRows); result.vector = buildTransformedVector(originalVector, result.newToOldRowMapping); - STORM_LOG_DEBUG("NeutralECRemover is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups. Resulting Matrix: " << std::endl << result.matrix << std::endl << " resulting vector: " << result.vector ); + STORM_LOG_DEBUG("NeutralECRemover is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups."); return result; }