From a22a05b8ec6cf12c57c191f1c40a7779306567bd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 4 Sep 2024 16:33:48 +0200
Subject: [PATCH] ltlsynt: implement --csv-without-formula

* bin/ltlsynt.cc: Implement that new option.
* tests/core/ltlsynt2.test: Test it.
* NEWS: Mention the change.
---
 NEWS                     |  7 +++++--
 bin/ltlsynt.cc           | 30 +++++++++++++++++++++++-------
 tests/core/ltlsynt2.test | 13 ++++++++++++-
 3 files changed, 40 insertions(+), 10 deletions(-)

diff --git a/NEWS b/NEWS
index 35cd420d4..012ca6f32 100644
--- a/NEWS
+++ b/NEWS
@@ -5,8 +5,11 @@ 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 --csv=FILENAME will now save the source filename for the
+    processed formulas as the first column of the CSV file.  A new
+    option --csv-without-formula=FILENAME can be used to save
+    everything but the formula column (as it can be very large, and
+    can be found from the source filename).
 
   - ltlsynt learned a --part-file option, to specify the partition of
     input/output proposition from a *.part file, as used in several
diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 12f7d1c91..ee985b4be 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -50,6 +50,7 @@ enum
   OPT_ALGO = 256,
   OPT_BYPASS,
   OPT_CSV,
+  OPT_CSV_NO_FORMULA,
   OPT_DECOMPOSE,
   OPT_DOT,
   OPT_FROM_PGAME,
@@ -153,6 +154,9 @@ static const argp_option options[] =
       "output statistics as CSV in FILENAME or on standard output "
       "(if '>>' is used to request append mode, the header line is "
       "not output)", 0 },
+    { "csv-without-formula", OPT_CSV_NO_FORMULA, "[>>]FILENAME",
+      OPTION_ARG_OPTIONAL, "like --csv, but without 'fomula' column", 0 },
+    { "csv-no-formula", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
     { "hide-status", OPT_HIDE, nullptr, 0,
       "Hide the REALIZABLE or UNREALIZABLE line.  (Hint: exit status "
       "is enough of an indication.)", 0 },
@@ -182,6 +186,7 @@ Exit status:\n\
   2   if any error has been reported";
 
 static const char* opt_csv = nullptr;
+static bool opt_csv_with_formula = true;
 static bool opt_print_pg = false;
 static bool opt_print_hoa = false;
 static const char* opt_print_hoa_args = nullptr;
@@ -358,7 +363,10 @@ namespace
     // (Even if that file was empty initially.)
     if (!outf.append())
       {
-        out << ("\"source\",\"formula\",\"algo\",\"tot_time\",\"trans_time\","
+        out << "\"source\",";
+        if (opt_csv_with_formula)
+          out << "\"formula\",";
+        out << ("\"algo\",\"tot_time\",\"trans_time\","
                 "\"split_time\",\"todpa_time\"");
         if (!opt_print_pg && !opt_print_hoa)
           {
@@ -385,11 +393,14 @@ namespace
           os.clear();
         }
       out << ',';
-      if (was_game)
-        os << filename;
-      else
-        os << f;
-      spot::escape_rfc4180(out << '"', os.str()) << "\",";
+      if (opt_csv_with_formula)
+        {
+          if (was_game)
+            os << filename;
+          else
+            os << f;
+          spot::escape_rfc4180(out << '"', os.str()) << "\",";
+        }
     }
     if (!was_game)
       out << '"' << algo_names[(int) gi->s] << '"';
@@ -763,7 +774,7 @@ namespace
       int res = solve_formula(f, input_aps, output_aps);
       if (opt_csv)
         {
-          if (filename == 0 || linenum <= 0)
+          if (!filename || linenum <= 0)
             {
               print_csv(f, filename, false);
             }
@@ -996,6 +1007,11 @@ parse_opt(int key, char *arg, struct argp_state *)
       break;
     case OPT_CSV:
       opt_csv = arg ? arg : "-";
+      opt_csv_with_formula = true;
+      break;
+    case OPT_CSV_NO_FORMULA:
+      opt_csv = arg ? arg : "-";
+      opt_csv_with_formula = false;
       break;
     case OPT_DECOMPOSE:
       opt_decompose_ltl = XARGMATCH("--decompose", arg,
diff --git a/tests/core/ltlsynt2.test b/tests/core/ltlsynt2.test
index 912a76b81..108cb5f94 100755
--- a/tests/core/ltlsynt2.test
+++ b/tests/core/ltlsynt2.test
@@ -82,7 +82,7 @@ EOF
 diff filtered.csv expected
 
 grep -v 0,0 filtered.csv >input.csv
-ltlsynt -F input.csv/-2 --csv=out.csv -q || exit 2
+ltlsynt -F input.csv/-2 --csv=out.csv -q
 $PYTHON test.py
 cat >expected <<EOF
 source,formula,algo,realizable,strat_num_states
@@ -92,3 +92,14 @@ 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
+
+ltlsynt -F input.csv/-2 --csv-without-formula=out.csv -q
+cut out.csv -d, -f1,2 >filtered.csv
+cat >expected <<EOF
+"source","algo"
+"input.csv:2","lar"
+"input.csv:3","lar"
+"input.csv:4","lar"
+"input.csv:5","lar"
+EOF
+diff filtered.csv expected