ltlsynt: implement --tlsf to call syfco automatically

Fixes #473.

* NEWS, doc/org/ltlsynt.org: Mention it.
* bin/common_trans.cc, bin/common_trans.hh (read_stdout_of_command):
New function.
* bin/ltlsynt.cc: Implement the --tlsf option.
* tests/core/syfco.test: New file.
* tests/Makefile.am: Add it.

NEWS

@@ -17,6 +17,10 @@ New in spot 2.10.4.dev  (net yet released)
   - autcross learned a --language-complemented option to assist in the
     case one is testing tools that complement automata.  (issue #504).
 
+  - ltlsynt as a new option --tlsf that takes the filename of a TLSF
+    specification and calls syfco (which must be installed) to convert
+    it into an LTL formula.
+
   Library:
 
   - The new function suffix_operator_normal_form() implements

bin/common_trans.cc

@@ -27,6 +27,7 @@
 #include <sys/wait.h>
 #include <fcntl.h>
 #include <iomanip>
+#include <fstream>
 #if __has_include(<spawn.h>)
 #define HAVE_SPAWN_H 1
 #include <spawn.h>
@@ -461,6 +462,93 @@ autproc_runner::round_automaton(spot::const_twa_graph_ptr aut, unsigned serial)
   filename_automaton.new_round(aut, serial);
 }
 
+
+std::string
+read_stdout_of_command(char* const* args)
+{
+#if HAVE_SPAWN_H
+  int cout_pipe[2];
+  if (int err = pipe(cout_pipe))
+    error(2, err, "pipe() failed");
+
+  posix_spawn_file_actions_t actions;
+  if (int err = posix_spawn_file_actions_init(&actions))
+    error(2, err, "posix_spawn_file_actions_init() failed");
+
+  posix_spawn_file_actions_addclose(&actions, STDIN_FILENO);
+  posix_spawn_file_actions_addclose(&actions, cout_pipe[0]);
+  posix_spawn_file_actions_adddup2(&actions, cout_pipe[1], STDOUT_FILENO);
+  posix_spawn_file_actions_addclose(&actions, cout_pipe[1]);
+
+  pid_t pid;
+  if (int err = posix_spawnp(&pid, args[0], &actions, nullptr, args, environ))
+    error(2, err, "failed to run '%s'", args[0]);
+
+  if (int err = posix_spawn_file_actions_destroy(&actions))
+    error(2, err, "posix_spawn_file_actions_destroy() failed");
+
+  if (close(cout_pipe[1]) < 0)
+    error(2, errno, "closing write-side of pipe failed");
+
+  std::string buffer(32, 0);
+  std::string results;
+  int bytes_read;
+  for (;;)
+    {
+      static char buffer[512];
+      bytes_read = read(cout_pipe[0], buffer, sizeof(buffer));
+      if (bytes_read > 0)
+        results.insert(results.end(), buffer, buffer + bytes_read);
+      else
+        break;
+    }
+  if (bytes_read < 0)
+    error(2, bytes_read, "failed to read from pipe");
+
+  if (cout_pipe[0] < 0)
+    error(2, errno, "closing read-side of pipe failed");
+
+  int exit_code = 0;
+  if (waitpid(pid, &exit_code, 0) == -1)
+    error(2, errno, "waitpid() failed");
+
+  if (exit_code)
+    error(2, 0, "'%s' exited with status %d", args[0], exit_code);
+
+  return results;
+#else
+  // We could provide a pipe+fork+exec alternative implementation, but
+  // systems without posix_spawn() might also not have fork and exec.
+  // For instance MinGW does not.  So let's fallback to system+tmpfile
+  // instead for maximum portability.
+  char prefix[30];
+  snprintf(prefix, sizeof prefix, "spot-tmp");
+  spot::temporary_file* tmpfile = spot::create_tmpfile(prefix);
+  std::string tmpname = tmpfile->name();
+  std::ostringstream cmd;
+  for (auto t = args; *t != nullptr; ++t)
+    spot::quote_shell_string(cmd, *t) << ' ';
+  cmd << '>';
+  spot::quote_shell_string(cmd, tmpfile->name());
+  std::string cmdstr = cmd.str();
+  int exit_code = system(cmdstr.c_str());
+  if (exit_code < 0)
+    error(2, errno, "failed to execute %s", cmdstr.c_str());
+  if (exit_code > 0)
+    error(2, 0, "'%s' exited with status %d", args[0], exit_code);
+
+  std::ifstream ifs(tmpname,  std::ifstream::in);
+  if (!ifs)
+    error(2, 0, "failed to open %s (output of %s)", tmpname.c_str(), args[0]);
+  ifs.exceptions(std::ifstream::failbit | std::ifstream::badbit);
+  std::stringstream buffer;
+  buffer << ifs.rdbuf();
+  delete tmpfile;
+  return buffer.str();
+#endif
+}
+
+
 std::atomic<bool> timed_out{false};
 unsigned timeout_count = 0;
 
