sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

further polishing code 

Former-commit-id: 100ca37977
main
TimQu 9 years ago
parent
c86c6953b5
commit
b00d3f154c
11 changed files with 368 additions and 205 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
  2. 198
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
  3. 52
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
  4. 58
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h
  5. 132
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h
  6. 6
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h
  7. 86
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
  8. 9
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h
  9. 14
      src/settings/modules/MultiObjectiveSettings.cpp
  10. 14
      src/settings/modules/MultiObjectiveSettings.h
  11. 2
      src/transformer/NeutralECRemover.h

2
src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
View File

@ -34,7 +34,7 @@ namespace storm {
template<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) {
auto preprocessedData = helper::SparseMdpMultiObjectivePreprocessingHelper<SparseMdpModelType>::preprocess(checkTask.getFormula(), this->getModel());
auto preprocessedData = helper::SparseMultiObjectivePreprocessor<SparseMdpModelType>::preprocess(checkTask.getFormula(), this->getModel());
std::cout << std::endl;
std::cout << "Preprocessing done." << std::endl;
preprocessedData.printToStream(std::cout);

198
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
View File

@ -18,8 +18,8 @@ namespace storm {
template <class SparseModelType, typename RationalNumberType>
typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::ReturnType SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::check(PreprocessorData const& data) {
ReturnType result;
result.overApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
result.underApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
result.overApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
result.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::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<SparseModelType> 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<storm::settings::modules::MultiObjectiveSettings>().isMaxIterationsSet() && result.iterations.size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxIterations());
} while(!converged);
} while(!result.isThresholdsAreAchievableSet() && !maxStepsPerformed(result));
}
template <class SparseModelType, typename RationalNumberType>
@ -96,68 +91,61 @@ namespace storm {
storm::storage::BitVector individualObjectivesToBeChecked(data.objectives.size(), true);
individualObjectivesToBeChecked.set(optimizingObjIndex, false);
SparseMultiObjectiveWeightVectorChecker<SparseModelType> 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<Point, bool> optimizationRes = underApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
while(true) {
std::pair<Point, bool> 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<double>(thresholds[optimizingObjIndex]) << ".");
result.setNumericalResult(thresholds[optimizingObjIndex]);
STORM_LOG_DEBUG("Best solution found so far is " << result.template getNumericalResult<double>() << ".");
//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<double>(*result.precisionOfResult));
if(storm::utility::convertNumber<double>(*result.precisionOfResult) < storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().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<double>());
}
converged |= (storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxIterationsSet() && result.iterations.size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().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 <class SparseModelType, typename RationalNumberType>
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::paretoQuery(PreprocessorData const& data, ReturnType& result) {
SparseMultiObjectiveWeightVectorChecker<SparseModelType> 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<data.objectives.size() && !maxStepsPerformed(result); ++objIndex) {
WeightVector direction(data.objectives.size(), storm::utility::zero<RationalNumberType>());
direction[objIndex] = storm::utility::one<RationalNumberType>();
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<storm::storage::geometry::Halfspace<RationalNumberType>> underApproxHalfspaces = result.underApproximation->getHalfspaces();
std::vector<Point> overApproxVertices = result.overApproximation->getVertices();
std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> underApproxHalfspaces = result.underApproximation()->getHalfspaces();
std::vector<Point> overApproxVertices = result.overApproximation()->getVertices();
uint_fast64_t farestHalfspaceIndex = underApproxHalfspaces.size();
RationalNumberType farestDistance = storm::utility::zero<RationalNumberType>();
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<double>(farestDistance));
if(storm::utility::convertNumber<double>(farestDistance) < storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()) {
result.precisionOfResult = farestDistance;
converged = true;
}
converged |= (storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxIterationsSet() && result.iterations.size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().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<double>());
if(targetPrecisionReached(result) || maxStepsPerformed(result)) {
break;
}
} while(!converged);
}
template <class SparseModelType, typename RationalNumberType>
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::refineResult(WeightVector const& direction, SparseWeightedObjectivesModelCheckerHelper<SparseModelType> const& weightedObjectivesChecker, ReturnType& result) {
weightedObjectivesChecker.check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction));
STORM_LOG_DEBUG("Result with weighted objectives is " << weightedObjectivesChecker.getInitialStateResultOfObjectives());
result.iterations.emplace_back(direction, storm::utility::vector::convertNumericVector<RationalNumberType>(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 <class SparseModelType, typename RationalNumberType>
typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::WeightVector SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) const {
typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::WeightVector SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) {
STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::convertNumericVector<double>(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<storm::storage::geometry::Halfspace<RationalNumberType>> 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<RationalNumberType>(halfspaces[farestHalfspaceIndex].normalVector());
bool foundSeparatingSingleObjectiveVector = nonZeroVectorEntries.getNumberOfSetBits()==1 && individualObjectivesToBeChecked.get(nonZeroVectorEntries.getNextSetIndex(0)) && farestDistance>storm::utility::zero<RationalNumberType>();
for(uint_fast64_t halfspaceIndex = 1; halfspaceIndex < halfspaces.size(); ++halfspaceIndex) {
uint_fast64_t farestHalfspaceIndex = halfspaces.size();
RationalNumberType farestDistance = -storm::utility::one<RationalNumberType>();
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<RationalNumberType>(halfspaces[farestHalfspaceIndex].normalVector());
bool isSeparatingSingleObjectiveVector = nonZeroVectorEntries.getNumberOfSetBits() == 1 && individualObjectivesToBeChecked.get(nonZeroVectorEntries.getNextSetIndex(0)) && distance>storm::utility::zero<RationalNumberType>();
// 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<RationalNumberType>()) {
storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero<RationalNumberType>(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<RationalNumberType>(halfspaces[farestHalfspaceIndex].normalVector());
storm::storage::BitVector nonZeroVectorEntries = ~storm::utility::vector::filterZero<RationalNumberType>(halfspaces[farestHalfspaceIndex].normalVector());
individualObjectivesToBeChecked.set(nonZeroVectorEntries.getNextSetIndex(0), false);
}
STORM_LOG_THROW(farestDistance>=storm::utility::zero<RationalNumberType>(), storm::exceptions::UnexpectedException, "There is no seperating vector.");
STORM_LOG_THROW(farestHalfspaceIndex<halfspaces.size(), storm::exceptions::UnexpectedException, "There is no seperating vector.");
STORM_LOG_DEBUG("Found separating weight vector: " << storm::utility::vector::convertNumericVector<double>(halfspaces[farestHalfspaceIndex].normalVector()) << ".");
return halfspaces[farestHalfspaceIndex].normalVector();
}
template <class SparseModelType, typename RationalNumberType>
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::updateOverApproximation(std::vector<typename ReturnType::Iteration> const& iterations, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation) {
storm::storage::geometry::Halfspace<RationalNumberType> h(iterations.back().weightVector, storm::utility::vector::dotProduct(iterations.back().weightVector, iterations.back().point));
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ReturnType& result) {
weightVectorChecker.check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction));
STORM_LOG_DEBUG("weighted objectives checker result is " << weightVectorChecker.getInitialStateResultOfObjectives());
if(saveScheduler) {
result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives<RationalNumberType>(), weightVectorChecker.getScheduler());
} else {
result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives<RationalNumberType>());
}
updateOverApproximation(result.refinementSteps(), result.overApproximation());
updateUnderApproximation(result.refinementSteps(), result.underApproximation());
}
template <class SparseModelType, typename RationalNumberType>
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::updateOverApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation) {
storm::storage::geometry::Halfspace<RationalNumberType> 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<double>(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<double>(h.euclideanDistance(refinementSteps.back().getPoint())) << ".");
}
overApproximation = overApproximation->intersection(h);
STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true));
}
template <class SparseModelType, typename RationalNumberType>
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::updateUnderApproximation(std::vector<typename ReturnType::Iteration> const& iterations, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& underApproximation) {
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::updateUnderApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& underApproximation) {
std::vector<Point> 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 <class SparseModelType, typename RationalNumberType>
bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::checkIfThresholdsAreSatisfied(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) const {
bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::checkIfThresholdsAreSatisfied(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) {
std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> halfspaces = polytope->getHalfspaces();
for(auto const& h : halfspaces) {
RationalNumberType distance = h.distance(thresholds);
@ -319,6 +305,20 @@ namespace storm {
return true;
}
template <class SparseModelType, typename RationalNumberType>
bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::targetPrecisionReached(ReturnType& result) {
result.setTargetPrecisionReached(result.isPrecisionOfResultSet() &&
result.getPrecisionOfResult() < storm::utility::convertNumber<RationalNumberType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()));
return result.getTargetPrecisionReached();
}
template <class SparseModelType, typename RationalNumberType>
bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::maxStepsPerformed(ReturnType& result) {
result.setMaxStepsPerformed(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxStepsSet() &&
result.refinementSteps().size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxSteps());
return result.getMaxStepsPerformed();
}
#ifdef STORM_HAVE_CARL
template class SparseMultiObjectiveHelper<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
#endif

52
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
View File

@ -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 SparseModelType, typename RationalNumberType>
class SparseMultiObjectiveHelper {
public:
typedef SpaseMultiObjectivePreprocessorReturnType<SparseModelType> PreprocessorData;
typedef SpaseMultiObjectiveHelperReturnType<RationalNumberType> ReturnType;
typedef SparseMultiObjectivePreprocessorReturnType<SparseModelType> PreprocessorData;
typedef SparseMultiObjectiveHelperReturnType<RationalNumberType> ReturnType;
typedef SparseMultiObjectiveHelperRefinementStep<RationalNumberType> RefinementStep;
typedef std::vector<RationalNumberType> Point;
typedef std::vector<RationalNumberType> 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<SparseModelType> 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<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) const;
static WeightVector findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> 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<SparseModelType>& 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<typename ReturnType::Iteration> const& iterations, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation);
static void updateUnderApproximation(std::vector<typename ReturnType::Iteration> const& iterations, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& underApproximation);
static void updateOverApproximation(std::vector<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& 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<RefinementStep> const& refinementSteps, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& 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<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, Point const& thresholds, storm::storage::BitVector const& strictThresholds) const;
static bool checkIfThresholdsAreSatisfied(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> 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);
};
}

