From 6e5592fe6a16ddd2df23d8555fc73ed9220311fe Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 4 Sep 2024 16:17:46 +0200
Subject: [PATCH] ltlsynt: save source filename with --csv

* bin/ltlsynt.cc (print_csv): Make filename mandatory, and add a
"was_game" argument.
(process_formula, process_aut_file): Adjust calls.
* tests/core/ltlsynt2.test: Adjust test cases.
---
 NEWS                     |  3 +++
 bin/ltlsynt.cc           | 45 +++++++++++++++++++++++++++++-----------
 tests/core/ltlsynt2.test | 38 +++++++++++++++++++++++----------
 3 files changed, 63 insertions(+), 23 deletions(-)

diff --git a/NEWS b/NEWS
index b255d1319..35cd420d4 100644
--- a/NEWS
+++ b/NEWS
@@ -5,6 +5,9 @@ New in spot 2.12.0.dev (not yet released)
   - ltlmix is a new tool that generates formulas by combining existing
     ones. See https://spot.lre.epita.fr/ltlmix.html for examples.
 
+  - ltlsynt --csv=FILENAME will now save the source filename for
+    the processed formulas as the first column of the CSV file.
+
   - ltlsynt learned a --part-file option, to specify the partition of
     input/output proposition from a *.part file, as used in several
     other tools.
diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index f465e2bf7..12f7d1c91 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -334,12 +334,13 @@ 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)
+  print_csv(const spot::formula& f, const char* filename, bool was_game)
   {
     auto& vs = gi->verbose_stream;
     auto& bv = gi->bv;
@@ -357,7 +358,7 @@ namespace
     // (Even if that file was empty initially.)
     if (!outf.append())
       {
-        out << ("\"formula\",\"algo\",\"tot_time\",\"trans_time\","
+        out << ("\"source\",\"formula\",\"algo\",\"tot_time\",\"trans_time\","
                 "\"split_time\",\"todpa_time\"");
         if (!opt_print_pg && !opt_print_hoa)
           {
@@ -374,14 +375,23 @@ namespace
             out << ",\"nb latches\",\"nb gates\"";
         out << '\n';
       }
-    std::ostringstream os;
-    if (filename)
-      os << filename;
-    else
-      os << f;
-    spot::escape_rfc4180(out << '"', os.str()) << "\",";
-     // if a filename was given, assume the game has been read directly
-    if (!filename)
+    {
+      std::ostringstream os;
+      if (filename)
+        {
+          os << filename;
+          spot::escape_rfc4180(out << '"', os.str()) << '"';
+          os.str("");
+          os.clear();
+        }
+      out << ',';
+      if (was_game)
+        os << filename;
+      else
+        os << f;
+      spot::escape_rfc4180(out << '"', os.str()) << "\",";
+    }
+    if (!was_game)
       out << '"' << algo_names[(int) gi->s] << '"';
     out << ',' << bv->total_time
         << ',' << bv->trans_time
@@ -752,7 +762,18 @@ namespace
         filter_list_of_aps(f, filename, linenum);
       int res = solve_formula(f, input_aps, output_aps);
       if (opt_csv)
-        print_csv(f);
+        {
+          if (filename == 0 || linenum <= 0)
+            {
+              print_csv(f, filename, false);
+            }
+          else
+            {
+              std::ostringstream os;
+              os << filename << ':' << linenum;
+              print_csv(f, os.str().c_str(), false);
+            }
+        }
       return res;
     }
 
@@ -951,7 +972,7 @@ namespace
               std::string loc = os.str();
               int res = process_pgame(haut->aut, loc);
               if (res < 2 && opt_csv)
-                print_csv(nullptr, loc.c_str());
+                print_csv(nullptr, loc.c_str(), true);
               err = std::max(err, res);
             }
         }
diff --git a/tests/core/ltlsynt2.test b/tests/core/ltlsynt2.test
index 5e26b28d3..912a76b81 100755
--- a/tests/core/ltlsynt2.test
+++ b/tests/core/ltlsynt2.test
@@ -47,7 +47,8 @@ except ImportError:
 
 x = pandas.read_csv("out.csv")
 x.to_csv('filtered.csv',
-         columns=('formula', 'algo', 'realizable', 'strat_num_states'),
+         columns=('source', 'formula', 'algo',
+                  'realizable', 'strat_num_states'),
          index=False)
 EOF
 
@@ -55,24 +56,39 @@ EOF
 $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,2
+source,formula,algo,realizable,strat_num_states
+formulas.ltl:1,G(i1 <-> Xo1),lar,1,3
+formulas.ltl:2,F(i1 xor i2) <-> Fo1,lar,1,2
+formulas.ltl:3,i1 <-> F(o1 xor o2),lar,1,3
+formulas.ltl:4,Fi1 <-> Go2,lar,0,0
+,o1 & F(i1 <-> o2),lar,1,2
 EOF
 
 diff filtered.csv expected
 
-# ltlfilt should be able to read the first columns
+# ltlfilt should be able to read the second column
 mv filtered.csv input.csv
-ltlsynt --ins=i1,i2 -F input.csv/-1 --csv=out.csv -q && exit 2
+ltlsynt --ins=i1,i2 -F input.csv/-2 --csv=out.csv -q && exit 2
 test $? -eq 1
 $PYTHON test.py
+cat >expected <<EOF
+source,formula,algo,realizable,strat_num_states
+input.csv:2,G(i1 <-> Xo1),lar,1,3
+input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2
+input.csv:4,i1 <-> F(o1 xor o2),lar,1,3
+input.csv:5,Fi1 <-> Go2,lar,0,0
+input.csv:6,o1 & F(i1 <-> o2),lar,1,2
+EOF
 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
+ltlsynt -F input.csv/-2 --csv=out.csv -q || exit 2
 $PYTHON test.py
-diff filtered.csv input.csv
+cat >expected <<EOF
+source,formula,algo,realizable,strat_num_states
+input.csv:2,G(i1 <-> Xo1),lar,1,3
+input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2
+input.csv:4,i1 <-> F(o1 xor o2),lar,1,3
+input.csv:5,o1 & F(i1 <-> o2),lar,1,2
+EOF
+diff filtered.csv expected