@@ -706,6 +794,7 @@ parse_simple_command(const char* cmd)
   return res;
 }
 
+
 #ifndef HAVE_SPAWN_H
 static void
 exec_command(const char* cmd)

bin/common_trans.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et
+// Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -175,3 +175,9 @@ int exec_with_timeout(const char* cmd);
 #define exec_with_timeout(cmd) system(cmd)
 #define setup_sig_handler() while (0);
 #endif // !ENABLE_TIMEOUT
+
+// Run a command (whose args[0], args[1], etc. are given by args), and
+// return its captured stdout.  Stderr is not captured.  Will abort
+// with an error message if the command is not found, or if it exit
+// with a non-zero status code.
+std::string read_stdout_of_command(char* const* args);

bin/ltlsynt.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2021 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -25,6 +25,7 @@
 #include "common_finput.hh"
 #include "common_setup.hh"
 #include "common_sys.hh"
+#include "common_trans.hh"
 
 #include <spot/misc/bddlt.hh>
 #include <spot/misc/escape.hh>
@@ -54,6 +55,7 @@ enum
   OPT_PRINT_HOA,
   OPT_REAL,
   OPT_SIMPLIFY,
+  OPT_TLSF,
   OPT_VERBOSE,
   OPT_VERIFY
 };
@@ -68,6 +70,9 @@ static const argp_option options[] =
     { "ins", OPT_INPUT, "PROPS", 0,
       "comma-separated list of uncontrollable (a.k.a. input) atomic"
       " propositions", 0 },
+    { "tlsf", OPT_TLSF, "FILENAME", 0,
+      "Read a TLSF specification from FILENAME, and call syfco to "
+      "convert it into LTL", 0 },
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
     { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0,
@@ -152,6 +157,8 @@ static const char* opt_print_hoa_args = nullptr;
 static bool opt_real = false;
 static bool opt_do_verify = false;
 static const char* opt_print_aiger = nullptr;
+static char* opt_tlsf = nullptr;
+static std::string opt_tlsf_string;
 
 static spot::synthesis_info* gi;
 
@@ -486,8 +493,8 @@ namespace
     // If we reach this line
     // a strategy was found for each subformula
     assert(mealy_machines.size() == sub_form.size()
-           && "There are subformula for which no mealy like object"
-                "has been created.");
+           && ("There are subformula for which no mealy like object"
+               " has been created."));
 
     spot::aig_ptr saig = nullptr;
     spot::twa_graph_ptr tot_strat = nullptr;
@@ -646,6 +653,18 @@ namespace
   };
 }
 
+static void
+split_aps(std::string arg, std::vector<std::string>& where)
+{
+  std::istringstream aps(arg);
+  std::string ap;
+  while (std::getline(aps, ap, ','))
+    {
+      ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
+      where.push_back(str_tolower(ap));
+    }
+}
+
 static int
 parse_opt(int key, char *arg, struct argp_state *)
 {
@@ -671,25 +690,13 @@ parse_opt(int key, char *arg, struct argp_state *)
     case OPT_INPUT:
       {
         all_input_aps.emplace(std::vector<std::string>{});
-        std::istringstream aps(arg);
-        std::string ap;
-        while (std::getline(aps, ap, ','))
-          {
-            ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
-            all_input_aps->push_back(str_tolower(ap));
-          }
+        split_aps(arg, *all_input_aps);
         break;
       }
     case OPT_OUTPUT:
       {
         all_output_aps.emplace(std::vector<std::string>{});
-        std::istringstream aps(arg);
-        std::string ap;
-        while (std::getline(aps, ap, ','))
-          {
-            ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
-            all_output_aps->push_back(str_tolower(ap));
-          }
+        split_aps(arg, *all_output_aps);
         break;
       }
     case OPT_PRINT:
@@ -710,6 +717,11 @@ parse_opt(int key, char *arg, struct argp_state *)
       gi->minimize_lvl = XARGMATCH("--simplify", arg,
                                    simplify_args, simplify_values);
       break;
+    case OPT_TLSF:
+      if (opt_tlsf)
+        error(2, 0, "option --tlsf may only be used once");
+      opt_tlsf = arg;
+      break;
     case OPT_VERBOSE:
       gi->verbose_stream = &std::cerr;
       if (not gi->bv)
@@ -746,6 +758,29 @@ main(int argc, char **argv)
                       argp_program_doc, children, nullptr, nullptr };
     if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
       exit(err);
