15namespace modelchecker {
16namespace multiobjective {
18template<
class SparseModelType,
typename GeometryValueType>
21 :
SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
23 "Invalid query Type");
24 initializeThresholdData();
27 this->
weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber<typename SparseModelType::ValueType>(0.1));
30template<
class SparseModelType,
typename GeometryValueType>
32 thresholds.reserve(this->objectives.size());
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>());
42 thresholds.back() *= -storm::utility::one<GeometryValueType>();
48template<
class SparseModelType,
typename GeometryValueType>
50 STORM_LOG_THROW(!produceScheduler, storm::exceptions::NotImplementedException,
"Scheduler computation is not implement for achievability queries.");
52 bool result = this->checkAchievability(env);
57template<
class SparseModelType,
typename GeometryValueType>
61 WeightVector separatingVector = this->findSeparatingVector(thresholds);
62 this->updateWeightedPrecision(separatingVector);
63 this->performRefinementStep(env, std::move(separatingVector),
false);
64 if (!checkIfThresholdsAreSatisfied(this->overApproximation)) {
67 if (checkIfThresholdsAreSatisfied(this->underApproximation)) {
71 STORM_LOG_ERROR(
"Could not check whether thresholds are achievable: Termination requested or maximum number of refinement steps exceeded.");
75template<
class SparseModelType,
typename GeometryValueType>
76void SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::updateWeightedPrecision(WeightVector
const& weights) {
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) {
84 STORM_LOG_ASSERT(distance >= storm::utility::zero<GeometryValueType>(),
"Negative distance between under- and over approximation was not expected");
87 distance /= GeometryValueType(2);
88 this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber<typename SparseModelType::ValueType>(distance));
94template<
class SparseModelType,
typename GeometryValueType>
95bool SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::checkIfThresholdsAreSatisfied(
97 std::vector<storm::storage::geometry::Halfspace<GeometryValueType>> halfspaces = polytope->getHalfspaces();
98 for (
auto const& h : halfspaces) {
101 if (h.isPointOnBoundary(thresholds)) {
102 for (
auto strictThreshold : strictThresholds) {
103 if (h.normalVector()[strictThreshold] > storm::utility::zero<GeometryValueType>()) {
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>;
119template class SparsePcaaAchievabilityQuery<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>;
120template class SparsePcaaAchievabilityQuery<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>;
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.
#define STORM_LOG_ERROR(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
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.
bool isZero(ValueType const &a)
ValueType sqrt(ValueType const &number)