Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMultiObjectivePreprocessorResult.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/optional.hpp>
4#include <memory>
5#include <vector>
6
10
12
13namespace storm {
14namespace modelchecker {
15namespace multiobjective {
16namespace preprocessing {
17
18template<class SparseModelType>
21
22 // Original data
24 SparseModelType const& originalModel;
25
26 // The preprocessed model and objectives
27 std::shared_ptr<SparseModelType> preprocessedModel;
28 std::vector<Objective<typename SparseModelType::ValueType>> objectives;
29
30 // Data about the query
32
33 // Indices of the objectives that can potentially yield infinite reward
35
40
42 uint64_t count = 0;
43 for (auto const& obj : objectives) {
44 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) {
45 ++count;
46 }
47 }
48 return count;
49 }
50
54
56 uint64_t count = 0;
57 for (auto const& obj : objectives) {
58 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
59 ++count;
60 }
61 }
62 return count;
63 }
64
68
70 // Trivial objectives are either total reward formulas, LRA reward formulas or single-dimensional step or time bounded cumulative reward formulas
71 for (auto const& obj : objectives) {
72 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) {
73 continue;
74 }
75 if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
76 continue;
77 }
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())) {
81 continue;
82 }
83 }
84 // Reaching this point means that the objective is considered as non-trivial
85 return false;
86 }
87 return true;
88 }
89
90 void printToStream(std::ostream& out) const {
91 out << "\n---------------------------------------------------------------------------------------------------------------------------------------\n";
92 out << " Multi-objective Query \n";
93 out << "---------------------------------------------------------------------------------------------------------------------------------------\n";
94 out << "\nOriginal Formula: \n";
95 out << "--------------------------------------------------------------\n";
96 out << "\t" << originalFormula << '\n';
97 out << "\nThe query considers " << objectives.size() << " objectives:\n";
98 out << "--------------------------------------------------------------\n";
99 for (auto const& obj : objectives) {
100 obj.printToStream(out);
101 out << '\n';
102 }
103 out << "Number of Long-Run-Average Reward Objectives (after preprocessing): " << getNumberOfLongRunAverageRewardFormulas() << ".\n";
104 out << "Number of Total Reward Objectives (after preprocessing): " << getNumberOfTotalRewardFormulas() << ".\n";
105 out << "--------------------------------------------------------------\n";
106 out << "\nOriginal Model Information:\n";
107 originalModel.printModelInformationToStream(out);
108 out << "\nPreprocessed Model Information:\n";
109 preprocessedModel->printModelInformationToStream(out);
110 out << "\n---------------------------------------------------------------------------------------------------------------------------------------\n";
111 }
112
113 friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorResult<SparseModelType> const& ret) {
114 ret.printToStream(out);
115 return out;
116 }
117};
118} // namespace preprocessing
119} // namespace multiobjective
120} // namespace modelchecker
121} // namespace storm
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
LabParser.cpp.
Definition cli.cpp:18
SparseMultiObjectivePreprocessorResult(storm::logic::MultiObjectiveFormula const &originalFormula, SparseModelType const &originalModel)
friend std::ostream & operator<<(std::ostream &out, SparseMultiObjectivePreprocessorResult< SparseModelType > const &ret)