2#include <boost/any.hpp>
11ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas)
12 : extractedFormulas(extractedFormulas), nestingLevel(0) {}
16 boost::any result = f.
accept(visitor, boost::any());
17 return boost::any_cast<std::shared_ptr<Formula>>(result);
21 if (nestingLevel > 0) {
22 return CloneVisitor::visit(f, data);
25 std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.
getLeftSubformula().
accept(*
this, data));
26 if (left->hasQualitativeResult()) {
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);
35 return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanPathFormula>(f.
getOperator(), left, right));
38boost::any ExtractMaximalStateFormulasVisitor::visit(
BoundedUntilFormula const& f, boost::any
const& data)
const {
39 if (nestingLevel > 0) {
40 return CloneVisitor::visit(f, data);
44 "Can not extract maximal state formulas for multi-dimensional bounded until");
46 std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.
getLeftSubformula().
accept(*
this, data));
47 if (left->hasQualitativeResult()) {
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);
57 std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
58 std::vector<TimeBoundReference> timeBoundReferences;
63 lowerBounds.emplace_back();
68 upperBounds.emplace_back();
73 return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
76boost::any ExtractMaximalStateFormulasVisitor::visit(
EventuallyFormula const& f, boost::any
const& data)
const {
77 if (nestingLevel > 0) {
78 return CloneVisitor::visit(f, data);
81 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.
getSubformula().
accept(*
this, data));
82 if (sub->hasQualitativeResult()) {
86 return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(sub));
89boost::any ExtractMaximalStateFormulasVisitor::visit(
GloballyFormula const& f, boost::any
const& data)
const {
90 if (nestingLevel > 0) {
91 return CloneVisitor::visit(f, data);
94 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.
getSubformula().
accept(*
this, data));
95 if (sub->hasQualitativeResult()) {
99 return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(sub));
102boost::any ExtractMaximalStateFormulasVisitor::visit(
NextFormula const& f, boost::any
const& data)
const {
103 if (nestingLevel > 0) {
104 return CloneVisitor::visit(f, data);
107 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.
getSubformula().
accept(*
this, data));
108 if (sub->hasQualitativeResult()) {
112 return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(sub));
116 if (nestingLevel > 0) {
117 return CloneVisitor::visit(f, data);
120 std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.
getSubformula().
accept(*
this, data));
121 if (sub->hasQualitativeResult()) {
125 return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanPathFormula>(f.
getOperator(), sub));
128boost::any ExtractMaximalStateFormulasVisitor::visit(
UntilFormula const& f, boost::any
const& data)
const {
129 if (nestingLevel > 0) {
130 return CloneVisitor::visit(f, data);
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);
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);
143 return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right));
146boost::any ExtractMaximalStateFormulasVisitor::visit(
TimeOperatorFormula const& f, boost::any
const& data)
const {
147 incrementNestingLevel();
148 boost::any result = CloneVisitor::visit(f, data);
149 decrementNestingLevel();
154 incrementNestingLevel();
155 boost::any result = CloneVisitor::visit(f, data);
156 decrementNestingLevel();
161 incrementNestingLevel();
162 boost::any result = CloneVisitor::visit(f, data);
163 decrementNestingLevel();
168 incrementNestingLevel();
169 boost::any result = CloneVisitor::visit(f, data);
170 decrementNestingLevel();
175 incrementNestingLevel();
176 boost::any result = CloneVisitor::visit(f, data);
177 decrementNestingLevel();
181std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(std::shared_ptr<Formula> f)
const {
188 auto it = cachedFormulas.find(f->toString());
189 if (it != cachedFormulas.end()) {
194 label =
"p" + std::to_string(extractedFormulas.size());
195 extractedFormulas[label] = f;
197 cachedFormulas[f->toString()] = label;
200 return std::make_shared<storm::logic::AtomicLabelFormula>(label);
203void ExtractMaximalStateFormulasVisitor::incrementNestingLevel()
const {
204 const_cast<std::size_t&
>(nestingLevel)++;
206void ExtractMaximalStateFormulasVisitor::decrementNestingLevel()
const {
208 const_cast<std::size_t&
>(nestingLevel)--;
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)