From 689aa7fdc097749ee6668c8584b63517a0e4ecc2 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 11 Oct 2017 22:19:43 +0200
Subject: [PATCH] translate: add support for -x tls-impl=N

This is long overdue, and we probably want to use tls-impl=1 in
ltlsynt.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh:
Add support for tls-impl=N.
* tests/core/ltl2tgba.test: Test it.
* bin/spot-x.cc, NEWS: Document it.
---
 NEWS                       |  4 ++++
 bin/spot-x.cc              |  7 +++++++
 spot/twaalgos/translate.cc | 31 ++++++++++++++++++++++++++++++-
 spot/twaalgos/translate.hh |  5 +++--
 tests/core/ltl2tgba.test   |  8 ++++++++
 5 files changed, 52 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 96c29bd4d..ebc923202 100644
--- a/NEWS
+++ b/NEWS
@@ -36,6 +36,10 @@ New in spot 2.4.1.dev (not yet released)
 
   - ltldo learned to limit the number of automata it outputs using -n.
 
+  - The new -x tls-impl=N option allows to fine-tune the
+    implication-based simplification rules of ltl2tgba.  See the
+    spot-x man-page for details.
+
   Library:
 
   - Rename three methods of spot::scc_info. New names are clearer. The
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index ad3b0ac36..511ff49d3 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -37,6 +37,13 @@ value) is a shorthand for KEY=1, while !KEY is a shorthand for KEY=0.";
 
 static const argp_option options[] =
   {
+    { nullptr, 0, nullptr, 0, "Temporal logic simplification options:", 0 },
+    { DOC("tls-impl",
+          "Control usage of implication-based rewriting. \
+(0) disables it, (1) enables rules based on syntactic implications, \
+(2) additionally allows automata-based implication checks, (3) enables \
+more rules based on automata-based implication checks.  The default value \
+depends on the --low/--medium/--high settings.") },
     { nullptr, 0, nullptr, 0, "Translation options:", 0 },
     { DOC("comp-susp", "Set to 1 to enable compositional suspension, \
 as described in our SPIN'13 paper (see Bibliography below).  Set to 2, \
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index d5be53d4d..c7de29be9 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -30,7 +30,7 @@ namespace spot
   void translator::setup_opt(const option_map* opt)
   {
     comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
-    relabel_bool_ = -1;
+    relabel_bool_ = tls_impl_ = -1;
 
     if (!opt)
       return;
@@ -43,6 +43,7 @@ namespace spot
         skel_wdba_ = opt->get("skel-wdba", -1);
         skel_simul_ = opt->get("skel-simul", 1);
       }
+    tls_impl_ = opt->get("tls-impl", -1);
   }
 
   void translator::build_simplifier(const bdd_dict_ptr& dict)
@@ -61,6 +62,34 @@ namespace spot
         options.reduce_basics = true;
         options.event_univ = true;
       }
+    // User-supplied fine-tuning?
+    if (tls_impl_ >= 0)
+      switch (tls_impl_)
+        {
+        case 0:
+          options.synt_impl = false;
+          options.containment_checks = false;
+          options.containment_checks_stronger = false;
+          break;
+        case 1:
+          options.synt_impl = true;
+          options.containment_checks = false;
+          options.containment_checks_stronger = false;
+          break;
+        case 2:
+          options.synt_impl = true;
+          options.containment_checks = true;
+          options.containment_checks_stronger = false;
+          break;
+        case 3:
+          options.synt_impl = true;
+          options.containment_checks = true;
+          options.containment_checks_stronger = true;
+          break;
+        default:
+          throw std::runtime_error
+            ("tls-impl should take a value between 0 and 3");
+        }
     simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
   }
 
diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh
index a7bf80e9d..271f72ee3 100644
--- a/spot/twaalgos/translate.hh
+++ b/spot/twaalgos/translate.hh
@@ -74,15 +74,15 @@ namespace spot
     translator(const bdd_dict_ptr& dict, const option_map* opt = nullptr)
       : postprocessor(opt)
     {
-      build_simplifier(dict);
       setup_opt(opt);
+      build_simplifier(dict);
     }
 
     translator(const option_map* opt = nullptr)
       : postprocessor(opt)
     {
-      build_simplifier(make_bdd_dict());
       setup_opt(opt);
+      build_simplifier(make_bdd_dict());
     }
 
     ~translator()
@@ -147,6 +147,7 @@ namespace spot
     int skel_wdba_;
     int skel_simul_;
     int relabel_bool_;
+    int tls_impl_;
   };
   /// @}
 }
diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test
index 6a7131774..81699d253 100755
--- a/tests/core/ltl2tgba.test
+++ b/tests/core/ltl2tgba.test
@@ -270,3 +270,11 @@ test 3 = `ltl2tgba -f 'G(Fa & Fb) U a' --stats=%s`
 # report inconsistent "universal" property.
 ltl2tgba --low 'X(((1) U (p1)) | (((p1) | (F(p0))) U ((0) R ((p2) M (p1)))))'>o
 grep deterministic o
+
+# test tls-impl=N
+f='(Fp0 W p0) & G((Gp0 W Xp0) M !Gp1)'
+ltl2tgba -f "$f" --low -x tls-impl=4 --stats=%s && exit 1
+test 4 = `ltl2tgba -f "$f" --low -x tls-impl=0 --stats=%s`
+test 3 = `ltl2tgba -f "$f" --low -x tls-impl=1 --stats=%s`
+test 2 = `ltl2tgba -f "$f" --low -x tls-impl=2 --stats=%s`
+test 2 = `ltl2tgba -f "$f" --low -x tls-impl=3 --stats=%s`