From 66aa6d08838d0cd122df1ef72fd6e83fc20c8ad0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 16 May 2020 19:22:28 +0200
Subject: [PATCH] ltlsynt: make sure the previous Xor optimization actually
 works

* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc: Update the tl_simplification
options after all preferences have been given.
* bin/ltlsynt.cc: Display the size of the translation output.
* tests/core/ltlsynt.test: Add test case.
---
 bin/ltlsynt.cc             |  8 ++++++--
 spot/tl/simplify.cc        |  6 ++++++
 spot/tl/simplify.hh        |  8 ++++++++
 spot/twaalgos/translate.cc | 16 ++++++++++++----
 tests/core/ltlsynt.test    | 16 ++++++++++++++++
 5 files changed, 48 insertions(+), 6 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index aeed8b499..e805a9f3e 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -384,8 +384,12 @@ namespace
       if (want_time)
         trans_time = sw.stop();
       if (verbose)
-        std::cerr << "translating formula done in "
-                  << trans_time << " seconds\n";
+        {
+          std::cerr << "translating formula done in "
+                    << trans_time << " seconds\n";
+          std::cerr << "automaton has " << aut->num_states()
+                    << " states and " << aut->num_sets() << " colors\n";
+        }
 
       spot::twa_graph_ptr dpa = nullptr;
       switch (opt_solver)
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 00fac4c9e..24f94d5eb 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -4100,6 +4100,12 @@ namespace spot
     return simplify_recursively(f, cache_);
   }
 
+  tl_simplifier_options&
+  tl_simplifier::options()
+  {
+    return cache_->options;
+  }
+
   formula
   tl_simplifier::negative_normal_form(formula f, bool negated)
   {
diff --git a/spot/tl/simplify.hh b/spot/tl/simplify.hh
index 34377ff62..7ecde7498 100644
--- a/spot/tl/simplify.hh
+++ b/spot/tl/simplify.hh
@@ -112,6 +112,14 @@ namespace spot
     /// constructor).
     formula simplify(formula f);
 
+#ifndef SWIG
+    /// The simplifier options.
+    ///
+    /// Those should can still be changed before the first formula is
+    /// simplified.
+    tl_simplifier_options& options();
+#endif
+
     /// Build the negative normal form of formula \a f.
     /// All negations of the formula are pushed in front of the
     /// atomic propositions.  Operators <=>, =>, xor are all removed
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index 878bcaa43..5ada74631 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -106,10 +106,6 @@ namespace spot
           throw std::runtime_error
             ("tls-impl should take a value between 0 and 3");
         }
-    if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
-      options.favor_event_univ = true;
-    if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
-      options.keep_top_xor = true;
     simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
   }
 
@@ -419,6 +415,18 @@ namespace spot
 
   twa_graph_ptr translator::run(formula* f)
   {
+    if (simpl_owned_)
+      {
+        // Modify the options according to set_pref() and set_type().
+        // We do it for all translation, but really only the first one
+        // matters.
+        auto& opt = simpl_owned_->options();
+        if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
+          opt.favor_event_univ = true;
+        if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
+          opt.keep_top_xor = true;
+      }
+
     // Do we want to relabel Boolean subformulas?
     // If we have a huge formula such as
     //  (a1 & a2 & ... & an) U (b1 | b2 | ... | bm)
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 805bcd348..1584b8bf5 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -103,6 +103,7 @@ diff out exp
 
 cat >exp <<EOF
 translating formula done in X seconds
+automaton has 3 states and 2 colors
 split inputs and outputs done in X seconds
 automaton has 9 states
 determinization done
@@ -117,6 +118,21 @@ ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
 diff outx exp
 
+cat >exp <<EOF
+translating formula done in X seconds
+automaton has 16 states and 2 colors
+split inputs and outputs done in X seconds
+automaton has 47 states
+LAR construction done in X seconds
+DPA has 47 states, 4 colors
+parity game built in X seconds
+parity game solved in X seconds
+EOF
+ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \
+        --verbose --realizability --algo=lar 2> out
+sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
+diff outx exp
+
 for r in '' '--real'; do
     opts="$r --ins=a --outs=b -f"
     ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || :