29namespace modelchecker {
30namespace multiobjective {
31namespace preprocessing {
33template<
typename SparseModelType>
36 std::shared_ptr<SparseModelType> model;
37 std::optional<storm::storage::SparseModelMemoryProductReverseData> memoryIncorporationReverseData;
43 if (produceScheduler) {
44 std::tie(model, memoryIncorporationReverseData) =
51 STORM_LOG_THROW(!produceScheduler, storm::exceptions::NotImplementedException,
"Cannot produce schedulers for the provided memory pattern.");
54 STORM_LOG_THROW(!produceScheduler, storm::exceptions::NotImplementedException,
"Cannot produce schedulers for the provided memory pattern.");
56 }
else if (schedRestr.isPositional()) {
57 model = std::make_shared<SparseModelType>(originalModel);
59 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"The given scheduler restriction has not been implemented.");
62 if (produceScheduler) {
63 std::tie(model, memoryIncorporationReverseData) =
71 boost::optional<std::string> deadlockLabel;
72 if (!produceScheduler) {
74 removeIrrelevantStates(model, deadlockLabel, originalFormula);
77 PreprocessorData data(model);
78 data.deadlockLabel = deadlockLabel;
79 data.memoryIncorporationReverseData = std::move(memoryIncorporationReverseData);
85 data.objectives.back()->originalFormula = subFormula;
86 data.finiteRewardCheckObjectives.resize(data.objectives.size(),
false);
87 data.upperResultBoundObjectives.resize(data.objectives.size(),
false);
88 STORM_LOG_THROW(data.objectives.back()->originalFormula->isOperatorFormula(), storm::exceptions::InvalidPropertyException,
89 "Could not preprocess the subformula " << *subFormula <<
" of " << originalFormula <<
" because it is not supported");
90 preprocessOperatorFormula(data.objectives.back()->originalFormula->asOperatorFormula(), data);
94 std::set<std::string> relevantRewardModels;
95 for (
auto const& obj : data.objectives) {
96 obj->formula->gatherReferencedRewardModels(relevantRewardModels);
98 data.model->restrictRewardModels(relevantRewardModels);
101 return buildResult(originalModel, originalFormula, data);
104template<
typename SparseModelType>
114template<
typename SparseModelType>
115void SparseMultiObjectivePreprocessor<SparseModelType>::removeIrrelevantStates(std::shared_ptr<SparseModelType>& model,
116 boost::optional<std::string>& deadlockLabel,
123 for (
auto const& opFormula : originalFormula.getSubformulas()) {
126 STORM_LOG_THROW(opFormula->isOperatorFormula(), storm::exceptions::InvalidPropertyException,
127 "Could not preprocess the subformula " << *opFormula <<
" of " << originalFormula <<
" because it is not supported");
128 auto const& pathFormula = opFormula->asOperatorFormula().getSubformula();
129 if (opFormula->isProbabilityOperatorFormula()) {
130 if (pathFormula.isUntilFormula()) {
131 auto lhs = mc.check(pathFormula.asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
132 auto rhs = mc.check(pathFormula.asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
135 }
else if (pathFormula.isBoundedUntilFormula()) {
136 if (pathFormula.asBoundedUntilFormula().hasMultiDimensionalSubformulas()) {
139 for (uint64_t i = 0; i < pathFormula.asBoundedUntilFormula().getDimension(); ++i) {
140 auto subPathFormula = pathFormula.asBoundedUntilFormula().restrictToDimension(i);
142 mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula(i))->asExplicitQualitativeCheckResult().getTruthValuesVector();
144 mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula(i))->asExplicitQualitativeCheckResult().getTruthValuesVector();
146 if (pathFormula.asBoundedUntilFormula().hasLowerBound(i)) {
151 absorbingStatesForSubformula &= absorbingStatesForSubSubformula;
154 auto lhs = mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
155 auto rhs = mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
157 if (pathFormula.asBoundedUntilFormula().hasLowerBound()) {
163 }
else if (pathFormula.isGloballyFormula()) {
164 auto phi = mc.check(pathFormula.asGloballyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
168 }
else if (pathFormula.isEventuallyFormula()) {
169 auto phi = mc.check(pathFormula.asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
173 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"The subformula of " << pathFormula <<
" is not supported.");
175 }
else if (opFormula->isRewardOperatorFormula()) {
176 auto const& baseRewardModel = opFormula->asRewardOperatorFormula().hasRewardModelName()
177 ? model->getRewardModel(opFormula->asRewardOperatorFormula().getRewardModelName())
178 : model->getUniqueRewardModel();
179 if (pathFormula.isEventuallyFormula()) {
184 auto phi = mc.check(pathFormula.asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
187 model->getTransitionMatrix(), model->getTransitionMatrix().getRowGroupIndices(), backwardTransitions, statesWithoutReward, phi);
190 }
else if (pathFormula.isCumulativeRewardFormula()) {
195 }
else if (pathFormula.isTotalRewardFormula()) {
199 }
else if (pathFormula.isLongRunAverageRewardFormula()) {
205 absorbingStatesForSubformula =
209 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"The subformula of " << pathFormula <<
" is not supported.");
211 }
else if (opFormula->isTimeOperatorFormula()) {
212 if (pathFormula.isEventuallyFormula()) {
213 auto phi = mc.check(pathFormula.asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
216 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"The subformula of " << pathFormula <<
" is not supported.");
218 }
else if (opFormula->isLongRunAverageOperatorFormula()) {
219 auto lraStates = mc.check(pathFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
223 backwardTransitions, ~lraStates, forallGloballyNotLraStates);
226 "Could not preprocess the subformula " << *opFormula <<
" of " << originalFormula <<
" because it is not supported");
228 absorbingStates &= absorbingStatesForSubformula;
229 if (absorbingStates.empty()) {
234 if (!absorbingStates.empty()) {
237 for (
auto absorbingState : absorbingStates) {
238 for (uint64_t action = model->getTransitionMatrix().getRowGroupIndices()[absorbingState];
239 action < model->getTransitionMatrix().getRowGroupIndices()[absorbingState + 1]; ++action) {
240 subsystemActions.set(action,
false);
245 auto const& submodel =
247 STORM_LOG_INFO(
"Making states absorbing reduced the state space from " << model->getNumberOfStates() <<
" to " << submodel.model->getNumberOfStates()
249 model = submodel.model->template as<SparseModelType>();
250 deadlockLabel = submodel.deadlockLabel;
254template<
typename SparseModelType>
255SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData::PreprocessorData(std::shared_ptr<SparseModelType> model) : model(model) {
257 rewardModelNamePrefix =
"obj";
259 bool prefixIsUnique =
true;
260 for (
auto const& rewardModels : model->getRewardModels()) {
261 if (rewardModelNamePrefix.size() <= rewardModels.first.size()) {
262 if (std::mismatch(rewardModelNamePrefix.begin(), rewardModelNamePrefix.end(), rewardModels.first.begin()).first ==
263 rewardModelNamePrefix.end()) {
264 prefixIsUnique =
false;
265 rewardModelNamePrefix =
"_" + rewardModelNamePrefix;
270 if (prefixIsUnique) {
281 if (considerComplementaryEvent) {
282 opInfo.
bound->threshold = opInfo.
bound->threshold.getManager().rational(storm::utility::one<storm::RationalNumber>()) - opInfo.
bound->threshold;
283 switch (opInfo.
bound->comparisonType) {
297 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"Current objective " << formula <<
" has unexpected comparison type");
301 opInfo.
optimalityType = storm::solver::OptimizationDirection::Maximize;
303 opInfo.
optimalityType = storm::solver::OptimizationDirection::Minimize;
306 "Optimization direction of formula " << formula <<
" ignored as the formula also specifies a threshold.");
310 if (considerComplementaryEvent) {
314 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"Objective " << formula <<
" does not specify whether to minimize or maximize");
319template<
typename SparseModelType>
320void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessOperatorFormula(
storm::logic::OperatorFormula const& formula, PreprocessorData& data) {
338 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"Could not preprocess the objective " << formula <<
" because it is not supported");
342template<
typename SparseModelType>
345 PreprocessorData& data) {
347 data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
348 data.objectives.back()->upperResultBound = storm::utility::one<ValueType>();
359 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"The subformula of " << formula <<
" is not supported.");
363template<
typename SparseModelType>
366 PreprocessorData& data) {
367 std::string rewardModelName;
370 STORM_LOG_THROW(data.model->hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException,
371 "The reward model specified by formula " << formula <<
" does not exist in the model");
375 auto prefixOf = [](std::string
const& left, std::string
const& right) {
376 return std::mismatch(left.begin(), left.end(), right.begin()).first == left.end();
378 bool uniqueRewardModelFound =
false;
379 for (
auto const& rewModel : data.model->getRewardModels()) {
380 if (prefixOf(data.rewardModelNamePrefix, rewModel.first)) {
384 STORM_LOG_THROW(!uniqueRewardModelFound, storm::exceptions::InvalidOperationException,
385 "The formula " << formula <<
" does not specify a reward model name and the reward model is not unique.");
386 uniqueRewardModelFound =
true;
387 rewardModelName = rewModel.first;
389 STORM_LOG_THROW(uniqueRewardModelFound, storm::exceptions::InvalidOperationException,
390 "The formula " << formula <<
" refers to an unnamed reward model but no reward model has been defined.");
393 data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
404 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"The subformula of " << formula <<
" is not supported.");
408template<
typename SparseModelType>
411 data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
416 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"The subformula of " << formula <<
" is not supported.");
420template<
typename SparseModelType>
423 PreprocessorData& data) {
424 data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
425 data.objectives.back()->upperResultBound = storm::utility::one<ValueType>();
429 std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
430 auto lraRewardFormula = std::make_shared<storm::logic::LongRunAverageRewardFormula>();
431 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(lraRewardFormula, rewardModelName, opInfo);
436 std::vector<typename SparseModelType::ValueType> lraRewards(data.model->getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>());
438 data.model->addRewardModel(rewardModelName,
typename SparseModelType::RewardModelType(std::move(lraRewards)));
441template<
typename SparseModelType>
444 std::shared_ptr<storm::logic::Formula const> subformula) {
451 STORM_LOG_THROW((data.model->getInitialStates() & rightSubformulaResult).empty(), storm::exceptions::NotImplementedException,
452 "The Probability for the objective "
453 << *data.objectives.back()->originalFormula
454 <<
" is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented.");
460 notLeftOrRight |= rightSubformulaResult;
463 storm::storage::BitVector allStates(data.model->getNumberOfStates(),
true), noStates(data.model->getNumberOfStates(),
false);
470 reachableFromInit &= ~notLeftOrRight;
472 if ((reachableFromInit & reachableFromGoal).empty()) {
473 STORM_LOG_INFO(
"Objective " << *data.objectives.back()->originalFormula <<
" is transformed to an expected total/cumulative reward property.");
477 std::vector<typename SparseModelType::ValueType> objectiveRewards(data.model->getTransitionMatrix().getRowCount(),
478 storm::utility::zero<typename SparseModelType::ValueType>());
479 for (
auto state : reachableFromInit) {
480 for (uint_fast64_t row = data.model->getTransitionMatrix().getRowGroupIndices()[state];
481 row < data.model->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) {
482 objectiveRewards[row] = data.model->getTransitionMatrix().getConstrainedRowSum(row, rightSubformulaResult);
485 std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
486 data.model->addRewardModel(rewardModelName,
typename SparseModelType::RewardModelType(std::nullopt, std::move(objectiveRewards)));
487 if (subformula ==
nullptr) {
488 subformula = std::make_shared<storm::logic::TotalRewardFormula>();
490 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardModelName, opInfo);
492 STORM_LOG_INFO(
"Objective " << *data.objectives.back()->originalFormula <<
" can not be transformed to an expected total/cumulative reward property.");
493 data.objectives.back()->formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(formula.
asSharedPointer(), opInfo);
497template<
typename SparseModelType>
502 STORM_LOG_INFO(
"Objective " << data.objectives.back()->originalFormula <<
" is not transformed to an expected cumulative reward property.");
503 data.objectives.back()->formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(formula.
asSharedPointer(), opInfo);
505 std::shared_ptr<storm::logic::Formula const> subformula;
508 subformula = std::make_shared<storm::logic::TotalRewardFormula>();
511 storm::exceptions::InvalidPropertyException,
512 "Bounded until formulas for Markov Automata are only allowed when time bounds are considered.");
514 subformula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, formula.
getTimeBoundReference());
517 opInfo, data, subformula);
519 STORM_LOG_THROW(
false, storm::exceptions::InvalidPropertyException,
"Property " << formula <<
"is not supported");
523template<
typename SparseModelType>
527 auto negatedSubformula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not,
533template<
typename SparseModelType>
536 boost::optional<std::string>
const& optionalRewardModelName) {
538 preprocessUntilFormula(
548 storm::storage::BitVector allStates(data.model->getNumberOfStates(),
true), noStates(data.model->getNumberOfStates(),
false);
555 reachableFromInit &= ~subFormulaResult;
558 if ((reachableFromInit & reachableFromGoal).empty()) {
559 STORM_LOG_INFO(
"Objective " << *data.objectives.back()->originalFormula <<
" is transformed to an expected total reward property.");
562 std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
563 auto totalRewardFormula = std::make_shared<storm::logic::TotalRewardFormula>();
564 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(totalRewardFormula, rewardModelName, opInfo);
568 assert(optionalRewardModelName.is_initialized());
569 auto objectiveRewards =
573 objectiveRewards.reduceToStateBasedRewards(data.model->getTransitionMatrix(),
false);
574 if (objectiveRewards.hasStateRewards()) {
576 storm::utility::zero<typename SparseModelType::ValueType>());
578 if (objectiveRewards.hasStateActionRewards()) {
579 for (
auto state : reachableFromGoal) {
580 std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + data.model->getTransitionMatrix().getRowGroupIndices()[state],
581 data.model->getTransitionMatrix().getRowGroupSize(state), storm::utility::zero<typename SparseModelType::ValueType>());
584 data.model->addRewardModel(rewardModelName, std::move(objectiveRewards));
587 std::vector<typename SparseModelType::ValueType> timeRewards(data.model->getNumberOfStates(),
588 storm::utility::zero<typename SparseModelType::ValueType>());
594 storm::utility::one<typename SparseModelType::ValueType>());
598 data.model->addRewardModel(rewardModelName,
typename SparseModelType::RewardModelType(std::move(timeRewards)));
601 "The formula " << formula <<
" neither considers reachability probabilities nor reachability rewards "
603 <<
". This is not supported.");
606 STORM_LOG_INFO(
"Objective " << *data.objectives.back()->originalFormula <<
" can not be transformed to an expected total/cumulative reward property.");
609 assert(optionalRewardModelName.is_initialized());
610 if (data.deadlockLabel) {
613 std::shared_ptr<storm::logic::Formula const> newSubSubformula =
614 std::make_shared<storm::logic::AtomicLabelFormula const>(data.deadlockLabel.get());
615 std::shared_ptr<storm::logic::Formula const> newSubformula = std::make_shared<storm::logic::BinaryBooleanStateFormula const>(
617 boost::optional<storm::logic::RewardAccumulation> newRewardAccumulation;
621 std::shared_ptr<storm::logic::Formula const> newFormula =
622 std::make_shared<storm::logic::EventuallyFormula const>(newSubformula, formula.
getContext(), newRewardAccumulation);
623 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(newFormula, optionalRewardModelName.get(), opInfo);
625 data.objectives.back()->formula =
626 std::make_shared<storm::logic::RewardOperatorFormula>(formula.
asSharedPointer(), optionalRewardModelName.get(), opInfo);
630 std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
632 if (data.deadlockLabel) {
635 std::shared_ptr<storm::logic::Formula const> newSubSubformula =
636 std::make_shared<storm::logic::AtomicLabelFormula const>(data.deadlockLabel.get());
637 newSubformula = std::make_shared<storm::logic::BinaryBooleanStateFormula const>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or,
641 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(newFormula, rewardModelName, opInfo);
642 std::vector<typename SparseModelType::ValueType> timeRewards;
644 timeRewards.assign(data.model->getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>());
648 storm::utility::one<typename SparseModelType::ValueType>());
650 timeRewards.assign(data.model->getNumberOfStates(), storm::utility::one<typename SparseModelType::ValueType>());
652 data.model->addRewardModel(rewardModelName,
typename SparseModelType::RewardModelType(std::move(timeRewards)));
655 "The formula " << formula <<
" neither considers reachability probabilities nor reachability rewards "
657 <<
". This is not supported.");
660 data.finiteRewardCheckObjectives.set(data.objectives.size() - 1,
true);
663template<
typename SparseModelType>
666 PreprocessorData& data,
667 boost::optional<std::string>
const& optionalRewardModelName) {
669 "Cumulative reward formulas are not supported for the given model type.");
670 std::string rewardModelName = optionalRewardModelName.get();
673 if (filteredRewards.isDifferentFromUnfilteredModel()) {
674 std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
675 data.model->addRewardModel(rewardModelName, std::move(filteredRewards.extract()));
678 std::vector<storm::logic::TimeBoundReference> newTimeBoundReferences;
679 bool onlyRewardBounds =
true;
682 if (oldTbr.isRewardBound()) {
683 if (oldTbr.hasRewardAccumulation()) {
685 oldTbr.getRewardAccumulation(), data.model->isDiscreteTimeModel());
686 if (filteredBoundRewards.isDifferentFromUnfilteredModel()) {
687 std::string freshRewardModelName =
688 data.rewardModelNamePrefix + std::to_string(data.objectives.size()) + std::string(
"_" + std::to_string(i));
689 data.model->addRewardModel(freshRewardModelName, std::move(filteredBoundRewards.extract()));
690 newTimeBoundReferences.emplace_back(freshRewardModelName);
693 newTimeBoundReferences.emplace_back(oldTbr.getRewardName());
696 newTimeBoundReferences.push_back(oldTbr);
699 onlyRewardBounds =
false;
700 newTimeBoundReferences.push_back(oldTbr);
704 auto newFormula = std::make_shared<storm::logic::CumulativeRewardFormula>(formula.
getBounds(), newTimeBoundReferences);
705 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(newFormula, rewardModelName, opInfo);
707 if (onlyRewardBounds) {
708 data.finiteRewardCheckObjectives.set(data.objectives.size() - 1,
true);
712template<
typename SparseModelType>
715 boost::optional<std::string>
const& optionalRewardModelName) {
716 std::string rewardModelName = optionalRewardModelName.get();
718 if (filteredRewards.isDifferentFromUnfilteredModel()) {
719 std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
720 data.model->addRewardModel(rewardModelName, filteredRewards.extract());
722 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(formula.
stripRewardAccumulation(), rewardModelName, opInfo);
723 data.finiteRewardCheckObjectives.set(data.objectives.size() - 1,
true);
726template<
typename SparseModelType>
729 PreprocessorData& data,
730 boost::optional<std::string>
const& optionalRewardModelName) {
731 std::string rewardModelName = optionalRewardModelName.get();
733 if (filteredRewards.isDifferentFromUnfilteredModel()) {
734 std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size());
735 data.model->addRewardModel(rewardModelName, std::move(filteredRewards.extract()));
737 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(formula.
stripRewardAccumulation(), rewardModelName, opInfo);
740template<
typename SparseModelType>
741typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMultiObjectivePreprocessor<SparseModelType>::buildResult(
743 ReturnType result(originalFormula, originalModel);
744 auto backwardTransitions = data.model->getBackwardTransitions();
745 result.preprocessedModel = data.model;
746 result.memoryIncorporationReverseData = data.memoryIncorporationReverseData;
748 for (
auto& obj : data.objectives) {
749 result.objectives.push_back(std::move(*obj));
751 result.queryType = getQueryType(result.objectives);
752 result.maybeInfiniteRewardObjectives = std::move(data.finiteRewardCheckObjectives);
757template<
typename SparseModelType>
758typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType::QueryType SparseMultiObjectivePreprocessor<SparseModelType>::getQueryType(
759 std::vector<Objective<ValueType>>
const& objectives) {
760 uint_fast64_t numOfObjectivesWithThreshold = 0;
761 for (
auto& obj : objectives) {
762 if (obj.formula->hasBound()) {
763 ++numOfObjectivesWithThreshold;
766 if (numOfObjectivesWithThreshold == objectives.size()) {
767 return ReturnType::QueryType::Achievability;
768 }
else if (numOfObjectivesWithThreshold + 1 == objectives.size()) {
770 return ReturnType::QueryType::Quantitative;
771 }
else if (numOfObjectivesWithThreshold == 0) {
772 return ReturnType::QueryType::Pareto;
775 "Invalid Multi-objective query: The numer of qualitative objectives should be either 0 (Pareto query), 1 (quantitative query), or "
776 "#objectives (achievability query).");
780template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
781template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>;
783template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<storm::RationalNumber>>;
784template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
ModelCheckerEnvironment & modelchecker()
MultiObjectiveModelCheckerEnvironment & multi()
bool isSchedulerRestrictionSet() const
storm::storage::SchedulerClass const & getSchedulerRestriction() const
bool isRewardBound() const
static ReturnType preprocess(Environment const &env, SparseModelType const &originalModel, storm::logic::MultiObjectiveFormula const &originalFormula, bool produceScheduler)
Preprocesses the given model w.r.t.
This class represents a Markov automaton.
storm::storage::BitVector const & getMarkovianStates() const
Retrieves the set of Markovian states of the model.
A bit vector that is internally represented as a vector of 64-bit values.
void complement()
Negates all bits in the bit vector.
bool isSubsetOf(BitVector const &other) const
Checks whether all bits that are set in the current bit vector are also set in the given bit vector.
size_t size() const
Retrieves the number of bits this bit vector can store.
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
bool isLowerBound(ComparisonType t)
storm::storage::BitVector getOnlyReachableViaPhi(SparseModelType const &model, storm::storage::BitVector const &phi)
storm::logic::OperatorInformation getOperatorInformation(storm::logic::OperatorFormula const &formula, bool considerComplementaryEvent)
OptimizationDirection constexpr invert(OptimizationDirection d)
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceFilter)
Performs a forward depth-first search through the underlying graph structure to identify the states t...
storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 1 of satisfying phi until psi under all possible re...
storm::storage::BitVector performProb0A(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
void setVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Sets the provided values at the provided positions in the given vector.
FilteredRewardModel< RewardModelType > createFilteredRewardModel(RewardModelType const &baseRewardModel, storm::logic::RewardAccumulation const &acc, bool isDiscreteTimeModel)
bool isZero(ValueType const &a)
bool considersComplementaryEvent