From b6b31f20afa969f342376205ab40e0e2c6a110d8 Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:25:13 +0200
Subject: [PATCH] (MDP-LTL) AcceptanceCondition: extractFromDNF

Convert a generic acceptance condition to DNF.
---
 src/storm/automata/AcceptanceCondition.cpp | 45 ++++++++++++++++++++++
 src/storm/automata/AcceptanceCondition.h   |  3 ++
 2 files changed, 48 insertions(+)

diff --git a/src/storm/automata/AcceptanceCondition.cpp b/src/storm/automata/AcceptanceCondition.cpp
index 4f0a7a02a..59e4f6775 100644
--- a/src/storm/automata/AcceptanceCondition.cpp
+++ b/src/storm/automata/AcceptanceCondition.cpp
@@ -1,5 +1,8 @@
 #include "AcceptanceCondition.h"
 
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidOperationException.h"
+
 namespace storm {
 namespace automata {
 
@@ -79,6 +82,48 @@ bool AcceptanceCondition::isAccepting(const storm::storage::StateBlock& scc, acc
     throw std::runtime_error("Missing case statement");
 }
 
+std::vector<std::vector<AcceptanceCondition::acceptance_expr::ptr>> AcceptanceCondition::extractFromDNF() const {
+    std::vector<std::vector<AcceptanceCondition::acceptance_expr::ptr>> dnf;
+
+    extractFromDNFRecursion(getAcceptanceExpression(), dnf, true);
+
+    return dnf;
+}
+
+
+void AcceptanceCondition::extractFromDNFRecursion(AcceptanceCondition::acceptance_expr::ptr e, std::vector<std::vector<acceptance_expr::ptr>>& dnf, bool topLevel) const {
+    if (topLevel) {
+        if (e->isOR()) {
+            if (e->getLeft()->isOR()) {
+                extractFromDNFRecursion(e->getLeft(), dnf, true);
+            } else {
+                dnf.emplace_back();
+                extractFromDNFRecursion(e->getLeft(), dnf, false);
+            }
+
+            if (e->getRight()->isOR()) {
+                extractFromDNFRecursion(e->getRight(), dnf, true);
+            } else {
+                dnf.emplace_back();
+                extractFromDNFRecursion(e->getRight(), dnf, false);
+            }
+        } else {
+            dnf.emplace_back();
+            extractFromDNFRecursion(e, dnf, false);
+        }
+    } else {
+        if (e->isOR() || e->isNOT()) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Acceptance condition is not in DNF");
+        } else if (e->isAND()) {
+            extractFromDNFRecursion(e->getLeft(), dnf, false);
+            extractFromDNFRecursion(e->getRight(), dnf, false);
+        } else {
+            dnf.back().push_back(e);
+        }
+    }
+}
+
+
 AcceptanceCondition::ptr AcceptanceCondition::lift(std::size_t productNumberOfStates, std::function<std::size_t (std::size_t)> mapping) const {
     AcceptanceCondition::ptr lifted(new AcceptanceCondition(productNumberOfStates, numberOfAcceptanceSets, acceptance));
     for (unsigned int i = 0; i < numberOfAcceptanceSets; i++) {
diff --git a/src/storm/automata/AcceptanceCondition.h b/src/storm/automata/AcceptanceCondition.h
index 7f1b993c8..7434cac4a 100644
--- a/src/storm/automata/AcceptanceCondition.h
+++ b/src/storm/automata/AcceptanceCondition.h
@@ -24,8 +24,11 @@ namespace storm {
             acceptance_expr::ptr getAcceptanceExpression() const;
 
             AcceptanceCondition::ptr lift(std::size_t productNumberOfStates, std::function<std::size_t (std::size_t)> mapping) const;
+
+            std::vector<std::vector<acceptance_expr::ptr>> extractFromDNF() const;
         private:
             bool isAccepting(const storm::storage::StateBlock& scc, acceptance_expr::ptr expr) const;
+            void extractFromDNFRecursion(acceptance_expr::ptr e, std::vector<std::vector<acceptance_expr::ptr>>& dnf, bool topLevel) const;
 
             std::size_t numberOfStates;
             unsigned int numberOfAcceptanceSets;