translate_aa: fix construction for transition based acc

* spot/twaalgos/translate_aa.cc: Here.

spot/tl/sonf.cc

@@ -131,7 +131,7 @@ namespace spot
           {
             // recurse into rhs first (_ []-> rhs)
             formula rhs =
-              f[1].map(extractor, extracted, extractor, false, false);
+              extractor(f[1], extracted, extractor, false, false);
             f = formula::binop(kind, f[0], rhs);
 
             formula ap = formula::ap(new_ap_name());

spot/twaalgos/alternation.cc

@@ -39,6 +39,7 @@ namespace spot
   }
 
   bdd outedge_combiner::operator()(unsigned st, const std::vector<unsigned>& dst_filter,
+                                   const std::vector<std::tuple<unsigned, bdd, unsigned>>& edge_filter,
                                    bool remove_original_edges)
   {
     const auto& dict = aut_->get_dict();
@@ -49,7 +50,23 @@ namespace spot
         for (auto& e: aut_->out(d1))
           {
             // handle edge filtering
-            if (!dst_filter.empty())
+            if (!edge_filter.empty())
+              {
+                // Trying all univ dests for e, find if there was at least one
+                // compatible edge that was accepting in the original TFA
+                auto univ_dests = aut_->univ_dests(e.dst);
+                if (std::all_of(univ_dests.begin(), univ_dests.end(),
+                                [&](unsigned dst) {
+                                  for (const auto& acc_e : edge_filter)
+                                    if(std::get<0>(acc_e) == e.src
+                                       && std::get<2>(acc_e) == dst
+                                       && bdd_implies(e.cond, std::get<1>(acc_e)))
+                                      return false; // false because we don't want to skip it
+                                  return true;
+                                }))
+                  continue;
+              }
+            else if (!dst_filter.empty()) // same for state-based acc
               {
                 // if any edge destination is an accepting state in the SERE
                 // automaton, handle the edge, otherwise skip it

spot/twaalgos/alternation.hh

@@ -54,6 +54,7 @@ namespace spot
     outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u);
     ~outedge_combiner();
     bdd operator()(unsigned st, const std::vector<unsigned>& dst_filter = std::vector<unsigned>(),
+                   const std::vector<std::tuple<unsigned, bdd, unsigned>>& edge_filter = std::vector<std::tuple<unsigned, bdd, unsigned>>(),
                    bool remove_original_edges = false);
     void new_dests(unsigned st, bdd out) const;
   };

spot/twaalgos/translate_aa.cc

@@ -26,6 +26,7 @@
 #include <spot/twaalgos/translate_aa.hh>
 #include <spot/tl/derive.hh>
 #include <spot/tl/expansions.hh>
+#include <spot/tl/expansions2.hh>
 #include <spot/tl/nenoform.hh>
 
 #include <iostream>
@@ -34,6 +35,24 @@ namespace spot
 {
   namespace
   {
+    twa_graph_ptr sere_aa_translate(formula f, const bdd_dict_ptr& dict)
+    {
+      // old bdd method
+      if (sere_aa_translation_options() == 0)
+        return sere_to_tgba(f, dict, true);
+
+      // derivation
+      if (sere_aa_translation_options() == 1)
+        return derive_finite_automaton_with_first(f, dict);
+
+      // linear form
+      if (sere_aa_translation_options() == 2)
+        return expand_finite_automaton(f, dict, exp_opts::expand_opt::None);
+
+      // linear form - trans-based
+      return expand_finite_automaton2(f, dict, exp_opts::expand_opt::None);
+    }
+
     struct ltl_to_aa_builder
     {
       ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink)
@@ -78,10 +97,11 @@ namespace spot
 
       unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut,
                                     std::map<unsigned, unsigned>& old_to_new,
-                                    std::vector<unsigned>* acc_states = nullptr,
+                                    std::vector<unsigned>* acc_edges = nullptr,
                                     bool use_accepting_sink = true)
       {
         unsigned ns = sere_aut->num_states();
+        bool trans_based = sere_aut->prop_state_acc().is_false();
 
         // TODO: create all new states at once, keeping an initial offset (the
         //       number of states already present in aut_)
@@ -92,8 +112,6 @@ namespace spot
           {
             unsigned new_st = aut_->new_state();
             p.first->second = new_st;
-            if (acc_states != nullptr && sere_aut->state_is_accepting(st))
-              acc_states->push_back(new_st);
           }
           return p.first->second;
         };
@@ -103,10 +121,22 @@ namespace spot
             unsigned new_st = register_state(st);
             for (const auto& e : sere_aut->out(st))
               {
-                if (use_accepting_sink && sere_aut->state_is_accepting(e.dst))
-                  aut_->new_edge(new_st, accepting_sink_, e.cond);
-                else
-                  aut_->new_edge(new_st, register_state(e.dst), e.cond);
+                bool edge_is_acc = ((trans_based && e.acc)
+                                    || (!trans_based && sere_aut->state_is_accepting(e.dst)));
+
+                if (edge_is_acc)
+                  {
+                    // point to accepting sink instead of original dst if asked
+                    if (use_accepting_sink)
+                      aut_->new_edge(new_st, accepting_sink_, e.cond);
+                    else
+                      {
+                        unsigned new_e = aut_->new_edge(new_st, register_state(e.dst), e.cond);
+                        // remember if old edges were accepting
+                        if (acc_edges != nullptr)
+                          acc_edges->push_back(new_e);
+                      }
+                  }
               }
           }
 
@@ -289,43 +319,22 @@ namespace spot
           {
             unsigned rhs_init = recurse(f[1]);
             const auto& dict = aut_->get_dict();
-            twa_graph_ptr sere_aut;
-            if (sere_aa_translation_options() == 0)
-              {
-                // old bdd method
-                sere_aut = sere_to_tgba(f[0], dict, true);
-              }
-            else if (sere_aa_translation_options() == 1)
-              {
-                // derivation
-                sere_aut = derive_finite_automaton_with_first(f[0], dict);
-              }
-            else
-              {
-                // linear form
-                sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None);
-              }
+            twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
 
             // TODO: this should be a std::vector<bool> !
-            std::vector<unsigned> acc_states;
-            std::map<unsigned, unsigned> old_to_new;
-            copy_sere_aut_to_res(sere_aut, old_to_new, &acc_states, false);
-
             std::vector<unsigned> acc_edges;
+            std::map<unsigned, unsigned> old_to_new;
+            copy_sere_aut_to_res(sere_aut, old_to_new, &acc_edges, false);
+
+            // mark all edges from NFA in new automaton
             unsigned ns = sere_aut->num_states();
             for (unsigned st = 0; st < ns; ++st)
               {
                 auto it = old_to_new.find(st);
                 assert(it != old_to_new.end());
                 unsigned new_st = it->second;
-
                 for (auto& e : aut_->out(new_st))
-                  {
-                    e.acc = acc_cond::mark_t{0};
-                    if (std::find(acc_states.begin(), acc_states.end(), e.dst)
-                        != acc_states.end())
-                      acc_edges.push_back(aut_->edge_number(e));
-                  }
+                  e.acc = acc_cond::mark_t{0};
               }
 
             for (unsigned i : acc_edges)
@@ -345,29 +354,27 @@ namespace spot
           {
             unsigned rhs_init = recurse(f[1]);
             const auto& dict = aut_->get_dict();
-            twa_graph_ptr sere_aut;
-            if (sere_aa_translation_options() == 0)
-              {
-                // old bdd method
-                sere_aut = sere_to_tgba(f[0], dict, true);
-              }
-            else if (sere_aa_translation_options() == 1)
-              {
-                // derivation
-                sere_aut = derive_finite_automaton_with_first(f[0], dict);
-              }
-            else
-              {
-                // linear form
-                sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None);
-              }
+            twa_graph_ptr sere_aut = sere_aa_translate(f[0], dict);
+            bool trans_based = sere_aut->prop_state_acc().is_false();
 
             // DFA recognizes the empty language, so {0} []-> rhs is always true
             unsigned ns = sere_aut->num_states();
-            bool has_accepting_state = false;
-            for (unsigned st = 0; st < ns && !has_accepting_state; ++st)
-              has_accepting_state = sere_aut->state_is_accepting(st);
-            if (!has_accepting_state)
+            bool accepts = false;
+            for (unsigned st = 0; st < ns && !accepts; ++st)
+              {
+                if (trans_based)
+                  {
+                    for (const auto& e : sere_aut->out(st))
+                      if (e.acc)
+                        {
+                          accepts = true;
+                          break;
+                        }
+                  }
+                else
+                  accepts = sere_aut->state_is_accepting(st);
+              }
+            if (!accepts)
               return accepting_sink_;
 
             std::map<unsigned, unsigned> old_to_new;
@@ -378,6 +385,8 @@ namespace spot
             std::vector<unsigned> univ_dest;
             // TODO: this should be a std::vector<bool> !
             std::vector<unsigned> acc_states;
+            // any edge compatible with that should be considered accepting
+            std::vector<std::tuple<unsigned, bdd, unsigned>> acc_edges;
 
             // registers a state in various maps and returns the index of the
             // anonymous bdd var representing that state
@@ -392,7 +401,7 @@ namespace spot
                 old_to_new.emplace(st, new_st);
                 var_to_state.emplace(v, new_st);
 
-                if (sere_aut->state_is_accepting(st))
+                if (!trans_based && sere_aut->state_is_accepting(st))
                   acc_states.push_back(new_st);
 
                 vars &= bdd_ithvar(v);
@@ -401,6 +410,15 @@ namespace spot
               return p.first->second;
             };
 
