From 3f030e23f0bc4eca936f7e7b4893846fc4f5b7d6 Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Wed, 9 Jun 2021 23:14:24 +0200
Subject: [PATCH] allow external ltl2da tools

---
 .../automata/LTL2DeterministicAutomaton.cpp   | 68 +++++++++++++++++--
 .../automata/LTL2DeterministicAutomaton.h     |  8 ++-
 2 files changed, 70 insertions(+), 6 deletions(-)

diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp
index 2d30710bd..0f07e2a4e 100644
--- a/src/storm/automata/LTL2DeterministicAutomaton.cpp
+++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp
@@ -5,6 +5,9 @@
 #include "storm/utility/macros.h"
 #include "storm/exceptions/ExpressionEvaluationException.h"
 #include "storm/exceptions/WrongFormatException.h"
+#include "storm/exceptions/FileIoException.h"
+
+#include <sys/wait.h>
 
 #ifdef STORM_HAVE_SPOT
 #include "spot/tl/formula.hh"
@@ -19,10 +22,13 @@
 namespace storm {
     namespace automata {
 
-        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f, bool dnf) {
+        bool LTL2DeterministicAutomaton::isExternalDaToolSet() {
+            return std::getenv("LTL2DA");
+        }
+
+        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2daInternalTool(std::string const& prefixLtl, bool dnf) {
 #ifdef STORM_HAVE_SPOT
 
-            std::string prefixLtl = f.toPrefixString();
             spot::parsed_formula spotPrefixLtl = spot::parse_prefix_ltl(prefixLtl);
             if(!spotPrefixLtl.errors.empty()){
                 std::ostringstream errorMsg;
@@ -34,12 +40,11 @@ namespace storm {
 
             // Request a deterministic, complete automaton with state-based acceptance
             spot::translator trans = spot::translator();
-            trans.set_type(spot::postprocessor::Generic);  //Generic
+            trans.set_type(spot::postprocessor::Generic);
             trans.set_pref(spot::postprocessor::Deterministic | spot::postprocessor::SBAcc | spot::postprocessor::Complete);
             STORM_LOG_INFO("Construct deterministic automaton for "<< spotFormula);
             auto aut = trans.run(spotFormula);
 
-            // TODO necessary for MDP LTL-MC
             if(!(aut->get_acceptance().is_dnf()) && dnf){
                 STORM_LOG_INFO("Convert acceptance condition "<< aut->get_acceptance() << " into DNF...");
                 // Transform the acceptance condition in disjunctive normal form and merge all the Fin-sets of each clause
@@ -61,5 +66,60 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Spot support.");
 #endif
         }
+
+        // TODO: this is quite hacky, improve robustness
+        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2daExternalTool(std::string const& prefixLtl) {
+
+
+            std::string ltl2da_tool = std::getenv("LTL2DA");
+
+            STORM_LOG_INFO("Calling external LTL->DA tool:   " << ltl2da_tool << " '" << prefixLtl << "' da.hoa");
+
+            pid_t pid;
+
+            pid = fork();
+            STORM_LOG_THROW(pid >= 0, storm::exceptions::FileIoException, "Could not construct deterministic automaton, fork failed");
+
+            if (pid == 0) {
+                // we are in the child process
+                if (execlp(ltl2da_tool.c_str(), ltl2da_tool.c_str(), prefixLtl.c_str(), "da.hoa", NULL) < 0) {
+                    std::cerr << "ERROR: exec failed: " << strerror(errno) << std::endl;
+                    std::exit(1);
+                }
+                // never reached
+                return std::shared_ptr<DeterministicAutomaton>();
+            } else { // in the parent
+                int status;
+
+                // wait for completion
+                while (wait(&status) != pid);
+
+                int rv;
+                if (WIFEXITED(status)) {
+                    rv = WEXITSTATUS(status);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Could not construct deterministic automaton: process aborted");
+                }
+                STORM_LOG_THROW(rv == 0, storm::exceptions::FileIoException, "Could not construct deterministic automaton for " << prefixLtl << ", return code = " << rv);
+
+                // TODO for MDP-MC the acceptance condition must be in DNF, otherwise Exception is thrown during computation if accepting ECs
+                STORM_LOG_INFO("Reading automaton for " << prefixLtl << " from da.hoa");
+
+                return DeterministicAutomaton::parseFromFile("da.hoa");
+            }
+        }
+
+        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f, bool dnf) {
+            std::string prefixLtl = f.toPrefixString();
+
+            storm::automata::DeterministicAutomaton::ptr da;
+            if(isExternalDaToolSet()){
+                da = ltl2daExternalTool(prefixLtl);
+            } else {
+                da = ltl2daInternalTool(prefixLtl, dnf);
+            }
+            return da;
+        }
+
     }
 }
diff --git a/src/storm/automata/LTL2DeterministicAutomaton.h b/src/storm/automata/LTL2DeterministicAutomaton.h
index 32be1ca32..1471922d3 100644
--- a/src/storm/automata/LTL2DeterministicAutomaton.h
+++ b/src/storm/automata/LTL2DeterministicAutomaton.h
@@ -10,14 +10,18 @@ namespace storm {
     }
 
     namespace automata {
-
         // fwd
         class DeterministicAutomaton;
 
-
         class LTL2DeterministicAutomaton {
         public:
             static std::shared_ptr<DeterministicAutomaton> ltl2da(storm::logic::Formula const&, bool dnf);
+
+        private:
+            static bool isExternalDaToolSet();
+
+            static std::shared_ptr<DeterministicAutomaton> ltl2daInternalTool(std::string const& prefixLtl, bool dnf);
+            static std::shared_ptr<DeterministicAutomaton> ltl2daExternalTool(std::string const& prefixLtl);
         };
 
     }