Browse Source
WeighedObjectives model checking, first version for multi-objective achievability queries
WeighedObjectives model checking, first version for multi-objective achievability queries
Former-commit-id: 484795cc7c
main
13 changed files with 600 additions and 42 deletions
-
13src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
-
42src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp
-
2src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h
-
137src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp
-
64src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.h
-
16src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h
-
163src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp
-
90src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.h
-
18src/storage/TotalScheduler.cpp
-
19src/storage/TotalScheduler.h
-
16src/storage/geometry/Polytope.cpp
-
21src/storage/geometry/Polytope.h
-
41src/utility/vector.h
@ -0,0 +1,137 @@ |
|||||
|
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.h"
|
||||
|
|
||||
|
#include "src/adapters/CarlAdapter.h"
|
||||
|
#include "src/models/sparse/Mdp.h"
|
||||
|
#include "src/models/sparse/StandardRewardModel.h"
|
||||
|
#include "src/utility/constants.h"
|
||||
|
|
||||
|
#include "src/exceptions/UnexpectedException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::SparseMultiObjectiveModelCheckerHelper(Information& info) : info(info), weightedObjectivesChecker(info) { |
||||
|
overApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope(); |
||||
|
underApproximation = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope(); |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::~SparseMultiObjectiveModelCheckerHelper() { |
||||
|
// Intentionally left empty
|
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
void SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::achievabilityQuery() { |
||||
|
Point queryPoint; |
||||
|
queryPoint.reserve(info.objectives.size()); |
||||
|
for(auto const& obj : info.objectives) { |
||||
|
STORM_LOG_THROW(obj.threshold, storm::exceptions::UnexpectedException, "Can not perform achievabilityQuery: No threshold given for at least one objective."); |
||||
|
queryPoint.push_back(storm::utility::convertNumber<RationalNumberType>(*obj.threshold)); |
||||
|
} |
||||
|
achievabilityQuery(queryPoint); |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
void SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::achievabilityQuery(Point const& queryPoint) { |
||||
|
storm::storage::BitVector individualObjectivesToBeChecked(info.objectives.size(), true); |
||||
|
while(true) { //TODO introduce convergence criterion? (like max num of iterations)
|
||||
|
storm::storage::geometry::Halfspace<RationalNumberType> separatingHalfspace = findSeparatingHalfspace(queryPoint, individualObjectivesToBeChecked); |
||||
|
|
||||
|
weightedObjectivesChecker.check(storm::utility::vector::convertNumericVector<ModelValueType>(separatingHalfspace.normalVector())); |
||||
|
storm::storage::TotalScheduler scheduler = weightedObjectivesChecker.getScheduler(); |
||||
|
Point weightedObjectivesResult = storm::utility::vector::convertNumericVector<RationalNumberType>(weightedObjectivesChecker.getInitialStateResultOfObjectives()); |
||||
|
|
||||
|
// Insert the computed scheduler and check whether we have already seen it before
|
||||
|
auto schedulerInsertRes = schedulers.insert(std::make_pair(std::move(scheduler), paretoOptimalPoints.end())); |
||||
|
if(schedulerInsertRes.second){ |
||||
|
// The scheduler is new, so insert the newly computed pareto optimal point.
|
||||
|
// To each scheduler, we assign the (unique) pareto optimal point it induces.
|
||||
|
schedulerInsertRes.first->second = paretoOptimalPoints.insert(std::make_pair(std::move(weightedObjectivesResult), std::vector<WeightVector>())).first; |
||||
|
} |
||||
|
// In the case where the scheduler is not new, we assume that the corresponding pareto optimal points for the old and new scheduler are equal
|
||||
|
// Note that the values might not be exactly equal due to numerical issues.
|
||||
|
|
||||
|
Point const& paretoPoint = schedulerInsertRes.first->second->first; |
||||
|
std::vector<WeightVector>& weightVectors = schedulerInsertRes.first->second->second; |
||||
|
weightVectors.push_back(std::move(separatingHalfspace.normalVector())); |
||||
|
|
||||
|
updateOverApproximation(paretoPoint, weightVectors.back()); |
||||
|
if(!overApproximation->contains(queryPoint)){ |
||||
|
std::cout << "PROPERTY VIOLATED" << std::endl; |
||||
|
return; |
||||
|
} |
||||
|
updateUnderApproximation(); |
||||
|
if(underApproximation->contains(queryPoint)){ |
||||
|
std::cout << "PROPERTY SATISFIED" << std::endl; |
||||
|
return; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
storm::storage::geometry::Halfspace<RationalNumberType> SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::findSeparatingHalfspace(Point const& pointToBeSeparated, storm::storage::BitVector& individualObjectivesToBeChecked) { |
||||
|
// First, we check 'simple' weight vectors that correspond to checking a single objective
|
||||
|
while (!individualObjectivesToBeChecked.empty()){ |
||||
|
uint_fast64_t objectiveIndex = individualObjectivesToBeChecked.getNextSetIndex(0); |
||||
|
individualObjectivesToBeChecked.set(objectiveIndex, false); |
||||
|
|
||||
|
WeightVector normalVector; // = (0..0 1 0..0)
|
||||
|
normalVector.reserve(info.objectives.size()); |
||||
|
for(uint_fast64_t i = 0; i<info.objectives.size(); ++i){ |
||||
|
normalVector.push_back( (i==objectiveIndex) ? storm::utility::one<RationalNumberType>() : storm::utility::zero<RationalNumberType>()); |
||||
|
} |
||||
|
|
||||
|
storm::storage::geometry::Halfspace<RationalNumberType> h(normalVector, storm::utility::vector::dotProduct(normalVector, pointToBeSeparated)); |
||||
|
bool hIsSeparating = true; |
||||
|
for(auto const& paretoPoint : paretoOptimalPoints){ |
||||
|
hIsSeparating &= h.contains(paretoPoint.first); |
||||
|
} |
||||
|
if(hIsSeparating) { |
||||
|
return h; |
||||
|
} |
||||
|
} |
||||
|
return underApproximation->findSeparatingHalfspace(pointToBeSeparated); |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
void SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::updateOverApproximation(Point const& newPoint, WeightVector const& newWeightVector) { |
||||
|
storm::storage::geometry::Halfspace<RationalNumberType> h(newWeightVector, storm::utility::vector::dotProduct(newWeightVector, newPoint)); |
||||
|
overApproximation = overApproximation->intersection(h); |
||||
|
STORM_LOG_DEBUG("Updated OverApproximation to polytope " << overApproximation->toString(true)); |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
void SparseMultiObjectiveModelCheckerHelper<SparseModelType, RationalNumberType>::updateUnderApproximation() { |
||||
|
std::vector<Point> paretoPointsVec; |
||||
|
paretoPointsVec.reserve(paretoOptimalPoints.size()); |
||||
|
for(auto const& paretoPoint : paretoOptimalPoints) { |
||||
|
paretoPointsVec.push_back(paretoPoint.first); |
||||
|
} |
||||
|
|
||||
|
boost::optional<Point> upperBounds; |
||||
|
if(!paretoPointsVec.empty()){ |
||||
|
//Get the pointwise maximum of the pareto points
|
||||
|
upperBounds = paretoPointsVec.front(); |
||||
|
for(auto paretoPointIt = paretoPointsVec.begin()+1; paretoPointIt != paretoPointsVec.end(); ++paretoPointIt){ |
||||
|
auto upperBoundIt = upperBounds->begin(); |
||||
|
for(auto const& paretoPointCoordinate : *paretoPointIt){ |
||||
|
if(paretoPointCoordinate>*upperBoundIt){ |
||||
|
*upperBoundIt = paretoPointCoordinate; |
||||
|
} |
||||
|
++upperBoundIt; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
underApproximation = storm::storage::geometry::Polytope<RationalNumberType>::create(paretoPointsVec)->downwardClosure(upperBounds); |
||||
|
STORM_LOG_DEBUG("Updated UnderApproximation to polytope " << overApproximation->toString(true)); |
||||
|
} |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template class SparseMultiObjectiveModelCheckerHelper<storm::models::sparse::Mdp<double>, storm::RationalNumber>; |
||||
|
#endif
|
||||
|
} |
||||
|
} |
||||
|
} |
@ -0,0 +1,64 @@ |
|||||
|
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERHELPER_H_ |
||||
|
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERHELPER_H_ |
||||
|
|
||||
|
#include <map> |
||||
|
#include <unordered_map> |
||||
|
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h" |
||||
|
#include "src/modelchecker/multiObjective/helper/SparseWeightedObjectivesModelCheckerHelper.h" |
||||
|
#include "src/storage/geometry/Polytope.h" |
||||
|
#include "src/storage/TotalScheduler.h" |
||||
|
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
|
||||
|
template <class SparseModelType, typename RationalNumberType> |
||||
|
class SparseMultiObjectiveModelCheckerHelper { |
||||
|
public: |
||||
|
typedef typename SparseModelType::ValueType ModelValueType; |
||||
|
typedef typename SparseModelType::RewardModelType RewardModelType; |
||||
|
typedef SparseMultiObjectiveModelCheckerInformation<SparseModelType> Information; |
||||
|
|
||||
|
|
||||
|
typedef std::vector<RationalNumberType> Point; |
||||
|
typedef std::vector<RationalNumberType> WeightVector; |
||||
|
|
||||
|
SparseMultiObjectiveModelCheckerHelper(Information& info); |
||||
|
|
||||
|
~SparseMultiObjectiveModelCheckerHelper(); |
||||
|
|
||||
|
void achievabilityQuery(); |
||||
|
|
||||
|
|
||||
|
private: |
||||
|
void achievabilityQuery(Point const& queryPoint); |
||||
|
|
||||
|
/* |
||||
|
* Returns a halfspace h that separates the underapproximation from the given point p, i.e., |
||||
|
* - p lies on the border of h and |
||||
|
* - for each x in the underApproximation, it holds that h contains x |
||||
|
* |
||||
|
* @param pointToBeSeparated the point that is to be seperated |
||||
|
* @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 ) |
||||
|
*/ |
||||
|
storm::storage::geometry::Halfspace<RationalNumberType> findSeparatingHalfspace(Point const& pointToBeSeparated, storm::storage::BitVector& individualObjectivesToBeChecked); |
||||
|
void updateOverApproximation(Point const& newPoint, WeightVector const& newWeightVector); |
||||
|
void updateUnderApproximation(); |
||||
|
|
||||
|
Information& info; |
||||
|
SparseWeightedObjectivesModelCheckerHelper<SparseModelType> weightedObjectivesChecker; |
||||
|
|
||||
|
//TODO: sort points as needed |
||||
|
std::map<Point, std::vector<WeightVector>> paretoOptimalPoints; |
||||
|
std::unordered_map<storm::storage::TotalScheduler, typename std::map<Point, std::vector<WeightVector>>::iterator> schedulers; |
||||
|
|
||||
|
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> overApproximation; |
||||
|
std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> underApproximation; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERHELPER_H_ */ |
@ -0,0 +1,163 @@ |
|||||
|
#include "src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.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/utility/graph.h"
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/utility/solver.h"
|
||||
|
#include "src/utility/vector.h"
|
||||
|
#include "src/exceptions/IllegalFunctionCallException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
|
||||
|
|
||||
|
template <class SparseModelType> |
||||
|
SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::SparseWeightedObjectivesModelCheckerHelper(Information const& info) : info(info), checkHasBeenCalled(false) , objectiveResults(info.objectives.size()){ |
||||
|
|
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType> |
||||
|
void SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::check(std::vector<ValueType> const& weightVector) { |
||||
|
|
||||
|
unboundedWeightedPhase(weightVector); |
||||
|
unboundedIndividualPhase(weightVector); |
||||
|
boundedPhase(weightVector); |
||||
|
checkHasBeenCalled=true; |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType> |
||||
|
std::vector<typename SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::ValueType> SparseWeightedObjectivesModelCheckerHelper<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; |
||||
|
res.reserve(objectiveResults.size()); |
||||
|
for(auto const& objResult : objectiveResults) { |
||||
|
res.push_back(objResult[*info.preprocessedModel.getInitialStates().begin()]); |
||||
|
} |
||||
|
return res; |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType> |
||||
|
storm::storage::TotalScheduler const& SparseWeightedObjectivesModelCheckerHelper<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>()); |
||||
|
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]); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// TODO check for +/- infty reward...
|
||||
|
|
||||
|
|
||||
|
//Testing..
|
||||
|
storm::storage::BitVector test(64); |
||||
|
test.set(63); |
||||
|
std::cout << "Test set index with 0: " << test.getNextSetIndex(0) << std::endl; |
||||
|
std::cout << "Test set index with 63: " << test.getNextSetIndex(63) << std::endl; |
||||
|
std::cout << "Test set index with 64: " << test.getNextSetIndex(64) << std::endl; |
||||
|
|
||||
|
storm::storage::BitVector actionsWithRewards = storm::utility::vector::filter<ValueType>(weightedRewardVector, [&] (ValueType const& value) -> bool {return !storm::utility::isZero(value);}); |
||||
|
storm::storage::BitVector statesWithRewards(info.preprocessedModel.getNumberOfStates(), false); |
||||
|
uint_fast64_t currActionIndex = actionsWithRewards.getNextSetIndex(0); |
||||
|
auto endOfRowGroup = info.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin() + 1; |
||||
|
for(uint_fast64_t state = 0; state<info.preprocessedModel.getNumberOfStates(); ++state){ |
||||
|
if(currActionIndex < *endOfRowGroup){ |
||||
|
statesWithRewards.set(state); |
||||
|
currActionIndex = actionsWithRewards.getNextSetIndex(*endOfRowGroup); |
||||
|
} |
||||
|
++endOfRowGroup; |
||||
|
} |
||||
|
|
||||
|
STORM_LOG_WARN("REMOVE VALIDATION CODE"); |
||||
|
for(uint_fast64_t state = 0; state<info.preprocessedModel.getNumberOfStates(); ++state){ |
||||
|
bool stateHasReward=false; |
||||
|
for(uint_fast64_t row = info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row< info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { |
||||
|
stateHasReward |= actionsWithRewards.get(row); |
||||
|
} |
||||
|
STORM_LOG_ERROR_COND(stateHasReward == statesWithRewards.get(state), "statesWithRewardsVector is wrong!!!!"); |
||||
|
} |
||||
|
|
||||
|
//Get the states from which a state with reward can be reached.
|
||||
|
storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0E(info.preprocessedModel.getTransitionMatrix(), |
||||
|
info.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), |
||||
|
info.preprocessedModel.getBackwardTransitions(), |
||||
|
storm::storage::BitVector(info.preprocessedModel.getNumberOfStates(), true), |
||||
|
statesWithRewards); |
||||
|
|
||||
|
this->weightedResult = std::vector<ValueType>(info.preprocessedModel.getNumberOfStates()); |
||||
|
this->scheduler = storm::storage::TotalScheduler(info.preprocessedModel.getNumberOfStates()); |
||||
|
|
||||
|
storm::storage::SparseMatrix<ValueType> submatrix = info.preprocessedModel.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false); |
||||
|
std::vector<ValueType> b(submatrix.getRowCount()); |
||||
|
storm::utility::vector::selectVectorValues(b, maybeStates, weightedRewardVector); |
||||
|
std::vector<ValueType> x(submatrix.getRowGroupCount(), storm::utility::zero<ValueType>()); |
||||
|
|
||||
|
storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> solverFactory; |
||||
|
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(submatrix, true); |
||||
|
solver->solveEquationSystem(x, b); |
||||
|
|
||||
|
storm::utility::vector::setVectorValues(this->weightedResult, maybeStates, x); |
||||
|
storm::utility::vector::setVectorValues(this->weightedResult, ~maybeStates, storm::utility::zero<ValueType>()); |
||||
|
|
||||
|
uint_fast64_t currentSubState = 0; |
||||
|
for (auto maybeState : maybeStates) { |
||||
|
this->scheduler.setChoice(maybeState, solver->getScheduler().getChoice(currentSubState)); |
||||
|
++currentSubState; |
||||
|
} |
||||
|
// Note that the choices for the ~maybeStates are arbitrary as no states with rewards are reachable any way.
|
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType> |
||||
|
void SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::unboundedIndividualPhase(std::vector<ValueType> const& weightVector) { |
||||
|
|
||||
|
storm::storage::SparseMatrix<ValueType> deterministicMatrix = info.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; |
||||
|
//TODO check if all but one entry of weightVector is zero
|
||||
|
for(uint_fast64_t objIndex = 0; objIndex < weightVector.size(); ++objIndex) { |
||||
|
if(!info.objectives[objIndex].stepBound){ |
||||
|
|
||||
|
storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), info.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), info.preprocessedModel.getRewardModel(info.objectives[objIndex].rewardModelName).getStateActionRewardVector()); |
||||
|
|
||||
|
storm::storage::BitVector statesWithRewards = storm::utility::vector::filter<ValueType>(deterministicStateRewards, [&] (ValueType const& value) -> bool {return !storm::utility::isZero(value);}); |
||||
|
// As target states, we take the states from which no reward is reachable.
|
||||
|
STORM_LOG_WARN("TODO: target state selection is currently only valid for reachability properties..."); |
||||
|
//TODO: we should be able to give some hint to the solver..
|
||||
|
storm::storage::BitVector targetStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); |
||||
|
objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(deterministicMatrix, |
||||
|
deterministicBackwardTransitions, |
||||
|
deterministicStateRewards, |
||||
|
targetStates, |
||||
|
false, //no qualitative checking,
|
||||
|
linearEquationSolverFactory); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <class SparseModelType> |
||||
|
void SparseWeightedObjectivesModelCheckerHelper<SparseModelType>::boundedPhase(std::vector<ValueType> const& weightVector) { |
||||
|
STORM_LOG_WARN("bounded properties not yet implemented"); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
|
||||
|
template class SparseWeightedObjectivesModelCheckerHelper<storm::models::sparse::Mdp<double>>; |
||||
|
|
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
@ -0,0 +1,90 @@ |
|||||
|
#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEWEIGHTEDOBJECTIVESMODELCHECKERHELPER_H_ |
||||
|
#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEWEIGHTEDOBJECTIVESMODELCHECKERHELPER_H_ |
||||
|
|
||||
|
#include <vector> |
||||
|
|
||||
|
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h" |
||||
|
#include "src/storage/TotalScheduler.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace helper { |
||||
|
|
||||
|
/*! |
||||
|
* Helper Class that takes a MultiObjectiveInformation and a weight vector and ... |
||||
|
* - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives |
||||
|
* - extracts the scheduler that induces this maximum |
||||
|
* - computes for each objective the value induced by this scheduler |
||||
|
*/ |
||||
|
template <class SparseModelType> |
||||
|
class SparseWeightedObjectivesModelCheckerHelper { |
||||
|
public: |
||||
|
typedef typename SparseModelType::ValueType ValueType; |
||||
|
typedef typename SparseModelType::RewardModelType RewardModelType; |
||||
|
typedef SparseMultiObjectiveModelCheckerInformation<SparseModelType> Information; |
||||
|
|
||||
|
SparseWeightedObjectivesModelCheckerHelper(Information const& info); |
||||
|
|
||||
|
/*! |
||||
|
* - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives |
||||
|
* - extracts the scheduler that induces this maximum |
||||
|
* - computes for each objective the value induced by this scheduler |
||||
|
*/ |
||||
|
void check(std::vector<ValueType> const& weightVector); |
||||
|
|
||||
|
/*! |
||||
|
* Getter methods for the results of the most recent call of check(..) |
||||
|
* 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; |
||||
|
// A scheduler that induces the optimal values |
||||
|
storm::storage::TotalScheduler const& getScheduler() const; |
||||
|
|
||||
|
|
||||
|
private: |
||||
|
|
||||
|
/*! |
||||
|
* Determines the scheduler that maximizes the weighted reward vector of the unbounded objectives |
||||
|
* |
||||
|
* @param weightVector the weight vector of the current check |
||||
|
*/ |
||||
|
void unboundedWeightedPhase(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); |
||||
|
|
||||
|
/*! |
||||
|
* For each time epoch (starting with the maximal stepBound occurring in the objectives), this method |
||||
|
* - determines the objectives that are relevant in the current time epoch |
||||
|
* - determines the maximizing scheduler for the weighted reward vector of these objectives |
||||
|
* - computes the values of these objectives w.r.t. this scheduler |
||||
|
* |
||||
|
* @param weightVector the weight vector of the current check |
||||
|
*/ |
||||
|
void boundedPhase(std::vector<ValueType> const& weightVector); |
||||
|
|
||||
|
// stores the considered information of the multi-objective model checking problem |
||||
|
Information const& info; |
||||
|
|
||||
|
// becomes true after the first call of check(..) |
||||
|
bool checkHasBeenCalled; |
||||
|
|
||||
|
// The result for the weighted reward vector (for all states of the model) |
||||
|
std::vector<ValueType> weightedResult; |
||||
|
// The results for the individual objectives (for all states of the model) |
||||
|
std::vector<std::vector<ValueType>> objectiveResults; |
||||
|
// The scheduler that maximizes the weighted rewards |
||||
|
storm::storage::TotalScheduler scheduler; |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEWEIGHTEDOBJECTIVESMODELCHECKERHELPER_H_ */ |
Reference in new issue
xxxxxxxxxx