From 393dd2af87b893fff7dc1344911edf269fc66bf0 Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:25:03 +0200
Subject: [PATCH] (LTL) ExtractMaximalStateFormulasVisitor

For PRCTL*-model checking, we need to extract the maximal state
subformulas in a path formula and substitute those with new
labels, e.g., for
 (F P>0.5[...]) & G (s=0 & d=1)
we would get
 (F a_1) & G a_2
as the resulting formula, with
 a_1 => P>0.5[...]
 a_2 => s=0 & d=1

This then allows the recursive computation of the satisfaction sets of
the maximal state subformulas and using those in the computation for
the (simplified) path formula.
---
 .../ExtractMaximalStateFormulasVisitor.cpp    | 170 ++++++++++++++++++
 .../ExtractMaximalStateFormulasVisitor.h      |  43 +++++
 2 files changed, 213 insertions(+)
 create mode 100644 src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp
 create mode 100644 src/storm/logic/ExtractMaximalStateFormulasVisitor.h

diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp
new file mode 100644
index 000000000..d6f465027
--- /dev/null
+++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp
@@ -0,0 +1,170 @@
+#include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
+
+#include "storm/logic/Formulas.h"
+
+#include "storm/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace logic {
+
+        ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(std::vector<LabelFormulaPair>& extractedFormulas) : extractedFormulas(extractedFormulas), nestingLevel(0) {
+        }
+
+        std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, std::vector<LabelFormulaPair>& extractedFormulas) {
+            ExtractMaximalStateFormulasVisitor visitor(extractedFormulas);
+            boost::any result = f.accept(visitor, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            if (nestingLevel > 0) {
+                return CloneVisitor::visit(f, data);
+            }
+
+            std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+            if (left->hasQualitativeResult()) {
+                left = extract(left);
+            }
+
+            std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+            if (right->hasQualitativeResult()) {
+                right = extract(right);
+            }
+
+            return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanPathFormula>(f.getOperator(), left, right));
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            if (nestingLevel > 0) {
+                return CloneVisitor::visit(f, data);
+            }
+
+            STORM_LOG_THROW(true, storm::exceptions::InvalidOperationException, "Can not extract maximal state formulas for bounded until");
+            // never reached
+            return boost::any();
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
+            if (nestingLevel > 0) {
+                return CloneVisitor::visit(f, data);
+            }
+
+            std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            if (sub->hasQualitativeResult()) {
+                sub = extract(sub);
+            }
+
+            return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(sub));
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
+            if (nestingLevel > 0) {
+                return CloneVisitor::visit(f, data);
+            }
+
+            std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            if (sub->hasQualitativeResult()) {
+                sub = extract(sub);
+            }
+
+            return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(sub));
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(NextFormula const& f, boost::any const& data) const {
+            if (nestingLevel > 0) {
+                return CloneVisitor::visit(f, data);
+            }
+
+            std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            if (sub->hasQualitativeResult()) {
+                sub = extract(sub);
+            }
+
+            return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(sub));
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            if (nestingLevel > 0) {
+                return CloneVisitor::visit(f, data);
+            }
+
+            std::shared_ptr<Formula> sub = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            if (sub->hasQualitativeResult()) {
+                sub = extract(sub);
+            }
+
+            return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanPathFormula>(f.getOperator(), sub));
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(UntilFormula const& f, boost::any const& data) const {
+            if (nestingLevel > 0) {
+                return CloneVisitor::visit(f, data);
+            }
+
+            std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+            if (left->hasQualitativeResult()) {
+                left = extract(left);
+            }
+
+            std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+            if (right->hasQualitativeResult()) {
+                right = extract(right);
+            }
+
+            return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right));
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
+            incrementNestingLevel();
+            boost::any result = CloneVisitor::visit(f, data);
+            decrementNestingLevel();
+            return result;
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
+            incrementNestingLevel();
+            boost::any result = CloneVisitor::visit(f, data);
+            decrementNestingLevel();
+            return result;
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+            incrementNestingLevel();
+            boost::any result = CloneVisitor::visit(f, data);
+            decrementNestingLevel();
+            return result;
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
+            incrementNestingLevel();
+            boost::any result = CloneVisitor::visit(f, data);
+            decrementNestingLevel();
+            return result;
+        }
+
+        boost::any ExtractMaximalStateFormulasVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            incrementNestingLevel();
+            boost::any result = CloneVisitor::visit(f, data);
+            decrementNestingLevel();
+            return result;
+        }
+
+        std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(std::shared_ptr<Formula> f) const {
+            std::string label = "p" + std::to_string(extractedFormulas.size());
+
+            const_cast<std::vector<LabelFormulaPair>&>(extractedFormulas).emplace_back(label, f);
+
+            return std::make_shared<storm::logic::AtomicLabelFormula>(label);
+        }
+
+        void ExtractMaximalStateFormulasVisitor::incrementNestingLevel() const {
+            const_cast<std::size_t&>(nestingLevel)++;
+        }
+        void ExtractMaximalStateFormulasVisitor::decrementNestingLevel() const {
+            STORM_LOG_ASSERT(nestingLevel > 0, "Illegal nesting level decrement");
+            const_cast<std::size_t&>(nestingLevel)--;
+        }
+
+
+    }
+}
diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.h b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h
new file mode 100644
index 000000000..e3bd1cea5
--- /dev/null
+++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h
@@ -0,0 +1,43 @@
+#pragma once
+
+#include <vector>
+
+#include "storm/logic/CloneVisitor.h"
+
+namespace storm {
+    namespace logic {
+
+        class ExtractMaximalStateFormulasVisitor : public CloneVisitor {
+        public:
+            typedef std::pair<std::string, std::shared_ptr<Formula const>> LabelFormulaPair;
+
+            static std::shared_ptr<Formula> extract(PathFormula const& f, std::vector<LabelFormulaPair>& extractedFormulas);
+
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+
+        private:
+            ExtractMaximalStateFormulasVisitor(std::vector<LabelFormulaPair>& extractedFormulas);
+
+            std::shared_ptr<Formula> extract(std::shared_ptr<Formula> f) const;
+            void incrementNestingLevel() const;
+            void decrementNestingLevel() const;
+
+            std::vector<LabelFormulaPair>& extractedFormulas;
+            std::size_t nestingLevel;
+        };
+
+    }
+}
+