From 0521901e9db006ceef1c896cb7abe2506a6a288c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 23 Sep 2022 09:42:15 +0200
Subject: [PATCH] revert c45ff0c94 and add test case showing why

* bin/ltlsynt.cc: Revert c45ff0c94.  Also fix documentation of exit
status.
* tests/core/ltlsynt2.test: New file.
* tests/Makefile.am: Add it.
---
 bin/ltlsynt.cc           | 10 ++++--
 tests/Makefile.am        |  1 +
 tests/core/ltlsynt2.test | 77 ++++++++++++++++++++++++++++++++++++++++
 3 files changed, 85 insertions(+), 3 deletions(-)
 create mode 100755 tests/core/ltlsynt2.test

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 630ccd629..44c55ef54 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -160,8 +160,8 @@ static const struct argp_child children[] =
 const char argp_program_doc[] = "\
 Synthesize a controller from its LTL specification.\v\
 Exit status:\n\
-  0   if the input problem is realizable\n\
-  1   if the input problem is not realizable\n\
+  0   if all input problems were realizable\n\
+  1   if at least one input problem was not realizable\n\
   2   if any error has been reported";
 
 static std::optional<std::vector<std::string>> all_output_aps;
@@ -279,6 +279,10 @@ namespace
       spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n';
   }
 
+  // If filename is passed, it is printed instead of the formula.  We
+  // use that when processing games since we have no formula to print.
+  // It would be cleaner to have two columns: one for location (that's
+  // filename + line number if known), and one for formula (if known).
   static void
   print_csv(const spot::formula& f, const char* filename = nullptr)
   {
@@ -705,7 +709,7 @@ namespace
         }
 
       if (opt_csv)
-        print_csv(f, filename);
+        print_csv(f);
       return res;
     }
 
diff --git a/tests/Makefile.am b/tests/Makefile.am
index 9570f7dcd..2384f115e 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -343,6 +343,7 @@ TESTS_twa = \
   core/parity2.test \
   core/pgsolver.test \
   core/ltlsynt.test \
+  core/ltlsynt2.test \
   core/ltlsynt-pgame.test \
   core/syfco.test \
   core/rabin2parity.test \
diff --git a/tests/core/ltlsynt2.test b/tests/core/ltlsynt2.test
new file mode 100755
index 000000000..dbb754d92
--- /dev/null
+++ b/tests/core/ltlsynt2.test
@@ -0,0 +1,77 @@
+#! /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/>.
+
+
+# More checks for ltlfilt
+
+. ./defs || exit 1
+
+set -e
+
+cat >formulas.ltl <<EOF
+G(i1 <-> Xo1)
+F(i1 xor i2) <-> F(o1)
+i1 <-> F(o1 xor o2)
+F(i1) <-> G(o2)
+EOF
+
+ltlsynt --ins=i1,i2 -F formulas.ltl -f 'o1 & F(i1 <-> o2)' -q --csv=out.csv &&\
+    exit 2
+test $? -eq 1 || exit 2
+
+cat >test.py <<EOF
+import sys
+try:
+  import pandas
+  import numpy as np
+except ImportError:
+  sys.exit(77)
+
+x = pandas.read_csv("out.csv")
+x.to_csv('filtered.csv',
+         columns=('formula', 'algo', 'realizable', 'strat_num_states'),
+         index=False)
+EOF
+
+# will exit 77 if panda is not installed
+$PYTHON test.py
+
+cat >expected <<EOF
+formula,algo,realizable,strat_num_states
+G(i1 <-> Xo1),lar,1,3
+F(i1 xor i2) <-> Fo1,lar,1,2
+i1 <-> F(o1 xor o2),lar,1,3
+Fi1 <-> Go2,lar,0,0
+o1 & F(i1 <-> o2),lar,1,4
+EOF
+
+diff filtered.csv expected
+
+# ltlfilt should be able to read the first columns
+mv filtered.csv input.csv
+ltlsynt --ins=i1,i2 -F input.csv/-1 --csv=out.csv -q && exit 2
+test $? -eq 1
+$PYTHON test.py
+diff filtered.csv expected
+
+grep -v 0,0 filtered.csv >input.csv
+ltlsynt --ins=i1,i2 -F input.csv/-1 --csv=out.csv -q || exit 2
+$PYTHON test.py
+diff filtered.csv input.csv