From 6404c526e2221bba6cd0e3094dd891094a653144 Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:25:01 +0200
Subject: [PATCH] WIP (LTL) LTL2DeterministicAutomaton (first hacky attempt)

Requires a script ltl2da on the PATH that takes two arguments, first
an LTL formula in prefix format, second the DA automaton output
filename. E.g., it could be called via

ltl2da "& p1 F G p0" out.hoa

and should produce a complete deterministic automaton (with arbitrary
acceptance) for the LTL formula 'p1 & F (G p0)' and write it to the
out.hoa file.

Optionally, you can set the LTL2DA environment variable to provide
the path to the script, e.g., invoking storm via

LTL2DA=../ltl2da-script bin/storm ...
---
 .../automata/LTL2DeterministicAutomaton.cpp   | 61 +++++++++++++++++++
 .../automata/LTL2DeterministicAutomaton.h     | 24 ++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 src/storm/automata/LTL2DeterministicAutomaton.cpp
 create mode 100644 src/storm/automata/LTL2DeterministicAutomaton.h

diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp
new file mode 100644
index 000000000..8a4275c60
--- /dev/null
+++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp
@@ -0,0 +1,61 @@
+#include "storm/automata/LTL2DeterministicAutomaton.h"
+#include "storm/automata/DeterministicAutomaton.h"
+
+#include "storm/logic/Formula.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/FileIoException.h"
+
+#include <cstring>
+#include <cerrno>
+#include <cstdlib>
+#include <unistd.h> // for execlp
+#include <sys/wait.h>
+
+namespace storm {
+    namespace automata {
+
+        // TODO: this is quite hacky, improve robustness
+        std::shared_ptr<DeterministicAutomaton> LTL2DeterministicAutomaton::ltl2da(storm::logic::Formula const& f) {
+            std::string prefixLtl = f.toPrefixString();
+
+            std::string ltl2da_tool = "ltl2da";
+            if (const char* ltl2da_env = std::getenv("LTL2DA")) {
+                ltl2da_tool = ltl2da_env;
+            }
+
+            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);
+
+                STORM_LOG_INFO("Reading automaton for " << prefixLtl << " from da.hoa");
+                return DeterministicAutomaton::parseFromFile("da.hoa");
+            }
+        }
+    }
+}
diff --git a/src/storm/automata/LTL2DeterministicAutomaton.h b/src/storm/automata/LTL2DeterministicAutomaton.h
new file mode 100644
index 000000000..c39f1b235
--- /dev/null
+++ b/src/storm/automata/LTL2DeterministicAutomaton.h
@@ -0,0 +1,24 @@
+#pragma
+
+#include <memory>
+
+namespace storm {
+
+    namespace logic {
+        // fwd
+        class Formula;
+    }
+
+    namespace automata {
+
+        // fwd
+        class DeterministicAutomaton;
+
+
+        class LTL2DeterministicAutomaton {
+        public:
+            static std::shared_ptr<DeterministicAutomaton> ltl2da(storm::logic::Formula const& f);
+        };
+
+    }
+}