ltlsynt: support multiple --tlsf options

* bin/common_finput.cc, bin/common_finput.hh: Add support for
process_tlsf_file.
* bin/ltlsynt.cc: Implement it.
* tests/core/syfco.test: Adjust test case.

bin/common_finput.cc

@@ -308,6 +308,12 @@ job_processor::process_aut_file(const char*)
   throw std::runtime_error("process_aut_file not defined for this tool");
 }
 
+int
+job_processor::process_tlsf_file(const char*)
+{
+  throw std::runtime_error("process_tlsf_file not defined for this tool");
+}
+
 int
 job_processor::process_ltl_file(const char* filename)
 {
@@ -377,6 +383,9 @@ job_processor::run()
         case job_type::AUT_FILENAME:
           error |= process_aut_file(j.str);
           break;
+        case job_type::TLSF_FILENAME:
+          error |= process_tlsf_file(j.str);
+          break;
         default:
           throw std::runtime_error("unexpected job type");
         }

bin/common_finput.hh

@@ -27,7 +27,8 @@
 
 enum class job_type : char { LTL_STRING,
                              LTL_FILENAME,
-                             AUT_FILENAME };
+                             AUT_FILENAME,
+                             TLSF_FILENAME };
 
 struct job
 {
@@ -77,6 +78,9 @@ public:
   virtual int
   process_aut_file(const char* filename);
 
+  virtual int
+  process_tlsf_file(const char* filename);
+
   virtual int
   run();
 

bin/ltlsynt.cc

@@ -157,8 +157,6 @@ 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;
 
@@ -582,6 +580,18 @@ namespace
     return 0;
   }
 
+  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));
+      }
+  }
+
   class ltl_processor final : public job_processor
   {
   private:
@@ -658,19 +668,40 @@ namespace
         print_csv(f);
       return res;
     }
-  };
+
+    int
+    process_tlsf_file(const char* filename) override
+    {
+      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,
+                          const_cast<char*>(filename), nullptr };
+      std::string tlsf_string = read_stdout_of_command(command);
+
+      // The set of atomic proposition will be temporary set to those
+      // given by syfco, unless they were forced from the command-line.
+      bool reset_aps = false;
+      if (!input_aps_.has_value() && !output_aps_.has_value())
+        {
+          reset_aps = true;
+          static char arg5[] = "--print-output-signals";
+          char* command[] = { arg0, arg5,
+                              const_cast<char*>(filename), nullptr };
+          std::string res = read_stdout_of_command(command);
+
+          output_aps_.emplace(std::vector<std::string>{});
+          split_aps(res, *output_aps_);
+        }
+      int res = process_string(tlsf_string, filename);
+      if (reset_aps)
+        output_aps_.reset();
+      return res;
     }
 
-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
@@ -726,9 +757,7 @@ parse_opt(int key, char *arg, struct argp_state *)
                                    simplify_args, simplify_values);
       break;
     case OPT_TLSF:
-      if (opt_tlsf)
+      jobs.emplace_back(arg, job_type::TLSF_FILENAME);
-        error(2, 0, "option --tlsf may only be used once");
-      opt_tlsf = arg;
       break;
     case OPT_VERBOSE:
       gi->verbose_stream = &std::cerr;
@@ -767,28 +796,6 @@ main(int argc, char **argv)
     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(), job_type::LTL_STRING);
-
-        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

tests/core/syfco.test

@@ -44,5 +44,8 @@ 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
+# --tlsf can be used several time
-grep 'option --tlsf may only be used once' stderr
+ltlsynt --tlsf test.tlsf > out1
+ltlsynt --tlsf test.tlsf --tlsf test.tlsf > out2
+cat out1 out1 > out11
+diff out11 out2