From 3729dfad907142a787dea50e041467942a368cee Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 22 Sep 2022 15:44:18 +0200
Subject: [PATCH] translate: add a branch-post option

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Here.
* NEWS, bin/spot-x.cc: Mention it.
* tests/core/genltl.test: Test it.
---
 NEWS                       |  5 +++++
 bin/spot-x.cc              |  5 +++++
 spot/twaalgos/translate.cc | 13 +++++++++++--
 spot/twaalgos/translate.hh |  3 ++-
 tests/core/genltl.test     |  7 ++++++-
 5 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index 2fbe8d2bf..4268ab81a 100644
--- a/NEWS
+++ b/NEWS
@@ -159,6 +159,11 @@ New in spot 2.10.6.dev  (not yet released)
     further simplification.  This was introduced to help with automata
     produced from formulas output by "genltl --eil-gsi" (see above).
 
+  - spot::postproc has new configuration variable branch-post that
+    can be used to control the use of branching-postponement (diabled
+    by default) or delayed-branching (see above, enabled by default).
+    See the spot-x(7) man page for details.
+
   - spot::parallel_policy is an object that can be passed to some
     algorithm to specify how many threads can be used if Spot has been
     compiled with --enable-pthread.  Currently, only
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index a653fc926..908cbb98a 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -50,6 +50,11 @@ implication checks for formula simplifications.  Defaults to 64.") },
     { nullptr, 0, nullptr, 0, "Translation options:", 0 },
     { DOC("ltl-split", "Set to 0 to disable the translation of automata \
 as product or sum of subformulas.") },
+    { DOC("branch-prop", "Set to 0 to disable branching-postponement \
+(done during translation, may create more states) and delayed-branching \
+(almost similar, but done after translation to only remove states).  \
+Set to 1 to force branching-postponement, and to 2 \
+to force delayed-branching.  By default delayed-branching is used.") },
     { DOC("comp-susp", "Set to 1 to enable compositional suspension, \
 as described in our SPIN'13 paper (see Bibliography below).  Set to 2, \
 to build only the skeleton TGBA without composing it.  Set to 0 (the \
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index a5a84a10b..cd1e2aa63 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -65,6 +65,7 @@ namespace spot
     int tls_max_states = opt->get("tls-max-states", 64);
     tls_max_states_ = std::max(0, tls_max_states);
     exprop_ = opt->get("exprop", -1);
+    branchpost_ = opt->get("branch-post", -1);
   }
 
   void translator::build_simplifier(const bdd_dict_ptr& dict)
@@ -399,10 +400,18 @@ namespace spot
         bool exprop = unambiguous
           || (level_ == postprocessor::High && exprop_ != 0)
           || exprop_ > 0;
+        // branch-post: 1 == force branching postponement
+        //              0 == disable branching post. and delay_branching
+        //              2 == force delay_branching
+        //             -1 == auto (delay_branching)
+        // Some quick experiments suggests that branching postponement
+        // can produce larger automata on non-obligations formulas, and
+        // that even on obligation formulas, delay_branching is faster.
+        bool bpost = branchpost_ == 1;
         aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop,
-                             true, false, false, nullptr, nullptr,
+                             true, bpost, false, nullptr, nullptr,
                              unambiguous);
-        if (delay_branching_here(aut))
+        if (!bpost && branchpost_ != 0 && delay_branching_here(aut))
           {
             aut->purge_unreachable_states();
             aut->merge_edges();
diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh
index 9dc6b12d2..d17c917b2 100644
--- a/spot/twaalgos/translate.hh
+++ b/spot/twaalgos/translate.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018, 2020, 2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -154,6 +154,7 @@ namespace spot
     bool gf_guarantee_ = true;
     bool gf_guarantee_set_ = false;
     bool ltl_split_;
+    int branchpost_ = -1;
     unsigned tls_max_states_ = 0;
     int exprop_;
     const option_map* opt_;
diff --git a/tests/core/genltl.test b/tests/core/genltl.test
index 622950f65..71b1ddf77 100755
--- a/tests/core/genltl.test
+++ b/tests/core/genltl.test
@@ -280,7 +280,8 @@ diff range1.ltl range2.ltl
 # I introduced delay_branching_here(), a cheap function that is called
 # before simplification.  In this case, this is enough to determinize
 # the automaton, simplifying simulation-based reduction greatly.
-genltl --eil-gsi=1..25 | ltlfilt --from-ltlf | ltl2tgba --stats=%s,%e >output
+genltl --eil-gsi=1..25 | ltlfilt --from-ltlf > formulas.ltl
+ltl2tgba -F formulas.ltl --stats=%s,%e >output
 cat >expected <<EOF
 5,9
 7,15
@@ -309,3 +310,7 @@ cat >expected <<EOF
 53,153
 EOF
 diff expected output
+
+# branching postponement should work as well
+ltl2tgba -F formulas.ltl -x branch-post=1 --stats=%s,%e >output
+diff expected output