Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparsePcaaAchievabilityQuery.cpp
Go to the documentation of this file.
2
11
13
14namespace storm {
15namespace modelchecker {
16namespace multiobjective {
17
18template<class SparseModelType, typename GeometryValueType>
21 : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
23 "Invalid query Type");
24 initializeThresholdData();
25
26 // Set the precision of the weight vector checker. Will be refined during the computation
27 this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber<typename SparseModelType::ValueType>(0.1));
28}
29
30template<class SparseModelType, typename GeometryValueType>
32 thresholds.reserve(this->objectives.size());
33 strictThresholds = storm::storage::BitVector(this->objectives.size(), false);
34 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
35 auto const& formula = *this->objectives[objIndex].formula;
36 STORM_LOG_ASSERT(formula.hasBound(), "Achievability query invoked but there is an objective without bound.");
37 thresholds.push_back(formula.template getThresholdAs<GeometryValueType>());
38 if (storm::solver::minimize(formula.getOptimalityType())) {
39 STORM_LOG_ASSERT(!storm::logic::isLowerBound(formula.getBound().comparisonType), "Minimizing objective should not specify an upper bound.");
40 // Values for minimizing objectives will be negated in order to convert them to maximizing objectives.
41 // Hence, we also negate the threshold
42 thresholds.back() *= -storm::utility::one<GeometryValueType>();
43 }
44 strictThresholds.set(objIndex, storm::logic::isStrict(formula.getBound().comparisonType));
45 }
46}
47
48template<class SparseModelType, typename GeometryValueType>
49std::unique_ptr<CheckResult> SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::check(Environment const& env, bool produceScheduler) {
50 STORM_LOG_THROW(!produceScheduler, storm::exceptions::NotImplementedException, "Scheduler computation is not implement for achievability queries.");
51
52 bool result = this->checkAchievability(env);
53
54 return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result));
55}
56
57template<class SparseModelType, typename GeometryValueType>
59 // repeatedly refine the over/ under approximation until the threshold point is either in the under approx. or not in the over approx.
60 while (!this->maxStepsPerformed(env) && !storm::utility::resources::isTerminate()) {
61 WeightVector separatingVector = this->findSeparatingVector(thresholds);
62 this->updateWeightedPrecision(separatingVector);
63 this->performRefinementStep(env, std::move(separatingVector), false); // scheduler computation currently not supported
64 if (!checkIfThresholdsAreSatisfied(this->overApproximation)) {
65 return false;
66 }
67 if (checkIfThresholdsAreSatisfied(this->underApproximation)) {
68 return true;
69 }
70 }
71 STORM_LOG_ERROR("Could not check whether thresholds are achievable: Termination requested or maximum number of refinement steps exceeded.");
72 return false;
73}
74
75template<class SparseModelType, typename GeometryValueType>
76void SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::updateWeightedPrecision(WeightVector const& weights) {
77 // Our heuristic considers the distance between the under- and the over approximation w.r.t. the given direction
78 std::pair<Point, bool> optimizationResOverApprox = this->overApproximation->optimize(weights);
79 if (optimizationResOverApprox.second) {
80 std::pair<Point, bool> optimizationResUnderApprox = this->underApproximation->optimize(weights);
81 if (optimizationResUnderApprox.second) {
82 GeometryValueType distance = storm::utility::vector::dotProduct(optimizationResOverApprox.first, weights) -
83 storm::utility::vector::dotProduct(optimizationResUnderApprox.first, weights);
84 STORM_LOG_ASSERT(distance >= storm::utility::zero<GeometryValueType>(), "Negative distance between under- and over approximation was not expected");
85 // Normalize the distance by dividing it with the Euclidean Norm of the weight-vector
86 distance /= storm::utility::sqrt(storm::utility::vector::dotProduct(weights, weights));
87 distance /= GeometryValueType(2);
88 this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber<typename SparseModelType::ValueType>(distance));
89 }
90 }
91 // do not update the precision if one of the approximations is unbounded in the provided direction
92}
93
94template<class SparseModelType, typename GeometryValueType>
95bool SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::checkIfThresholdsAreSatisfied(
96 std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> const& polytope) {
97 std::vector<storm::storage::geometry::Halfspace<GeometryValueType>> halfspaces = polytope->getHalfspaces();
98 for (auto const& h : halfspaces) {
99 if (storm::utility::isZero(h.distance(thresholds))) {
100 // Check if the threshold point is on the boundary of the halfspace and whether this is violates strict thresholds
101 if (h.isPointOnBoundary(thresholds)) {
102 for (auto strictThreshold : strictThresholds) {
103 if (h.normalVector()[strictThreshold] > storm::utility::zero<GeometryValueType>()) {
104 return false;
105 }
106 }
107 }
108 } else {
109 return false;
110 }
111 }
112 return true;
113}
114
115#ifdef STORM_HAVE_CARL
116template class SparsePcaaAchievabilityQuery<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
117template class SparsePcaaAchievabilityQuery<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
118
119template class SparsePcaaAchievabilityQuery<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>;
120template class SparsePcaaAchievabilityQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>;
121#endif
122} // namespace multiobjective
123} // namespace modelchecker
124} // namespace storm
SparsePcaaAchievabilityQuery(preprocessing::SparseMultiObjectivePreprocessorResult< SparseModelType > &preprocessorResult)
virtual std::unique_ptr< CheckResult > check(Environment const &env, bool produceScheduler) override
std::unique_ptr< PcaaWeightVectorChecker< SparseModelType > > weightVectorChecker
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
#define STORM_LOG_ERROR(message)
Definition logging.h:26
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
bool isLowerBound(ComparisonType t)
bool isStrict(ComparisonType t)
bool constexpr minimize(OptimizationDirection d)
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
T dotProduct(std::vector< T > const &firstOperand, std::vector< T > const &secondOperand)
Computes the dot product (aka scalar product) and returns the result.
Definition vector.h:477
bool isZero(ValueType const &a)
Definition constants.cpp:41
ValueType sqrt(ValueType const &number)
LabParser.cpp.