Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ExtractMaximalStateFormulasVisitor.cpp
Go to the documentation of this file.
2#include <boost/any.hpp>
3
5
7
8namespace storm {
9namespace logic {
10
11ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas)
12 : extractedFormulas(extractedFormulas), nestingLevel(0) {}
13
14std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, ApToFormulaMap& extractedFormulas) {
15 ExtractMaximalStateFormulasVisitor visitor(extractedFormulas);
16 boost::any result = f.accept(visitor, boost::any());
17 return boost::any_cast<std::shared_ptr<Formula>>(result);
18}
19
20boost::any ExtractMaximalStateFormulasVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
21 if (nestingLevel > 0) {
22 return CloneVisitor::visit(f, data);
23 }
24
25 std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
26 if (left->hasQualitativeResult()) {
27 left = extract(left);
28 }
29
30 std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
31 if (right->hasQualitativeResult()) {
32 right = extract(right);
33 }
34
35 return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanPathFormula>(f.getOperator(), left, right));
36}
37
38boost::any ExtractMaximalStateFormulasVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
39 if (nestingLevel > 0) {
40 return CloneVisitor::visit(f, data);
41 }
42
43 STORM_LOG_THROW(!f.hasMultiDimensionalSubformulas(), storm::exceptions::InvalidOperationException,
44 "Can not extract maximal state formulas for multi-dimensional bounded until");
45
46 std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
47 if (left->hasQualitativeResult()) {
48 left = extract(left);
49 }
50
51 std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
52 if (right->hasQualitativeResult()) {
53 right = extract(right);
54 }
55
56 // Copy bound information
57 std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
58 std::vector<TimeBoundReference> timeBoundReferences;
59 for (uint64_t i = 0; i < f.getDimension(); ++i) {
60 if (f.hasLowerBound(i)) {
61 lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i)));
62 } else {
63 lowerBounds.emplace_back();
64 }
65 if (f.hasUpperBound(i)) {
66 upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i)));
67 } else {
68 upperBounds.emplace_back();
69 }
70 timeBoundReferences.push_back(f.getTimeBoundReference(i));
71 }
72
73 return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
74}
75
76boost::any ExtractMaximalStateFormulasVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
77 if (nestingLevel > 0) {
78 return CloneVisitor::visit(f, data);
79 }
80
81 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
82 if (sub->hasQualitativeResult()) {
83 sub = extract(sub);
84 }
85
86 return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(sub));
87}
88
89boost::any ExtractMaximalStateFormulasVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
90 if (nestingLevel > 0) {
91 return CloneVisitor::visit(f, data);
92 }
93
94 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
95 if (sub->hasQualitativeResult()) {
96 sub = extract(sub);
97 }
98
99 return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(sub));
100}
101
102boost::any ExtractMaximalStateFormulasVisitor::visit(NextFormula const& f, boost::any const& data) const {
103 if (nestingLevel > 0) {
104 return CloneVisitor::visit(f, data);
105 }
106
107 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
108 if (sub->hasQualitativeResult()) {
109 sub = extract(sub);
110 }
111
112 return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(sub));
113}
114
115boost::any ExtractMaximalStateFormulasVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
116 if (nestingLevel > 0) {
117 return CloneVisitor::visit(f, data);
118 }
119
120 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
121 if (sub->hasQualitativeResult()) {
122 sub = extract(sub);
123 }
124
125 return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanPathFormula>(f.getOperator(), sub));
126}
127
128boost::any ExtractMaximalStateFormulasVisitor::visit(UntilFormula const& f, boost::any const& data) const {
129 if (nestingLevel > 0) {
130 return CloneVisitor::visit(f, data);
131 }
132
133 std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
134 if (left->hasQualitativeResult()) {
135 left = extract(left);
136 }
137
138 std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
139 if (right->hasQualitativeResult()) {
140 right = extract(right);
141 }
142
143 return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right));
144}
145
146boost::any ExtractMaximalStateFormulasVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
147 incrementNestingLevel();
148 boost::any result = CloneVisitor::visit(f, data);
149 decrementNestingLevel();
150 return result;
151}
152
153boost::any ExtractMaximalStateFormulasVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
154 incrementNestingLevel();
155 boost::any result = CloneVisitor::visit(f, data);
156 decrementNestingLevel();
157 return result;
158}
159
160boost::any ExtractMaximalStateFormulasVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
161 incrementNestingLevel();
162 boost::any result = CloneVisitor::visit(f, data);
163 decrementNestingLevel();
164 return result;
165}
166
167boost::any ExtractMaximalStateFormulasVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
168 incrementNestingLevel();
169 boost::any result = CloneVisitor::visit(f, data);
170 decrementNestingLevel();
171 return result;
172}
173
174boost::any ExtractMaximalStateFormulasVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
175 incrementNestingLevel();
176 boost::any result = CloneVisitor::visit(f, data);
177 decrementNestingLevel();
178 return result;
179}
180
181std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(std::shared_ptr<Formula> f) const {
182 // We use the string representation of formulae to check if they are equivalent.
183 // Of course, this could be made more elegant if there were an actual operator< and/or operator== for formulae
184
185 std::string label;
186
187 // Find equivalent formula in cache
188 auto it = cachedFormulas.find(f->toString());
189 if (it != cachedFormulas.end()) {
190 // Reuse label of equivalent formula
191 label = it->second;
192 } else {
193 // Create new label
194 label = "p" + std::to_string(extractedFormulas.size());
195 extractedFormulas[label] = f;
196 // Update cache
197 cachedFormulas[f->toString()] = label;
198 }
199
200 return std::make_shared<storm::logic::AtomicLabelFormula>(label);
201}
202
203void ExtractMaximalStateFormulasVisitor::incrementNestingLevel() const {
204 const_cast<std::size_t&>(nestingLevel)++;
205}
206void ExtractMaximalStateFormulasVisitor::decrementNestingLevel() const {
207 STORM_LOG_ASSERT(nestingLevel > 0, "Illegal nesting level decrement");
208 const_cast<std::size_t&>(nestingLevel)--;
209}
210
211} // namespace logic
212} // namespace storm
Formula const & getRightSubformula() const
Formula const & getLeftSubformula() const
TimeBoundReference const & getTimeBoundReference(unsigned i=0) const
bool isLowerBoundStrict(unsigned i=0) const
storm::expressions::Expression const & getUpperBound(unsigned i=0) const
storm::expressions::Expression const & getLowerBound(unsigned i=0) const
bool isUpperBoundStrict(unsigned i=0) const
std::map< std::string, std::shared_ptr< Formula const > > ApToFormulaMap
boost::any accept(FormulaVisitor const &visitor) const
Definition Formula.cpp:16
Formula const & getSubformula() const
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
LabParser.cpp.
Definition cli.cpp:18