+            // FIXME: this code handles dualization, but we cannot dualize if
+            // this situation arises:
+            //
+            // State: 0
+            // [a] 1
+            // [a] 2 {0}
+            //
+            // The quick fix is to simply determinize the NFA before dualizing,
+            // which removes any existentialism.
             aut_->copy_ap_of(sere_aut);
             for (unsigned st = 0; st < ns; ++st)
               {
@@ -411,6 +429,15 @@ namespace spot
                   {
                     int st_bddi = register_state(e.dst);
                     sig |= e.cond & bdd_ithvar(st_bddi);
+
+                    // register edge that was accepting in TFA
+                    if (trans_based && e.acc)
+                      {
+                        unsigned new_src = old_to_new[e.src];
+                        unsigned new_dst = old_to_new[e.dst];
+
+                        acc_edges.push_back({new_src, e.cond, new_dst});
+                      }
                   }
 
                 for (bdd cond : minterms_of(bddtrue, aps))
@@ -446,7 +473,7 @@ namespace spot
                 unsigned new_st = it->second;
 
                 bdd comb = bddtrue;
-                comb &= oe_(new_st, acc_states, true);
+                comb &= oe_(new_st, acc_states, acc_edges, true);
                 if (comb != bddtrue)
                   {
                     comb &= oe_(rhs_init);
@@ -529,14 +556,16 @@ namespace spot
           pref = 0;
         else if (!strcasecmp(version, "derive"))
           pref = 1;
-        else if (!strcasecmp(version, "expansion"))
+        else if (!strcasecmp(version, "lf"))
           pref = 2;
+        else if (!strcasecmp(version, "lft"))
+          pref = 3;
         else
           {
             const char* err = ("sere_aa_translation_options(): argument"
-                              " should be one of {bdd,derive,expansion}");
+                              " should be one of {bdd,derive,lf,lft}");
             if (env)
-              err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,expansion}";
+              err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,lf,lft}";
             throw std::runtime_error(err);
           }
       }