From 3fd5f38248dbd8f26cb09de78e700d7e271c25ee Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Sat, 23 May 2020 14:13:33 +0200
Subject: [PATCH] ltlsynt: Add -x option for translation

* bin/ltlsynt.cc: ltlsynt can use extra options for translator.
---
 bin/ltlsynt.cc | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 0c1ce9aae..f672d9f3f 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -99,6 +99,8 @@ static const argp_option options[] =
       "not output)", 0 },
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
+    { "extra-options", 'x', "OPTS", 0,
+        "fine-tuning options (see spot-x (7))", 0 },
     { nullptr, 0, nullptr, 0, nullptr, 0 },
   };
 
@@ -125,6 +127,7 @@ static const char* opt_csv = nullptr;
 static bool opt_print_pg = false;
 static bool opt_real = false;
 static bool opt_print_aiger = false;
+static spot::option_map extra_options;
 
 static double trans_time = 0.0;
 static double split_time = 0.0;
@@ -643,6 +646,13 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_VERBOSE:
       verbose = true;
       break;
+    case 'x':
+      {
+        const char* opt = extra_options.parse_options(arg);
+        if (opt)
+          error(2, 0, "failed to parse --options near '%s'", opt);
+      }
+      break;
     }
   END_EXCEPTION_PROTECT;
   return 0;
@@ -661,8 +671,11 @@ main(int argc, char **argv)
       // Setup the dictionary now, so that BuDDy's initialization is
       // not measured in our timings.
       spot::bdd_dict_ptr dict = spot::make_bdd_dict();
-      spot::translator trans(dict);
+      spot::translator trans(dict, &extra_options);
       ltl_processor processor(trans, input_aps, output_aps);
+
+      // Diagnose unused -x options
+      extra_options.report_unused_options();
       return processor.run();
     });
 }