Browse Source

Added abstract superclass for WeightVectorCheckers

tempestpy_adaptions
TimQu 7 years ago
parent
commit
9716289f6a
  1. 81
      src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp
  2. 105
      src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h
  3. 26
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
  4. 12
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
  5. 91
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  6. 38
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h

81
src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp

@ -0,0 +1,81 @@
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
template <typename ModelType>
PcaaWeightVectorChecker<ModelType>::PcaaWeightVectorChecker(ModelType const& model, std::vector<Objective<ValueType>> const& objectives) : model(model), objectives(objectives) {
// Intentionally left empty
}
template <typename ModelType>
void PcaaWeightVectorChecker<ModelType>::setWeightedPrecision(ValueType const& value) {
weightedPrecision = value;
}
template <typename ModelType>
typename PcaaWeightVectorChecker<ModelType>::ValueType const& PcaaWeightVectorChecker<ModelType>::getWeightedPrecision() const {
return weightedPrecision;
}
template <typename ModelType>
storm::storage::Scheduler<typename PcaaWeightVectorChecker<ModelType>::ValueType> PcaaWeightVectorChecker<ModelType>::computeScheduler() const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler generation is not supported in this setting.");
}
template <typename ModelType>
template<typename VT, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::Mdp<VT>>::value, int>::type>
std::unique_ptr<PcaaWeightVectorChecker<ModelType>> WeightVectorCheckerFactory<ModelType>::create(ModelType const& model,
std::vector<Objective<typename ModelType::ValueType>> const& objectives,
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates) {
return std::make_unique<SparseMdpPcaaWeightVectorChecker<ModelType>>(model, objectives, possibleECActions, possibleBottomStates);
}
template <typename ModelType>
template<typename VT, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::MarkovAutomaton<VT>>::value, int>::type>
std::unique_ptr<PcaaWeightVectorChecker<ModelType>> WeightVectorCheckerFactory<ModelType>::create(ModelType const& model,
std::vector<Objective<typename ModelType::ValueType>> const& objectives,
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates) {
return std::make_unique<SparseMaPcaaWeightVectorChecker<ModelType>>(model, objectives, possibleECActions, possibleBottomStates);
}
template <class ModelType>
bool WeightVectorCheckerFactory<ModelType>::onlyCumulativeOrTotalRewardObjectives(std::vector<Objective<typename ModelType::ValueType>> const& objectives) {
for (auto const& obj : objectives) {
if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula()))) {
return false;
}
}
return true;
}
template class PcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>;
template class PcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;
template class PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
template class WeightVectorCheckerFactory<storm::models::sparse::Mdp<double>>;
template class WeightVectorCheckerFactory<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<double>>;
template class WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>> WeightVectorCheckerFactory<storm::models::sparse::Mdp<double>>::create(storm::models::sparse::Mdp<double> const& model, std::vector<Objective<double>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates);
template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>> WeightVectorCheckerFactory<storm::models::sparse::Mdp<storm::RationalNumber>>::create(storm::models::sparse::Mdp<storm::RationalNumber> const& model, std::vector<Objective<storm::RationalNumber>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates);
template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>> WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<double>>::create(storm::models::sparse::MarkovAutomaton<double> const& model, std::vector<Objective<double>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates);
template std::unique_ptr<PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>> WeightVectorCheckerFactory<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>::create(storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, std::vector<Objective<storm::RationalNumber>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates);
}
}
}

105
src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h

