From 5d80cc556ca17fafc31e03739e23a4bcf1bb44bb Mon Sep 17 00:00:00 2001
From: Maximilien Colange <colange@lrde.epita.fr>
Date: Tue, 2 Jan 2018 09:24:31 +0100
Subject: [PATCH] Add a verbose option to ltlsynt

* bin/ltlsynt.cc: implement it
---
 bin/ltlsynt.cc | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index a7bd73ae0..f257c1a4c 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -53,7 +53,8 @@ enum
   OPT_OUTPUT,
   OPT_PRINT,
   OPT_PRINT_AIGER,
-  OPT_REAL
+  OPT_REAL,
+  OPT_VERBOSE
 };
 
 static const argp_option options[] =
@@ -80,6 +81,8 @@ static const argp_option options[] =
       "realizability only, do not compute a winning strategy", 0},
     { "aiger", OPT_PRINT_AIGER, nullptr, 0,
       "prints the winning strategy as an AIGER circuit", 0},
+    { "verbose", OPT_VERBOSE, nullptr, 0,
+      "verbose mode", -1 },
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
     { nullptr, 0, nullptr, 0, nullptr, 0 },
@@ -129,6 +132,7 @@ static solver const solver_types[] =
 ARGMATCH_VERIFY(solver_args, solver_types);
 
 static solver opt_solver = REC;
+static bool verbose = false;
 
 namespace
 {
@@ -276,7 +280,6 @@ namespace
     return aut;
   }
 
-
   class ltl_processor final : public job_processor
   {
   private:
@@ -300,6 +303,8 @@ namespace
       timer.start();
 
       auto aut = trans_.run(&f);
+      if (verbose)
+        std::cerr << "translating formula done" << std::endl;
       bdd all_inputs = bddtrue;
       bdd all_outputs = bddtrue;
       for (unsigned i = 0; i < input_aps_.size(); ++i)
@@ -318,10 +323,17 @@ namespace
           unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
           all_outputs &= bdd_ithvar(v);
         }
+
       auto split = split_automaton(aut, all_inputs);
+      if (verbose)
+        std::cerr << "split inputs and outputs done" << std::endl;
       auto dpa = to_dpa(split);
+      if (verbose)
+        std::cerr << "determinization done" << std::endl;
       auto owner = make_alternating_owner(dpa);
       auto pg = spot::parity_game(dpa, owner);
+      if (verbose)
+        std::cerr << "parity game built" << std::endl;
       timer.stop();
 
       if (opt_print_pg)
@@ -425,6 +437,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_PRINT_AIGER:
       opt_print_aiger = true;
       break;
+    case OPT_VERBOSE:
+      verbose = true;
+      break;
     }
   return 0;
 }