ltlsynt: add --from-pgame option to read parity games

* bin/common_file.cc, bin/common_file.hh (output_file): Add a
force_append option.
* bin/ltlsynt.cc: Implement the --from-pgame option, and
fix suppot for --csv when multiple inputs are processed.
* NEWS: Mention the new option.
* tests/core/syfco.test: Add a test case.
* tests/core/ltlsynt-pgame.test: New file.
* tests/Makefile.am: Add it.

NEWS

@@ -29,10 +29,13 @@ New in spot 2.10.6.dev  (not 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
+  - ltlsynt has 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.
 
+  - ltlsynt has a new option --from-pgame that takes a parity game in
+    extended HOA format, as used in the Synthesis Competition.
+
   Library:
 
   - A global variable, together with its setters and getters to define the

bin/common_file.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
+// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et
-// l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -22,15 +22,18 @@
 #include <iostream>
 
 
-output_file::output_file(const char* name)
+output_file::output_file(const char* name, bool force_append)
 {
   std::ios_base::openmode mode = std::ios_base::trunc;
   if (name[0] == '>' && name[1] == '>')
     {
-      mode = std::ios_base::app;
       append_ = true;
       name += 2;
     }
+  if (force_append)
+    append_ = true;
+  if (append_)
+    mode = std::ios_base::app;
   if (name[0] == '-' && name[1] == 0)
     {
       os_ = &std::cout;

bin/common_file.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
+// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -33,7 +33,7 @@ public:
   // Open a file for output.  "-" is interpreted as stdout.
   // Names that start with ">>" are opened for append.
   // The function calls error() on... error.
-  output_file(const char* name);
+  output_file(const char* name, bool force_append = false);
 
   void close(const std::string& name);
 

bin/ltlsynt.cc

@@ -23,6 +23,7 @@
 
 #include "common_aoutput.hh"
 #include "common_finput.hh"
+#include "common_hoaread.hh"
 #include "common_setup.hh"
 #include "common_sys.hh"
 #include "common_trans.hh"
@@ -48,6 +49,7 @@ enum
   OPT_BYPASS,
   OPT_CSV,
   OPT_DECOMPOSE,
+  OPT_FROM_PGAME,
   OPT_INPUT,
   OPT_OUTPUT,
   OPT_PRINT,
@@ -73,6 +75,9 @@ static const argp_option options[] =
     { "tlsf", OPT_TLSF, "FILENAME", 0,
       "Read a TLSF specification from FILENAME, and call syfco to "
       "convert it into LTL", 0 },
+    { "from-pgame", OPT_FROM_PGAME, "FILENAME", 0,
+      "Read a parity game in Extended HOA format instead of building it.",
+      0 },
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
     { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0,
@@ -250,7 +255,7 @@ namespace
     };
 
   static void
-  print_csv(const spot::formula& f)
+  print_csv(const spot::formula& f, const char* filename = nullptr)
   {
     auto& vs = gi->verbose_stream;
     auto& bv = gi->bv;
@@ -259,7 +264,9 @@ namespace
     if (vs)
       *vs << "writing CSV to " << opt_csv << '\n';
 
-    output_file outf(opt_csv);
+    static bool not_first_time = false;
+    output_file outf(opt_csv, not_first_time);
+    not_first_time = true;      // force append on next print.
     std::ostream& out = outf.ostream();
 
     // Do not output the header line if we append to a file.
@@ -284,10 +291,15 @@ namespace
         out << '\n';
       }
     std::ostringstream os;
+    if (filename)
+      os << filename;
+    else
       os << f;
-    spot::escape_rfc4180(out << '"', os.str());
+    spot::escape_rfc4180(out << '"', os.str()) << "\",";
-    out << "\",\"" << algo_names[(int) gi->s]
+     // if a filename was given, assume the game has been read directly
-        << "\"," << bv->total_time
+    if (!filename)
+      out << '"' << algo_names[(int) gi->s] << '"';
+    out << ',' << bv->total_time
         << ',' << bv->trans_time
         << ',' << bv->split_time
         << ',' << bv->paritize_time;
@@ -319,6 +331,8 @@ namespace
                 const std::vector<std::string>& input_aps,
                 const std::vector<std::string>& output_aps)
   {
+    if (opt_csv)              // reset benchmark data
+      gi->bv = spot::synthesis_info::bench_var();
     spot::stopwatch sw;
     if (gi->bv)
       sw.start();
@@ -386,7 +400,7 @@ namespace
       [](const spot::twa_graph_ptr& game)->void
         {
           if (opt_print_pg)
-            pg_print(std::cout, game);
+            spot::pg_print(std::cout, game);
           else
             spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n';
         }
@@ -438,6 +452,8 @@ namespace
               safe_tot_time();
               return 1;
             }
+          if (gi->bv)
+            gi->bv->realizable = true;
           // Create the (partial) strategy
           // only if we need it
           if (!opt_real)
@@ -701,6 +717,141 @@ namespace
       return res;
     }
 
+    int process_pgame(spot::twa_graph_ptr arena,
+                      const std::string& location)
+    {
+      if (opt_csv)              // reset benchmark data
+        gi->bv = spot::synthesis_info::bench_var();
+      spot::stopwatch sw_global;
+      spot::stopwatch sw_local;
+      if (gi->bv)
+        {
+          sw_global.start();
+          sw_local.start();
+        }
+      if (!arena->get_named_prop<bdd>("synthesis-outputs"))
+        {
+          std::cerr << location << ": controllable-AP is not specified\n";
+          return 2;
+        }
+      if (!arena->get_named_prop<std::vector<bool>>("state-player"))
+        arena = spot::split_2step(arena, true);
+      // FIXME: If we do not split the game, we should check that it is
+      // alternating.
+      spot::change_parity_here(arena,
+                               spot::parity_kind_max,
+                               spot::parity_style_odd);
+      spot::colorize_parity_here(arena, true);
+      if (gi->bv)
+        {
+          gi->bv->split_time += sw_local.stop();
+          gi->bv->nb_states_arena += arena->num_states();
+          auto spptr =
+            arena->get_named_prop<std::vector<bool>>("state-player");
+          assert(spptr);
+          gi->bv->nb_states_arena_env +=
+            std::count(spptr->cbegin(), spptr->cend(), false);
+        }
+      if (opt_print_pg || opt_print_hoa)
+        {
+          if (opt_print_pg)
+            spot::pg_print(std::cout, arena);
+          else
+            spot::print_hoa(std::cout, arena, opt_print_hoa_args) << '\n';
+          return 0;
+        }
+      auto safe_tot_time = [&]() {
+        if (gi->bv)
+          gi->bv->total_time = sw_global.stop();
+      };
+      if (!spot::solve_game(arena, *gi))
+        {
+          std::cout << "UNREALIZABLE" << std::endl;
+          safe_tot_time();
+          return 1;
+        }
+      if (gi->bv)
+        gi->bv->realizable = true;
+      std::cout << "REALIZABLE" << std::endl;
+      if (opt_real)
+        {
+          safe_tot_time();
+          return 0;
+        }
+      sw_local.start();
+      spot::twa_graph_ptr mealy_like =
+        spot::solved_game_to_mealy(arena, *gi);
+      // Keep the machine split for aiger otherwise, separate it.
+      spot::simplify_mealy_here(mealy_like, *gi, opt_print_aiger);
+
+      automaton_printer printer;
+      spot::process_timer timer_printer_dummy;
+      if (opt_print_aiger)
+        {
+          if (gi->bv)
+            sw_local.start();
+          spot::aig_ptr saig =
+            spot::mealy_machine_to_aig(mealy_like, opt_print_aiger);
+          if (gi->bv)
+            {
+              gi->bv->aig_time = sw_local.stop();
+              gi->bv->nb_latches = saig->num_latches();
+              gi->bv->nb_gates = saig->num_gates();
+            }
+          if (gi->verbose_stream)
+            {
+              *gi->verbose_stream << "AIG circuit was created in "
+                                  << gi->bv->aig_time
+                                  << " seconds and has " << saig->num_latches()
+                                  << " latches and "
+                                  << saig->num_gates() << " gates\n";
+            }
+          spot::print_aiger(std::cout, saig) << '\n';
+        }
+      else
+        {
+          printer.print(mealy_like, timer_printer_dummy);
+        }
+      safe_tot_time();
+      return 0;
+    }
+
+    int
+    process_aut_file(const char* filename) override
+    {
+      spot::automaton_stream_parser hp(filename);
+      int err = 0;
+      while (!abort_run)
+        {
+          spot::parsed_aut_ptr haut = hp.parse(spot::make_bdd_dict());
+          if (!haut->aut && haut->errors.empty())
+            break;
+          if (haut->format_errors(std::cerr))
+            err = 2;
+          if (!haut->aut /*|| (err && abort_on_error_)*/)
+            {
+              error(2, 0, "failed to read automaton from %s",
+                    haut->filename.c_str());
+            }
+          else if (haut->aborted)
+            {
+              std::cerr << haut->filename << ':' << haut->loc
+                        << ": aborted input automaton\n";
+              err = std::max(err, 2);
+            }
+          else
+            {
+              std::ostringstream os;
+              os << haut->filename << ':' << haut->loc;
+              std::string loc = os.str();
+              int res = process_pgame(haut->aut, loc);
+              if (res < 2 && opt_csv)
+                print_csv(nullptr, loc.c_str());
+              err = std::max(err, res);
+            }
+        }
+      return err;
+    }
   };
 }
 