@ -0,0 +1,105 @@
#pragma once
#include <vector>
#include "storm/storage/Scheduler.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h"
#include "storm/modelchecker/multiobjective/Objective.h"
namespace storm {
namespace modelchecker {
namespace multiobjective {
/*!
* Helper Class that takes a weight vector and ...
* - computes the optimal value w.r.t. the weighted sum of the individual objectives
* - extracts the scheduler that induces this optimum
* - computes for each objective the value induced by this scheduler
*/
template <typename ModelType>
class PcaaWeightVectorChecker {
public:
typedef typename ModelType::ValueType ValueType;
/*
* Creates a weight vector checker.
*
* @param objectives The (preprocessed) objectives
*
*/
PcaaWeightVectorChecker(ModelType const& model, std::vector<Objective<ValueType>> const& objectives);
virtual ~PcaaWeightVectorChecker() = default;
virtual void check(std::vector<ValueType> const& weightVector) = 0;
/*!
* Retrieves the results of the individual objectives at the initial state of the given model.
* Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown.
* Also note that there is no guarantee that the under/over approximation is in fact correct
* as long as the underlying solution methods are unsound (e.g., standard value iteration).
*/
virtual std::vector<ValueType> getUnderApproximationOfInitialStateResults() const = 0;
virtual std::vector<ValueType> getOverApproximationOfInitialStateResults() const = 0;
/*!
* Sets the precision of this weight vector checker. After calling check() the following will hold:
* Let h_lower and h_upper be two hyperplanes such that
* * the normal vector is the provided weight-vector where the entry for minimizing objectives is negated
* * getUnderApproximationOfInitialStateResults() lies on h_lower and
* * getOverApproximationOfInitialStateResults() lies on h_upper.
* Then the distance between the two hyperplanes is at most weightedPrecision
*/
void setWeightedPrecision(ValueType const& value);
/*!
* Returns the precision of this weight vector checker.
*/
ValueType const& getWeightedPrecision() const;
/*!
* Retrieves a scheduler that induces the current values (if such a scheduler was generated).
* Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown.
*/
virtual storm::storage::Scheduler<ValueType> computeScheduler() const;
protected:
// The (preprocessed) model
ModelType const& model;
// The (preprocessed) objectives
std::vector<Objective<ValueType>> const& objectives;
// The precision of this weight vector checker.
ValueType weightedPrecision;
};
template<typename ModelType>
class WeightVectorCheckerFactory {
public:
template<typename VT = typename ModelType::ValueType, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::Mdp<VT>>::value, int>::type = 0>
static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(ModelType const& model,
std::vector<Objective<typename ModelType::ValueType>> const& objectives,
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates);
template<typename VT = typename ModelType::ValueType, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::MarkovAutomaton<VT>>::value, int>::type = 0>
static std::unique_ptr<PcaaWeightVectorChecker<ModelType>> create(ModelType const& model,
std::vector<Objective<typename ModelType::ValueType>> const& objectives,
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates);
private:
static bool onlyCumulativeOrTotalRewardObjectives(std::vector<Objective<typename ModelType::ValueType>> const& objectives);
};
}
}
}

26
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp

@ -5,8 +5,6 @@
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/MultiObjectiveSettings.h"
#include "storm/storage/geometry/Hyperrectangle.h"
@ -26,33 +24,13 @@ namespace storm {
originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula),
preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) {
initializeWeightVectorChecker(preprocessedModel, objectives, preprocessorResult.possibleECChoices, preprocessorResult.possibleBottomStates);
this->weightVectorChecker = WeightVectorCheckerFactory<SparseModelType>::create(preprocessedModel, objectives, preprocessorResult.possibleECChoices, preprocessorResult.possibleBottomStates);
this->diracWeightVectorsToBeChecked = storm::storage::BitVector(this->objectives.size(), true);
this->overApproximation = storm::storage::geometry::Polytope<GeometryValueType>::createUniversalPolytope();
this->underApproximation = storm::storage::geometry::Polytope<GeometryValueType>::createEmptyPolytope();
}
template<>
void SparsePcaaQuery<storm::models::sparse::Mdp<double>, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp<double> const& model, std::vector<Objective<double>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) {
this->weightVectorChecker = std::unique_ptr<SparsePcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>>(new SparseMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>(model, objectives, possibleECActions, possibleBottomStates));
}
template<>
void SparsePcaaQuery<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp<storm::RationalNumber> const& model, std::vector<Objective<storm::RationalNumber>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) {
this->weightVectorChecker = std::unique_ptr<SparsePcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>>(new SparseMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>(model, objectives, possibleECActions, possibleBottomStates));
}
template<>
void SparsePcaaQuery<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton<double> const& model, std::vector<Objective<double>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) {
this->weightVectorChecker = std::unique_ptr<SparsePcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>>(new SparseMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>(model, objectives, possibleECActions, possibleBottomStates));
}
template<>
void SparsePcaaQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton<storm::RationalNumber> const& model, std::vector<Objective<storm::RationalNumber>> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) {
this->weightVectorChecker = std::unique_ptr<SparsePcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>>(new SparseMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(model, objectives, possibleECActions, possibleBottomStates));
}
template <class SparseModelType, typename GeometryValueType>
typename SparsePcaaQuery<SparseModelType, GeometryValueType>::WeightVector SparsePcaaQuery<SparseModelType, GeometryValueType>::findSeparatingVector(Point const& pointToBeSeparated) {
STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(pointToBeSeparated)) << ".");