58
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h
View File

@ -0,0 +1,58 @@
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_
#include <vector>
#include <boost/optional.hpp>
#include "src/storage/TotalScheduler.h"
namespace storm {
namespace modelchecker {
namespace helper {
template <typename RationalNumberType>
class SparseMultiObjectiveHelperRefinementStep {
public:
SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
//Intentionally left empty
}
SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
//Intentionally left empty
}
SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point) : weightVector(weightVector), point(point) {
//Intentionally left empty
}
SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point) : weightVector(weightVector), point(point) {
//Intentionally left empty
}
std::vector<RationalNumberType> const& getWeightVector() const {
return weightVector;
}
std::vector<RationalNumberType> const& getPoint() const {
return point;
}
bool hasScheduler() const {
return static_cast<bool>(scheduler);
}
storm::storage::TotalScheduler const& getScheduler() const {
return scheduler.get();
}
private:
std::vector<RationalNumberType> const weightVector;
std::vector<RationalNumberType> const point;
boost::optional<storm::storage::TotalScheduler> const scheduler;
};
}
}
}
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_ */

132
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h
View File

@ -3,51 +3,129 @@
#include <vector>
#include <memory>
#include <iomanip>
#include <boost/optional.hpp>
#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 <typename RationalNumberType>
struct SparseMultiObjectiveHelperReturnType {
struct Iteration {
Iteration (std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
//Intentionally left empty
}
Iteration (std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
//Intentionally left empty
}
std::vector<RationalNumberType> weightVector;
std::vector<RationalNumberType> point;
storm::storage::TotalScheduler scheduler;
class SparseMultiObjectiveHelperReturnType {
public:
std::vector<SparseMultiObjectiveHelperRefinementStep<RationalNumberType>>& refinementSteps() {
return steps;
}
std::vector<SparseMultiObjectiveHelperRefinementStep<RationalNumberType>> const& refinementSteps() const {
return steps;
}
//Stores the results for the individual iterations
std::vector<Iteration> iterations;
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& overApproximation() {
return overApprox;
}
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& overApproximation() const {
return overApprox;
}
//Stores an over/ under approximation of the set of achievable values
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> overApproximation;
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> underApproximation;
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>>& underApproximation() {
return underApprox;
}
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> 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<bool> 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<bool>(numericalResult);
}
template<typename TargetValueType = RationalNumberType>
TargetValueType getNumericalResult() const {
return storm::utility::convertNumber<TargetValueType>(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<bool>(precisionOfResult);
}
template<typename TargetValueType = RationalNumberType>
TargetValueType getPrecisionOfResult() const {
return storm::utility::convertNumber<TargetValueType>(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<SparseMultiObjectiveHelperRefinementStep<RationalNumberType>> steps;
//Stores an overapproximation of the set of achievable values
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> overApprox;
//Stores an underapproximation of the set of achievable values
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> 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<RationalNumberType> numericalResult;
boost::optional<bool> 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<RationalNumberType> 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;
};
}
}

6
src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h
View File

@ -15,7 +15,7 @@ namespace storm {
namespace helper {
template <class SparseModelType>
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<uint_fast64_t> newToOldStateIndexMapping;
std::vector<ObjectiveInformation> objectives;
bool produceSchedulers;
};
}
}

86
src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
View File

@ -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 <class SparseModelType>
SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::SparseWeightedObjectivesModelCheckerHelper(Information const& info) : info(info), checkHasBeenCalled(false) , objectiveResults(info.objectives.size()){
SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), checkHasBeenCalled(false) , objectiveResults(data.objectives.size()){
//Intentionally left empty
}
template <class SparseModelType>
void SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::check(std::vector<ValueType> const& weightVector) {
STORM_LOG_DEBUG("Checking weighted objectives with weight vector " << std::endl << "\t" << weightVector);
void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> 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 <class SparseModelType>
std::vector<typename SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::ValueType> SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::getInitialStateResultOfObjectives() const {
template<typename TargetValueType>
std::vector<TargetValueType> SparseMultiObjectiveWeightVectorChecker<SparseModelType>::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<ValueType> res;
STORM_LOG_ASSERT(data.preprocessedModel.getInitialStates().getNumberOfSetBits()==1, "The considered model has multiple initial states");
std::vector<TargetValueType> res;
res.reserve(objectiveResults.size());
for(auto const& objResult : objectiveResults) {
res.push_back(objResult[*info.preprocessedModel.getInitialStates().begin()]);
res.push_back(storm::utility::convertNumber<TargetValueType>(objResult[*data.preprocessedModel.getInitialStates().begin()]));
}
return res;
}
template <class SparseModelType>
storm::storage::TotalScheduler const& SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::getScheduler() const {
storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getScheduler() const {
STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
return scheduler;
}
template <class SparseModelType>
void SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightVector) {
std::vector<ValueType> weightedRewardVector(info.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightVector) {
std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
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<ValueType>::transform(info.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(info.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true));
auto removerResult = storm::transformer::NeutralECRemover<ValueType>::transform(data.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true));
std::vector<ValueType> 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<ValueType>(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<ValueType>(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 <class SparseModelType>
void SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::unboundedIndividualPhase(std::vector<ValueType> const& weightVector) {
void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedIndividualPhase(std::vector<ValueType> const& weightVector) {
storm::storage::SparseMatrix<ValueType> deterministicMatrix = info.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true);
storm::storage::SparseMatrix<ValueType> deterministicMatrix = data.preprocessedModel.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true);
storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount());
storm::utility::solver::LinearEquationSolverFactory<ValueType> 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 <class SparseModelType>
void SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::boundedPhase(std::vector<ValueType> const& weightVector) {
void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::boundedPhase(std::vector<ValueType> const& weightVector) {
STORM_LOG_WARN("bounded properties not yet implemented");
}
template class SparseWeightedObjectivesModelCheckerHelper<storm::models::sparse::Mdp<double>>;
template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>;
template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<double>() const;
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
#endif
}
}

9
src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h
View File

@ -21,9 +21,9 @@ namespace storm {
public:
typedef typename SparseModelType::ValueType ValueType;
typedef typename SparseModelType::RewardModelType RewardModelType;
typedef SparseMultiObjectiveModelCheckerInformation<SparseModelType> Information;
typedef SparseMultiObjectivePreprocessorReturnType<SparseModelType> 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<ValueType> getInitialStateResultOfObjectives() const;
template<typename TargetValueType = ValueType>
std::vector<TargetValueType> 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<ValueType> 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;

14
src/settings/modules/MultiObjectiveSettings.cpp
View File

@ -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

14
src/settings/modules/MultiObjectiveSettings.h
View File

@ -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

2
src/transformer/NeutralECRemover.h
View File

@ -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;
}

Write Preview
Loading…
Cancel
Save