+
+    if (opt_tlsf)
+      {
+        static char arg0[] = "syfco";
+        static char arg1[] = "-f";
+        static char arg2[] = "ltlxba";
+        static char arg3[] = "-m";
+        static char arg4[] = "fully";
+        char* command[] = { arg0, arg1, arg2, arg3, arg4, opt_tlsf, nullptr };
+        opt_tlsf_string = read_stdout_of_command(command);
+        jobs.emplace_back(opt_tlsf_string.c_str(), false);
+
+        if (!all_input_aps.has_value() && !all_output_aps.has_value())
+          {
+            static char arg5[] = "--print-output-signals";
+            char* command[] = { arg0, arg5, opt_tlsf, nullptr };
+            std::string res = read_stdout_of_command(command);
+
+            all_output_aps.emplace(std::vector<std::string>{});
+            split_aps(res, *all_output_aps);
+          }
+      }
+
     check_no_formula();
 
     // Check if inputs and outputs are distinct

doc/org/ltlsynt.org

@@ -104,14 +104,20 @@ specification language created for the purpose of this competition.
 Fortunately, the SYNTCOMP organizers also provide a tool called
 [[https://github.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula.
 
-The following four steps show you how a TLSF specification called =FILE= can
+The following line shows how a TLSF specification called =FILE= can
 be synthesized using =syfco= and =ltlsynt=:
 
 #+BEGIN_SRC sh :export code
-LTL=$(syfco FILE -f ltlxba -m fully)
-IN=$(syfco FILE --print-input-signals)
-OUT=$(syfco FILE --print-output-signals)
-ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"
+ltlsynt --tlsf FILE
+#+END_SRC
+
+The above =--tlsf= option will call =syfco= to perform the conversion
+and extract output signals, as if you had used:
+
+#+BEGIN_SRC sh :export code
+LTL=$(syfco -f ltlxba -m fully FILE)
+OUT=$(syfco --print-output-signals FILE)
+ltlsynt --formula="$LTL" --outs="$OUT"
 #+END_SRC
 
 * Internal details

tests/Makefile.am

@@ -342,6 +342,7 @@ TESTS_twa = \
   core/parity.test \
   core/parity2.test \
   core/ltlsynt.test \
+  core/syfco.test \
   core/rabin2parity.test \
   core/twacube.test
 

tests/core/syfco.test

@@ -0,0 +1,48 @@
+#! /bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs || exit 1
+set -e
+
+# Test that we can pass a tlsf specification to ltlsynt.  This
+# only work if syfco is installed.
+
+(syfco --version) || exit 77
+
+cat >test.tlsf <<EOF
+INFO {
+  TITLE:       "example"
+  DESCRIPTION: "test case"
+  SEMANTICS:   Mealy
+  TARGET:      Mealy
+}
+MAIN {
+  INPUTS { in; }
+  OUTPUTS { out; }
+  GUARANTEE { G((in) <-> X(out)); }
+}
+EOF
+
+test REALIZABLE = `ltlsynt --tlsf test.tlsf --realizability`
+test UNREALIZABLE = `ltlsynt --tlsf test.tlsf --outs=foo --realizability`
+test UNREALIZABLE = `ltlsynt --outs=foo --tlsf test.tlsf --realizability`
+
+ltlsynt --tlsf test.tlsf  --tlsf test.tlsf 2>stderr && exit 0
+grep 'option --tlsf may only be used once' stderr