@@ -719,13 +870,14 @@ parse_opt(int key, char *arg, struct argp_state *)
       break;
     case OPT_CSV:
       opt_csv = arg ? arg : "-";
-      if (not gi->bv)
-        gi->bv = spot::synthesis_info::bench_var();
       break;
     case OPT_DECOMPOSE:
       opt_decompose_ltl = XARGMATCH("--decompose", arg,
                                     decompose_args, decompose_values);
       break;
+    case OPT_FROM_PGAME:
+      jobs.emplace_back(arg, job_type::AUT_FILENAME);
+      break;
     case OPT_INPUT:
       {
         all_input_aps.emplace(std::vector<std::string>{});

tests/Makefile.am

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

tests/core/ltlsynt-pgame.test

@@ -0,0 +1,157 @@
+#! /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
+
+# From SYNTCOMP
+cat >aut7.hoa <<EOF
+HOA: v1
+name: "GFa | G(b <-> Xa)"
+Start: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+AP: 2 "a" "b"
+controllable-AP: 1
+properties: explicit-labels trans-labels
+--BODY--
+State: 0
+ [t] 1
+ [1] 2
+ [!1] 3
+State: 1 "GFa"
+ [0] 1 {0}
+ [!0] 1
+State: 2 "a & G(b <-> Xa)" {0}
+ [0&1] 2
+ [0&!1] 3
+State: 3 "!a & G(b <-> Xa)" {0}
+ [!0&1] 2
+ [!0&!1] 3
+--END--
+EOF
+
+test UNREALIZABLE = `ltlsynt --realizability --from-pgame aut7.hoa`
+
+grep -v controllable-AP aut7.hoa > aut7b.hoa
+run 2 ltlsynt --realizability --from-pgame aut7b.hoa 2>stderr
+grep 'aut7b.*controllable-AP' stderr
+
+
+# From SYNTCOMP
+cat >UnderapproxDemo2.ehoa <<EOF
+HOA: v1
+States: 4
+Start: 0
+AP: 4 "u0y0x" "u0y0y" "p0p0p0x" "p0p0p0y"
+controllable-AP: 1 0
+acc-name: parity max even 3
+Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))
+properties: trans-labels explicit-labels trans-acc colored complete
+properties: deterministic
+--BODY--
+State: 0
+[!0&1&2&!3 | 0&!1&2&!3] 1 {1}
+[!0&1&!2&!3 | 0&!1&!2&!3] 0 {2}
+[!0&1&3 | 0&!1&3] 2 {1}
+[!0&!1 | 0&1] 3 {1}
+State: 1
+[!0&1&!3 | 0&!1&!3] 1 {1}
+[!0&1&3 | 0&!1&3] 2 {1}
+[!0&!1 | 0&1] 3 {1}
+State: 2
+[!0&1 | 0&!1] 2 {2}
+[!0&!1 | 0&1] 3 {1}
+State: 3
+[t] 3 {1}
+--END--
+EOF
+
+test UNREALIZABLE = `ltlsynt --realizability --from-pgame UnderapproxDemo2.ehoa`
+
+# From SYNTCOMP
+cat >starve.ehoa <<EOF
+HOA: v1
+name: "G(!r | Fg)"
+States: 2
+Start: 0
+AP: 2 "r" "g"
+acc-name: parity min odd 3
+Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
+properties: trans-labels explicit-labels trans-acc colored complete
+properties: deterministic stutter-invariant
+controllable-AP: 1
+--BODY--
+State: 0
+[!0 | 1] 0 {1}
+[0&!1] 1 {2}
+State: 1
+[1] 0 {1}
+[!1] 1 {2}
+--END--
+EOF
+
+test REALIZABLE = `ltlsynt --realizability --from-pgame starve.ehoa`
+
+cat >expect <<EOF
+REALIZABLE
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "r" "g"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+controllable-AP: 1
+--BODY--
+State: 0
+[!0] 0
+[0&1] 0
+--END--
+EOF
+ltlsynt --from-pgame starve.ehoa >results
+diff expect results
+
+ltlsynt --realizability --from-pgame starve.ehoa \
+        --from-pgame UnderapproxDemo2.ehoa \
+        --from-pgame aut7.hoa --csv=out.csv >result || :
+cat >expect <<EOF
+REALIZABLE
+UNREALIZABLE
+UNREALIZABLE
+EOF
+diff result expect
+cat out.csv
+test 4 = `wc -l < out.csv`
+
+ltlsynt --from-pgame starve.ehoa \
+        --from-pgame UnderapproxDemo2.ehoa \
+        --from-pgame aut7.hoa --csv=out.csv >result || :
+test 4 = `wc -l < out.csv`
+cut -d, -f 9,10,11,12,13 <out.csv >right
+end='"strat_num_states","strat_num_edges"'
+cat >expect <<EOF
+"realizable","dpa_num_states","dpa_num_states_env",$end
+1,4,2,1,2
+0,9,4,0,0
+0,10,5,0,0
+EOF
+diff right expect

tests/core/syfco.test

@@ -49,3 +49,7 @@ ltlsynt --tlsf test.tlsf > out1
 ltlsynt --tlsf test.tlsf --tlsf test.tlsf > out2
 cat out1 out1 > out11
 diff out11 out2
+
+ltlsynt --tlsf test.tlsf --tlsf test.tlsf --print-game > pgame.hoa
+ltlsynt --from-pgame pgame.hoa > out3
+diff out2 out3