3#include <boost/optional.hpp>
14namespace modelchecker {
15namespace multiobjective {
16namespace preprocessing {
18template<
class SparseModelType>
28 std::vector<Objective<typename SparseModelType::ValueType>>
objectives;
44 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) {
58 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
72 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) {
75 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
78 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isCumulativeRewardFormula()) {
79 auto const& subf = obj.formula->getSubformula().asCumulativeRewardFormula();
80 if (!subf.isMultiDimensional() && (subf.getTimeBoundReference().isTimeBound() || subf.getTimeBoundReference().isStepBound())) {
91 out <<
"\n---------------------------------------------------------------------------------------------------------------------------------------\n";
92 out <<
" Multi-objective Query \n";
93 out <<
"---------------------------------------------------------------------------------------------------------------------------------------\n";
94 out <<
"\nOriginal Formula: \n";
95 out <<
"--------------------------------------------------------------\n";
97 out <<
"\nThe query considers " <<
objectives.size() <<
" objectives:\n";
98 out <<
"--------------------------------------------------------------\n";
100 obj.printToStream(out);
105 out <<
"--------------------------------------------------------------\n";
106 out <<
"\nOriginal Model Information:\n";
108 out <<
"\nPreprocessed Model Information:\n";
110 out <<
"\n---------------------------------------------------------------------------------------------------------------------------------------\n";
A bit vector that is internally represented as a vector of 64-bit values.
bool containsLongRunAverageRewardFormulas() const
uint64_t getNumberOfLongRunAverageRewardFormulas() const
bool containsOnlyTrivialObjectives() const
SparseModelType const & originalModel
SparseMultiObjectivePreprocessorResult(storm::logic::MultiObjectiveFormula const &originalFormula, SparseModelType const &originalModel)
std::shared_ptr< SparseModelType > preprocessedModel
std::vector< Objective< typename SparseModelType::ValueType > > objectives
bool containsOnlyTotalRewardFormulas() const
storm::storage::BitVector maybeInfiniteRewardObjectives
friend std::ostream & operator<<(std::ostream &out, SparseMultiObjectivePreprocessorResult< SparseModelType > const &ret)
storm::logic::MultiObjectiveFormula const & originalFormula
void printToStream(std::ostream &out) const
uint64_t getNumberOfTotalRewardFormulas() const