12
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h

@ -3,7 +3,7 @@
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h"
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h"
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/storage/geometry/Polytope.h"
namespace storm {
@ -39,14 +39,6 @@ namespace storm {
protected:
/*
* Initializes the weight vector checker with the provided data from preprocessing
*/
void initializeWeightVectorChecker(SparseModelType const& model,
std::vector<Objective<typename SparseModelType::ValueType>> const& objectives,
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates);
/*
* Represents the information obtained in a single iteration of the algorithm
*/
@ -108,7 +100,7 @@ namespace storm {
std::vector<Objective<typename SparseModelType::ValueType>> objectives;
// The corresponding weight vector checker
std::unique_ptr<SparsePcaaWeightVectorChecker<SparseModelType>> weightVectorChecker;
std::unique_ptr<PcaaWeightVectorChecker<SparseModelType>> weightVectorChecker;
//The results in each iteration of the algorithm
std::vector<RefinementStep> refinementSteps;

91
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@ -28,10 +28,9 @@ namespace storm {
std::vector<Objective<typename SparseModelType::ValueType>> const& objectives,
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates) :
model(model),
objectives(objectives),
PcaaWeightVectorChecker<SparseModelType>(model, objectives),
possibleECActions(possibleECActions),
actionsWithoutRewardInUnboundedPhase(model.getNumberOfChoices(), true),
actionsWithoutRewardInUnboundedPhase(this->model.getNumberOfChoices(), true),
possibleBottomStates(possibleBottomStates),
objectivesWithNoUpperTimeBound(objectives.size(), false),
discreteActionRewards(objectives.size()),
@ -39,15 +38,15 @@ namespace storm {
objectiveResults(objectives.size()),
offsetsToUnderApproximation(objectives.size()),
offsetsToOverApproximation(objectives.size()),
optimalChoices(model.getNumberOfStates(), 0) {
optimalChoices(this->model.getNumberOfStates(), 0) {
// set data for unbounded objectives
for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
auto const& formula = *objectives[objIndex].formula;
auto const& formula = *this->objectives[objIndex].formula;
if (formula.getSubformula().isTotalRewardFormula()) {
objectivesWithNoUpperTimeBound.set(objIndex, true);
STORM_LOG_ASSERT(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), "Unexpected type of operator formula.");
actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()).getChoicesWithZeroReward(model.getTransitionMatrix());
actionsWithoutRewardInUnboundedPhase &= this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()).getChoicesWithZeroReward(this->model.getTransitionMatrix());
}
}
}
@ -55,14 +54,14 @@ namespace storm {
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) {
checkHasBeenCalled=true;
checkHasBeenCalled = true;
STORM_LOG_INFO("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVector)));
std::vector<ValueType> weightedRewardVector(model.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> weightedRewardVector(this->model.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
boost::optional<ValueType> weightedLowerResultBound = storm::utility::zero<ValueType>();
boost::optional<ValueType> weightedUpperResultBound = storm::utility::zero<ValueType>();
for (auto objIndex : objectivesWithNoUpperTimeBound) {
auto const& obj = objectives[objIndex];
if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) {
auto const& obj = this->objectives[objIndex];
if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
if (obj.lowerResultBound && weightedUpperResultBound) {
weightedUpperResultBound.get() -= weightVector[objIndex] * obj.lowerResultBound.get();
} else {
@ -103,17 +102,7 @@ namespace storm {
// Validate that the results are sufficiently precise
ValueType resultingWeightedPrecision = storm::utility::abs<ValueType>(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector));
resultingWeightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weightVector, weightVector));
STORM_LOG_THROW(resultingWeightedPrecision <= weightedPrecision, storm::exceptions::UnexpectedException, "The desired precision was not reached");
}
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::setWeightedPrecision(ValueType const& weightedPrecision) {
this->weightedPrecision = weightedPrecision;
}
template <class SparseModelType>
typename SparsePcaaWeightVectorChecker<SparseModelType>::ValueType const& SparsePcaaWeightVectorChecker<SparseModelType>::getWeightedPrecision() const {
return this->weightedPrecision;
STORM_LOG_THROW(resultingWeightedPrecision <= this->getWeightedPrecision(), storm::exceptions::UnexpectedException, "The desired precision was not reached");
}
template <class SparseModelType>
@ -160,24 +149,24 @@ namespace storm {
void SparsePcaaWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector, boost::optional<ValueType> const& lowerResultBound, boost::optional<ValueType> const& upperResultBound) {
if (this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) {
this->weightedResult = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
this->optimalChoices = std::vector<uint_fast64_t>(model.getNumberOfStates(), 0);
this->weightedResult = std::vector<ValueType>(this->model.getNumberOfStates(), storm::utility::zero<ValueType>());
this->optimalChoices = std::vector<uint_fast64_t>(this->model.getNumberOfStates(), 0);
return;
}
// Only consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero).
storm::storage::BitVector zeroRewardActions = storm::utility::vector::filterZero(weightedRewardVector);
storm::storage::BitVector nonZeroRewardActions = ~zeroRewardActions;
storm::storage::BitVector nonZeroRewardStates(model.getNumberOfStates(), false);
for(uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state){
if(nonZeroRewardActions.getNextSetIndex(model.getTransitionMatrix().getRowGroupIndices()[state]) < model.getTransitionMatrix().getRowGroupIndices()[state+1]) {
storm::storage::BitVector nonZeroRewardStates(this->model.getNumberOfStates(), false);
for(uint_fast64_t state = 0; state < this->model.getNumberOfStates(); ++state){
if(nonZeroRewardActions.getNextSetIndex(this->model.getTransitionMatrix().getRowGroupIndices()[state]) < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) {
nonZeroRewardStates.set(state);
}
}
storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix().transpose(true), storm::storage::BitVector(model.getNumberOfStates(), true), nonZeroRewardStates);
storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(this->model.getTransitionMatrix().transpose(true), storm::storage::BitVector(this->model.getNumberOfStates(), true), nonZeroRewardStates);
// Remove neutral end components, i.e., ECs in which no reward is earned.
auto ecEliminatorResult = storm::transformer::EndComponentEliminator<ValueType>::transform(model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates);
auto ecEliminatorResult = storm::transformer::EndComponentEliminator<ValueType>::transform(this->model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates);
std::vector<ValueType> subRewardVector(ecEliminatorResult.newToOldRowMapping.size());
storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector);
@ -195,7 +184,7 @@ namespace storm {
}
solver->solveEquations(subResult, subRewardVector);
this->weightedResult = std::vector<ValueType>(model.getNumberOfStates());
this->weightedResult = std::vector<ValueType>(this->model.getNumberOfStates());
transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getSchedulerChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->weightedResult, this->optimalChoices);
}
@ -205,16 +194,16 @@ namespace storm {
if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) {
uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin();
objectiveResults[objIndex] = weightedResult;
if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) {
if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one<ValueType>());
}
for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) {
for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) {
if (objIndex != objIndex2) {
objectiveResults[objIndex2] = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
objectiveResults[objIndex2] = std::vector<ValueType>(this->model.getNumberOfStates(), storm::utility::zero<ValueType>());
}
}
} else {
storm::storage::SparseMatrix<ValueType> deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->optimalChoices, true);
storm::storage::SparseMatrix<ValueType> deterministicMatrix = this->model.getTransitionMatrix().selectRowsFromRowGroups(this->optimalChoices, true);
storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount());
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
@ -225,11 +214,11 @@ namespace storm {
ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound);
for (uint_fast64_t const &objIndex : storm::utility::vector::getSortedIndices(weightVector)) {
auto const& obj = objectives[objIndex];
auto const& obj = this->objectives[objIndex];
if (objectivesWithNoUpperTimeBound.get(objIndex)) {
offsetsToUnderApproximation[objIndex] = storm::utility::zero<ValueType>();
offsetsToOverApproximation[objIndex] = storm::utility::zero<ValueType>();
storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]);
storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, this->model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]);
storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards);
// As maybestates we pick the states from which a state with reward is reachable
storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards);
@ -245,7 +234,7 @@ namespace storm {
storm::utility::vector::clip(objectiveResults[objIndex], obj.lowerResultBound, obj.upperResultBound);
}
// Make sure that the objectiveResult is initialized correctly
objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero<ValueType>());
objectiveResults[objIndex].resize(this->model.getNumberOfStates(), storm::utility::zero<ValueType>());
if (!maybeStates.empty()) {
storm::storage::SparseMatrix<ValueType> submatrix = deterministicMatrix.getSubmatrix(
@ -279,7 +268,7 @@ namespace storm {
sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex];
}
} else {
objectiveResults[objIndex] = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
objectiveResults[objIndex] = std::vector<ValueType>(this->model.getNumberOfStates(), storm::utility::zero<ValueType>());
}
}
}
@ -294,13 +283,13 @@ namespace storm {
std::vector<ValueType>& originalSolution,
std::vector<uint_fast64_t>& originalOptimalChoices) const {
storm::storage::BitVector bottomStates(model.getTransitionMatrix().getRowGroupCount(), false);
storm::storage::BitVector statesThatShouldStayInTheirEC(model.getTransitionMatrix().getRowGroupCount(), false);
storm::storage::BitVector statesWithUndefSched(model.getTransitionMatrix().getRowGroupCount(), false);
storm::storage::BitVector bottomStates(this->model.getTransitionMatrix().getRowGroupCount(), false);
storm::storage::BitVector statesThatShouldStayInTheirEC(this->model.getTransitionMatrix().getRowGroupCount(), false);
storm::storage::BitVector statesWithUndefSched(this->model.getTransitionMatrix().getRowGroupCount(), false);
// Handle all the states for which the choice in the original model is uniquely given by the choice in the reduced model
// Also store some information regarding the remaining states
for(uint_fast64_t state = 0; state < model.getTransitionMatrix().getRowGroupCount(); ++state) {
for(uint_fast64_t state = 0; state < this->model.getTransitionMatrix().getRowGroupCount(); ++state) {
// Check if the state exists in the reduced model, i.e., the mapping retrieves a valid index
uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state];
if(stateInReducedModel < reducedMatrix.getRowGroupCount()) {
@ -309,7 +298,7 @@ namespace storm {
uint_fast64_t chosenRowInOriginalModel = reducedToOriginalChoiceMapping[chosenRowInReducedModel];
// Check if the state is a bottom state, i.e., the chosen row stays inside its EC.
bool stateIsBottom = possibleBottomStates.get(state);
for(auto const& entry : model.getTransitionMatrix().getRow(chosenRowInOriginalModel)) {
for(auto const& entry : this->model.getTransitionMatrix().getRow(chosenRowInOriginalModel)) {
stateIsBottom &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel;
}
if(stateIsBottom) {
@ -317,9 +306,9 @@ namespace storm {
statesThatShouldStayInTheirEC.set(state);
} else {
// Check if the chosen row originaly belonged to the current state (and not to another state of the EC)
if(chosenRowInOriginalModel >= model.getTransitionMatrix().getRowGroupIndices()[state] &&
chosenRowInOriginalModel < model.getTransitionMatrix().getRowGroupIndices()[state+1]) {
originalOptimalChoices[state] = chosenRowInOriginalModel - model.getTransitionMatrix().getRowGroupIndices()[state];
if(chosenRowInOriginalModel >= this->model.getTransitionMatrix().getRowGroupIndices()[state] &&
chosenRowInOriginalModel < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) {
originalOptimalChoices[state] = chosenRowInOriginalModel - this->model.getTransitionMatrix().getRowGroupIndices()[state];
} else {
statesWithUndefSched.set(state);
statesThatShouldStayInTheirEC.set(state);
@ -344,16 +333,16 @@ namespace storm {
// Find a row with zero rewards that only leads to bottom states.
// If the state should stay in its EC, we also need to make sure that all successors map to the same state in the reduced model
uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state];
for(uint_fast64_t row = model.getTransitionMatrix().getRowGroupIndices()[state]; row < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
for(uint_fast64_t row = this->model.getTransitionMatrix().getRowGroupIndices()[state]; row < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
bool rowOnlyLeadsToBottomStates = true;
bool rowStaysInEC = true;
for( auto const& entry : model.getTransitionMatrix().getRow(row)) {
for( auto const& entry : this->model.getTransitionMatrix().getRow(row)) {
rowOnlyLeadsToBottomStates &= bottomStates.get(entry.getColumn());
rowStaysInEC &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel;
}
if(rowOnlyLeadsToBottomStates && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state)) && actionsWithoutRewardInUnboundedPhase.get(row)) {
foundRowForState = true;
originalOptimalChoices[state] = row - model.getTransitionMatrix().getRowGroupIndices()[state];
originalOptimalChoices[state] = row - this->model.getTransitionMatrix().getRowGroupIndices()[state];
break;
}
}
@ -365,15 +354,15 @@ namespace storm {
for(auto state : statesWithUndefSched) {
// Iteratively Try to find a choice such that at least one successor has a defined scheduler.
uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state];
for(uint_fast64_t row = model.getTransitionMatrix().getRowGroupIndices()[state]; row < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
for(uint_fast64_t row = this->model.getTransitionMatrix().getRowGroupIndices()[state]; row < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
bool rowStaysInEC = true;
bool rowLeadsToDefinedScheduler = false;
for(auto const& entry : model.getTransitionMatrix().getRow(row)) {
for(auto const& entry : this->model.getTransitionMatrix().getRow(row)) {
rowStaysInEC &= ( stateInReducedModel == originalToReducedStateMapping[entry.getColumn()]);
rowLeadsToDefinedScheduler |= !statesWithUndefSched.get(entry.getColumn());
}
if(rowLeadsToDefinedScheduler && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state))) {
originalOptimalChoices[state] = row - model.getTransitionMatrix().getRowGroupIndices()[state];
originalOptimalChoices[state] = row - this->model.getTransitionMatrix().getRowGroupIndices()[state];
statesWithUndefSched.set(state, false);
}
}

38
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h

@ -1,11 +1,10 @@
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAWEIGHTVECTORCHECKER_H_
#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAWEIGHTVECTORCHECKER_H_
#pragma once
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/Scheduler.h"
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/utility/vector.h"
namespace storm {
@ -19,7 +18,7 @@ namespace storm {
* - computes for each objective the value induced by this scheduler
*/
template <class SparseModelType>
class SparsePcaaWeightVectorChecker {
class SparsePcaaWeightVectorChecker : public PcaaWeightVectorChecker<SparseModelType> {
public:
typedef typename SparseModelType::ValueType ValueType;
@ -45,7 +44,7 @@ namespace storm {
* - extracts the scheduler that induces this optimum
* - computes for each objective the value induced by this scheduler
*/
void check(std::vector<ValueType> const& weightVector);
virtual void check(std::vector<ValueType> const& weightVector) override;
/*!
* Retrieves the results of the individual objectives at the initial state of the given model.
@ -53,31 +52,15 @@ namespace storm {
* Also note that there is no guarantee that the under/over approximation is in fact correct
* as long as the underlying solution methods are unsound (e.g., standard value iteration).
*/
std::vector<ValueType> getUnderApproximationOfInitialStateResults() const;
std::vector<ValueType> getOverApproximationOfInitialStateResults() const;
/*!
* Sets the precision of this weight vector checker. After calling check() the following will hold:
* Let h_lower and h_upper be two hyperplanes such that
* * the normal vector is the provided weight-vector where the entry for minimizing objectives is negated
* * getUnderApproximationOfInitialStateResults() lies on h_lower and
* * getOverApproximationOfInitialStateResults() lies on h_upper.
* Then the distance between the two hyperplanes is at most weightedPrecision
*/
void setWeightedPrecision(ValueType const& weightedPrecision);
/*!
* Returns the precision of this weight vector checker.
*/
ValueType const& getWeightedPrecision() const;
virtual std::vector<ValueType> getUnderApproximationOfInitialStateResults() const override;
virtual std::vector<ValueType> getOverApproximationOfInitialStateResults() const override;
/*!
* Retrieves a scheduler that induces the current values
* Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown.
* Also note that (currently) the scheduler only supports unbounded objectives.
*/
storm::storage::Scheduler<ValueType> computeScheduler() const;
virtual storm::storage::Scheduler<ValueType> computeScheduler() const override;
protected:
@ -118,10 +101,6 @@ namespace storm {
std::vector<ValueType>& originalSolution,
std::vector<uint_fast64_t>& originalOptimalChoices) const;
// The (preprocessed) model
SparseModelType const& model;
// The (preprocessed) objectives
std::vector<Objective<ValueType>> const& objectives;
// Overapproximation of the set of choices that are part of an end component.
storm::storage::BitVector possibleECActions;
@ -135,8 +114,6 @@ namespace storm {
storm::storage::BitVector objectivesWithNoUpperTimeBound;
// stores the (discretized) state action rewards for each objective.
std::vector<std::vector<ValueType>> discreteActionRewards;
// stores the precision of this weight vector checker.
ValueType weightedPrecision;
// Memory for the solution of the most recent call of check(..)
// becomes true after the first call of check(..)
bool checkHasBeenCalled;
@ -157,4 +134,3 @@ namespace storm {
}
}
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAWEIGHTVECTORCHECKER_H_ */
Loading…
Cancel
Save