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

considered solver requirements for multiobjective model checking

tempestpy_adaptions
TimQu 7 years ago
parent
b3349dc344
commit
64ca58494d
6 changed files with 85 additions and 38 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. 15
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
  2. 3
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
  3. 21
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
  4. 2
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h
  5. 72
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  6. 10
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h

15
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
View File

@ -35,6 +35,7 @@ namespace storm {
data.objectives.push_back(std::make_shared<Objective<ValueType>>());
data.objectives.back()->originalFormula = subFormula;
data.finiteRewardCheckObjectives.resize(data.objectives.size(), false);
data.upperResultBoundObjectives.resize(data.objectives.size(), false);
if (data.objectives.back()->originalFormula->isOperatorFormula()) {
preprocessOperatorFormula(data.objectives.back()->originalFormula->asOperatorFormula(), data);
} else {
@ -69,6 +70,16 @@ namespace storm {
}
preprocessedModel->restrictRewardModels(relevantRewardModels);
// Compute upper result bounds wherever this is necessarry
for (auto const& objIndex : data.upperResultBoundObjectives) {
auto const& formula = data.objectives[objIndex]->formula->asRewardOperatorFormula();
auto const& rewModel = preprocessedModel->getRewardModel(formula.getRewardModelName());
// BaierUpperRewardBoundsComputer<ValueType> baier(submatrix, choiceRewards, oneStepTargetProbabilities);
// hintInformation.upperResultBound = baier.computeUpperBound();
}
// Build the actual result
return buildResult(originalModel, originalFormula, data, preprocessedModel, backwardTransitions);
}
@ -330,13 +341,12 @@ namespace storm {
auto totalRewardFormula = std::make_shared<storm::logic::TotalRewardFormula>();
data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(totalRewardFormula, auxRewardModelName, opInfo);
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
data.upperResultBoundObjectives.set(data.objectives.size() - 1, true);
if (formula.isReachabilityRewardFormula()) {
assert(optionalRewardModelName.is_initialized());
data.tasks.push_back(std::make_shared<SparseMultiObjectivePreprocessorReachRewToTotalRewTask<SparseModelType>>(data.objectives.back(), relevantStatesFormula, optionalRewardModelName.get()));
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1);
} else if (formula.isReachabilityTimeFormula() && data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1);
data.tasks.push_back(std::make_shared<SparseMultiObjectivePreprocessorReachTimeToTotalRewTask<SparseModelType>>(data.objectives.back(), relevantStatesFormula));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported.");
@ -358,6 +368,7 @@ namespace storm {
auto totalRewardFormula = std::make_shared<storm::logic::TotalRewardFormula>();
data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(totalRewardFormula, *optionalRewardModelName, opInfo);
data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
data.upperResultBoundObjectives.set(data.objectives.size() - 1, true);
}
template<typename SparseModelType>

3
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
View File

@ -41,6 +41,9 @@ namespace storm {
// Indices of the objectives that require a check for finite reward
storm::storage::BitVector finiteRewardCheckObjectives;
// Indices of the objectives for which we need to compute an upper bound for the result
storm::storage::BitVector upperResultBoundObjectives;
std::string memoryLabelPrefix;
std::string rewardModelNamePrefix;

21
src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
View File

@ -13,6 +13,7 @@
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm {
namespace modelchecker {
@ -72,7 +73,7 @@ namespace storm {
// Initialize a minMaxSolver to compute an optimal scheduler (w.r.t. PS) for each epoch
// No EC elimination is necessary as we assume non-zenoness
std::unique_ptr<MinMaxSolverData> minMax = initMinMaxSolver(PS);
std::unique_ptr<MinMaxSolverData> minMax = initMinMaxSolver(PS, weightVector);
// create a linear equation solver for the model induced by the optimal choice vector.
// the solver will be updated whenever the optimal choice vector has changed.
@ -294,13 +295,27 @@ namespace storm {
}
template <class SparseMaModelType>
std::unique_ptr<typename SparseMaPcaaWeightVectorChecker<SparseMaModelType>::MinMaxSolverData> SparseMaPcaaWeightVectorChecker<SparseMaModelType>::initMinMaxSolver(SubModel const& PS) const {
std::unique_ptr<typename SparseMaPcaaWeightVectorChecker<SparseMaModelType>::MinMaxSolverData> SparseMaPcaaWeightVectorChecker<SparseMaModelType>::initMinMaxSolver(SubModel const& PS, std::vector<ValueType> const& weightVector) const {
std::unique_ptr<MinMaxSolverData> result(new MinMaxSolverData());
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
result->solver = minMaxSolverFactory.create(PS.toPS);
result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
result->solver->setTrackScheduler(true);
result->solver->setCachingEnabled(true);
auto req = result->solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
req.clearNoEndComponents();
boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true));
if (lowerBound) {
result->solver->setLowerBound(lowerBound.get());
req.clearLowerBounds();
}
boost::optional<ValueType> upperBound = this->computeWeightedResultBound(false, weightVector, storm::storage::BitVector(weightVector.size(), true));
if (upperBound) {
result->solver->setUpperBound(upperBound.get());
req.clearUpperBounds();
}
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met.");
result->solver->setRequirementsChecked(true);
result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
result->b.resize(PS.getNumberOfChoices());

2
src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h
View File

@ -117,7 +117,7 @@ namespace storm {
/*!
* Initializes the data for the MinMax solver
*/
std::unique_ptr<MinMaxSolverData> initMinMaxSolver(SubModel const& PS) const;
std::unique_ptr<MinMaxSolverData> initMinMaxSolver(SubModel const& PS, std::vector<ValueType> const& weightVector) const;
/*!
* Initializes the data for the LinEq solver

72
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
View File

@ -19,6 +19,7 @@
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm {
namespace modelchecker {
@ -92,39 +93,17 @@ namespace storm {
void SparsePcaaWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) {
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(transitionMatrix.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 = this->objectives[objIndex];
if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
if (obj.lowerResultBound && weightedUpperResultBound) {
weightedUpperResultBound.get() -= weightVector[objIndex] * obj.lowerResultBound.get();
} else {
weightedUpperResultBound = boost::none;
}
if (obj.upperResultBound && weightedLowerResultBound) {
weightedLowerResultBound.get() -= weightVector[objIndex] * obj.upperResultBound.get();
} else {
weightedLowerResultBound = boost::none;
}
storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], -weightVector[objIndex]);
} else {
if (obj.lowerResultBound && weightedLowerResultBound) {
weightedLowerResultBound.get() += weightVector[objIndex] * obj.lowerResultBound.get();
} else {
weightedLowerResultBound = boost::none;
}
if (obj.upperResultBound && weightedUpperResultBound) {
weightedUpperResultBound.get() += weightVector[objIndex] * obj.upperResultBound.get();
} else {
weightedUpperResultBound = boost::none;
}
storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], weightVector[objIndex]);
}
}
unboundedWeightedPhase(weightedRewardVector, weightedLowerResultBound, weightedUpperResultBound);
unboundedWeightedPhase(weightedRewardVector, weightVector);
unboundedIndividualPhase(weightVector);
// Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound
@ -180,7 +159,28 @@ namespace storm {
}
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector, boost::optional<ValueType> const& lowerResultBound, boost::optional<ValueType> const& upperResultBound) {
boost::optional<typename SparseModelType::ValueType> SparsePcaaWeightVectorChecker<SparseModelType>::computeWeightedResultBound(bool lower, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter) const {
ValueType result = storm::utility::zero<ValueType>();
for (auto const& objIndex : objectiveFilter) {
boost::optional<ValueType> const& objBound = (lower == storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) ? this->objectives[objIndex].upperResultBound : this->objectives[objIndex].lowerResultBound;
if (objBound) {
if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
result -= objBound.get() * weightVector[objIndex];
} else {
result += objBound.get() * weightVector[objIndex];
}
} else {
// If there is an objective without the corresponding bound we can not give guarantees for the weighted sum
return boost::none;
}
}
return result;
}
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector, std::vector<ValueType> const& weightVector) {
if (this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) {
this->weightedResult = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
@ -194,14 +194,22 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> solverFactory;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(ecQuotient->matrix);
solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
solver->setTrackScheduler(true);
if (lowerResultBound) {
solver->setLowerBound(*lowerResultBound);
auto req = solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
req.clearNoEndComponents();
boost::optional<ValueType> lowerBound = computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound);
if (lowerBound) {
solver->setLowerBound(lowerBound.get());
req.clearLowerBounds();
}
if (upperResultBound) {
solver->setUpperBound(*upperResultBound);
boost::optional<ValueType> upperBound = computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound);
if (upperBound) {
solver->setUpperBound(upperBound.get());
req.clearUpperBounds();
}
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met.");
solver->setRequirementsChecked(true);
solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
// Use the (0...0) vector as initial guess for the solution.
std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero<ValueType>());
@ -273,12 +281,16 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(submatrix));
auto req = solver->getRequirements();
if (obj.lowerResultBound) {
req.clearLowerBounds();
solver->setLowerBound(*obj.lowerResultBound);
}
if (obj.upperResultBound) {
solver->setUpperBound(*obj.upperResultBound);
req.clearUpperBounds();
}
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met.");
solver->solveEquations(x, b);
// Set the result for this objective accordingly

10
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h
View File

@ -66,18 +66,24 @@ namespace storm {
void initialize(SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0;
/*!
* Computes the weighted lower and upper bounds for the provided set of objectives.
* @param lower if true, lower result bounds are computed. otherwise upper result bounds
* @param weightVector the weight vector ooof the current check
*/
boost::optional<ValueType> computeWeightedResultBound(bool lower, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter) const;
/*!
* Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives
*
* @param weightedRewardVector the weighted rewards (only considering the unbounded objectives)
*/
void unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector, boost::optional<ValueType> const& lowerResultBound, boost::optional<ValueType> const& upperResultBound);
void unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector, std::vector<ValueType> const& weightVector);
/*!
* Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase
*
* @param weightVector the weight vector of the current check
*/
void unboundedIndividualPhase(std::vector<ValueType> const& weightVector);
Write Preview
Loading…
Cancel
Save