alternation: implement remove_alternation() for weak alt automata

This mixes the subset construction (for 1-state rejecting SCCs) and
the breakpoint construction (for larger rejecting SCCs).  The
algorithm should probably be rewritten in a cleaner and more efficient
way, but that should do for a first version.  It should be easy to
extend it to support Büchi acceptance (since the breakpoint
construction works for this) when we need it.

* spot/twaalgos/alternation.hh,
spot/twaalgos/alternation.cc (remove_alternation): New function.
* tests/python/alternation.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.

doc/org/tut.org

@@ -75,3 +75,4 @@ real notebooks instead.
   automata.
 - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
 - [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]].
+- [[https://spot.lrde.epita.fr/ipynb/alternation.html][=alternation.ipynb=]] examples of alternating automata.

spot/twaalgos/alternation.cc

@@ -17,9 +17,11 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-#include <spot/twaalgos/alternation.hh>
 #include <algorithm>
+#include <sstream>
+#include <spot/twaalgos/alternation.hh>
 #include <spot/misc/minato.hh>
+#include <spot/twaalgos/strength.hh>
 
 namespace spot
 {
@@ -62,6 +64,8 @@ namespace spot
     return res;
   }
 
+
+
   void outedge_combiner::new_dests(unsigned st, bdd out) const
   {
     minato_isop isop(out);
@@ -85,4 +89,394 @@ namespace spot
       }
   }
 
+
+
+  namespace
+  {
+    class alternation_remover final
+    {
+    protected:
+      const_twa_graph_ptr aut_;
+      scc_info si_;
+      enum scc_class : char { accept, reject_1, reject_more };
+      std::vector<scc_class> class_of_;
+      bool has_reject_more_ = false;
+      unsigned reject_1_count_ = 0;
+      std::set<unsigned> true_states_;
+
+      void classify_each_scc()
+      {
+        auto& g = aut_->get_graph();
+        unsigned sc = si_.scc_count();
+        for (unsigned n = 0; n < sc; ++n)
+          {
+            if (si_.is_trivial(n))
+              continue;
+            if (si_.states_of(n).size() == 1)
+              {
+                if (si_.is_rejecting_scc(n))
+                  {
+                    class_of_[n] = scc_class::reject_1;
+                    ++reject_1_count_;
+                  }
+                else
+                  {
+                    // For size one, scc_info should always be able to
+                    // decide rejecting/accepting.
+                    assert(si_.is_accepting_scc(n));
+
+                    unsigned s = si_.states_of(n).front();
+                    auto& ss = g.state_storage(s);
+                    if (ss.succ == ss.succ_tail)
+                      {
+                        auto& es = g.edge_storage(ss.succ);
+                        if (es.cond == bddtrue && !aut_->is_univ_dest(es.dst))
+                          true_states_.emplace(s);
+                      }
+                  }
+              }
+            else
+              {
+                acc_cond::mark_t m;
+                bool first = true;
+                for (auto src: si_.states_of(n))
+                  for (auto& t: aut_->out(src))
+                    for (unsigned d: aut_->univ_dests(t.dst))
+                      if (si_.scc_of(d) == n)
+                        {
+                          if (first)
+                            {
+                              first = false;
+                              m = t.acc;
+                              if (!aut_->acc().accepting(m))
+                                {
+                                  class_of_[n] = reject_more;
+                                  has_reject_more_ = true;
+                                }
+                              // In case of a universal edge we only
+                              // need to check the first destination
+                              // inside the SCC, because the other
+                              // have the same t.acc.
+                              break;
+                            }
+                          else if (m != t.acc)
+                            {
+                              throw std::runtime_error
+                                ("alternation_removal() only work with weak "
+                                 "alternating automata");
+                            }
+                        }
+              }
+          }
+      }
+
+      std::vector<int> state_to_var_;
+      std::map<int, unsigned> var_to_state_;
+      std::vector<int> scc_to_var_;
+      std::map<int, acc_cond::mark_t> var_to_mark_;
+      bdd all_vars_;
+      bdd all_marks_;
+      bdd all_states_;
+
+      void allocate_state_vars()
+      {
+        auto d = aut_->get_dict();
+        // We need one BDD variable per possible output state.  If
+        // that state is in a reject_more SCC we actually use two
+        // variables for the breakpoint.
+        unsigned ns = aut_->num_states();
+        state_to_var_.reserve(ns);
+        bdd all_states = bddtrue;
+        for (unsigned s = 0; s < ns; ++s)
+          {
+            if (!si_.reachable_state(s))
+              {
+                state_to_var_.push_back(0);
+                continue;
+              }
+            scc_class c = class_of_[si_.scc_of(s)];
+            bool r = c == scc_class::reject_more;
+            int v = d->register_anonymous_variables(1 + r, this);
+            state_to_var_.push_back(v);
+            var_to_state_[v] = s;
+            all_states &= bdd_ithvar(v);
+            if (r)
+              {
+                var_to_state_[v + 1] = ~s;
+                all_states &= bdd_ithvar(v + 1);
+              }
+          }
+        // We also use one BDD variable per reject_1 SCC.  Each of
+        // these variables will represent a bit in mark_t.  We reserve
+        // the first bit for the break_point construction if we have
+        // some reject_more SCC.
+        unsigned nc = si_.scc_count();
+        scc_to_var_.reserve(nc);
+        unsigned mark_pos = has_reject_more_;
+        bdd all_marks = bddtrue;
+        for (unsigned s = 0; s < nc; ++s)
+          {
+            scc_class c = class_of_[s];
+            if (c == scc_class::reject_1)
+              {
+                int v = d->register_anonymous_variables(1, this);
+                scc_to_var_.emplace_back(v);
+                var_to_mark_.emplace(v, acc_cond::mark_t({mark_pos++}));
+                bdd bv = bdd_ithvar(v);
+                all_marks &= bv;
+              }
+            else
+              {
+                scc_to_var_.emplace_back(0);
+              }
+          }
+        all_marks_ = all_marks;
+        all_states_ = all_states;
+        all_vars_ = all_states & all_marks;
+      }
+
+      std::map<unsigned, bdd> state_as_bdd_cache_;
+
+      bdd state_as_bdd(unsigned s)
+      {
+        auto p = state_as_bdd_cache_.emplace(s, bddfalse);
+        if (!p.second)
+          return p.first->second;
+
+        bool marked = (int)s < 0;
+        if (marked)
+          s = ~s;
+
+        unsigned scc_s = si_.scc_of(s);
+        bdd res = bddfalse;
+        for (auto& e: aut_->out(s))
+          {
+            bdd dest = bddtrue;
+            for (unsigned d: aut_->univ_dests(e.dst))
+              {
+                unsigned scc_d = si_.scc_of(d);
+                scc_class c = class_of_[scc_d];
+                bool mark =
+                  marked && (scc_s == scc_d) && (c == scc_class::reject_more);
+                dest &= bdd_ithvar(state_to_var_[d] + mark);
+                if (c == scc_class::reject_1 && scc_s == scc_d)
+                  dest &= bdd_ithvar(scc_to_var_[scc_s]);
+              }
+            res |= e.cond & dest;
+          }
+
+        p.first->second = res;
+        return res;
+      }
+
+      acc_cond::mark_t bdd_to_state(bdd b, std::vector<unsigned>& s)
+      {
+        acc_cond::mark_t m = 0U;
+        while (b != bddtrue)
+          {
+            assert(bdd_low(b) == bddfalse);
+            int v = bdd_var(b);
+            auto it = var_to_state_.find(v);
+            if (it != var_to_state_.end())
+              {
+                s.push_back(it->second);
+              }
+            else
+              {
+                auto it2 = var_to_mark_.find(v);
+                assert(it2 != var_to_mark_.end());
+                m |= it2->second;
+              }
+            b = bdd_high(b);
+          }
+        return m;
+      }
+
+      void simplify_state_set(std::vector<unsigned>& ss)
+      {
+        auto to_remove = true_states_;
+        for (unsigned i: ss)
+          if ((int)i < 0)
+            to_remove.emplace(~i);
+
+        auto i =
+          std::remove_if(ss.begin(), ss.end(),
+                         [&] (unsigned s) {
+                           return to_remove.find(s) != to_remove.end();
+                         });
+        ss.erase(i, ss.end());
+        std::sort(ss.begin(), ss.end());
+      }
+
+      bool has_mark(const std::vector<unsigned>& ss)
+      {
+        for (unsigned i: ss)
+          if ((int)i < 0)
+            return true;
+        return false;
+      }
+
+      void set_mark(std::vector<unsigned>& ss)
+      {
+        for (unsigned& s: ss)
+          if (class_of_[si_.scc_of(s)] == scc_class::reject_more)
+            s = ~s;
+      }
+
+    public:
+      alternation_remover(const const_twa_graph_ptr& aut)
+        : aut_(aut), si_(aut), class_of_(si_.scc_count(), scc_class::accept)
+      {
+      }
+
+      ~alternation_remover()
+      {
+        aut_->get_dict()->unregister_all_my_variables(this);
+      }
+
+
+      twa_graph_ptr run(bool named_states)
+      {
+        // First, we classify each SCC into three possible classes:
+        //
+        // 1) trivial or accepting
+        // 2) rejecting of size 1
+        // 3) rejecting of size >1
+        classify_each_scc();
+
+        // Rejecting SCCs of size 1 can be handled using genralized
+        // Büchi acceptance, using one set per SCC, as in Gastin &
+        // Oddoux CAV'01.  See also Boker & et al. ICALP'10.  Larger
+        // rejecting SCCs require a more expensive procedure known as
+        // the break point construction.  See Miyano & Hayashi (TCS
+        // 1984).  We are currently combining the two constructions.
+        auto res = make_twa_graph(aut_->get_dict());
+        res->copy_ap_of(aut_);
+        // We preserve deterministic-like properties, and
+        // stutter-invariance.
+        res->prop_copy(aut_, {false, false, true, true});
+        res->set_generalized_buchi(has_reject_more_ + reject_1_count_);
+
+        // We for easier computation of outgoing sets, we will
+        // represent states using BDD variables.
+        allocate_state_vars();
+
+        // Conversion between state-sets and states.
+        typedef std::vector<unsigned> state_set;
+        std::vector<state_set> s_to_ss;
+        std::map<state_set, unsigned> ss_to_s;
+        std::stack<unsigned> todo;
+
+        std::vector<std::string>* state_name = nullptr;
+        if (named_states)
+          {
+            state_name = new std::vector<std::string>();
+            res->set_named_prop("state-names", state_name);
+          }
+
+        auto new_state = [&](state_set& ss, bool& need_mark)
+        {
+          simplify_state_set(ss);
+
+          if (has_reject_more_)
+            {
+              need_mark = has_mark(ss);
+              if (!need_mark)
+                set_mark(ss);
+            }
+
+          auto p = ss_to_s.emplace(ss, 0);
+          if (!p.second)
+            return p.first->second;
+          unsigned s = res->new_state();
+          assert(s == s_to_ss.size());
+          p.first->second = s;
+          s_to_ss.emplace_back(ss);
+          todo.emplace(s);
+
+          if (named_states)
+            {
+              std::ostringstream os;
+              bool notfirst = false;
+              for (unsigned s: ss)
+                {
+                  if (notfirst)
+                    os << ',';
+                  else
+                    notfirst = true;
+                  if ((int)s < 0)
+                    {
+                      os << '~';
+                      s = ~s;
+                    }
+                  os << s;
+                }
+              if (!notfirst)
+                os << "{}";
+              state_name->emplace_back(os.str());
+            }
+          return s;
+        };
+
+        const auto& i = aut_->univ_dests(aut_->get_init_state_number());
+        state_set is(i.begin(), i.end());
+        bool has_mark = false;
+        res->set_init_state(new_state(is, has_mark));
+
+        acc_cond::mark_t all_marks = res->acc().all_sets();
+
+        state_set v;
+        while (!todo.empty())
+          {
+            unsigned s = todo.top();
+            todo.pop();
+
+            bdd bs = bddtrue;
+            for (unsigned se: s_to_ss[s])
+              bs &= state_as_bdd(se);
+
+
+            bdd ap = bdd_exist(bdd_support(bs), all_vars_);
+            bdd all_letters = bdd_exist(bs, all_vars_);
+
+            // First loop over all possible valuations atomic properties.
+            while (all_letters != bddfalse)
+              {
+                bdd oneletter = bdd_satoneset(all_letters, ap, bddtrue);
+                all_letters -= oneletter;
+
+                minato_isop isop(bs & oneletter);
+                bdd cube;
+                while ((cube = isop.next()) != bddfalse)
+                  {
+                    bdd cond = bdd_exist(cube, all_vars_);
+                    bdd dest = bdd_existcomp(cube, all_vars_);
+                    v.clear();
+                    acc_cond::mark_t m = bdd_to_state(dest, v);
+                    unsigned d = new_state(v, has_mark);
+                    if (has_mark)
+                      m.set(0);
+                    res->new_edge(s, d, cond, all_marks - m);
+                  }
+              }
+          }
+        res->merge_edges();
+        return res;
+      }
+    };
+
+  }
+
+
+  twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut,
+                                   bool named_states)
+  {
+    if (!aut->is_alternating())
+      // Nothing to do, why was this function called at all?
+      return std::const_pointer_cast<twa_graph>(aut);
+
+    alternation_remover ar(aut);
+    return ar.run(named_states);
+  }
+
 }

spot/twaalgos/alternation.hh

@@ -90,7 +90,14 @@ namespace spot
   }
   /// @}
 
-
+  /// \brief Remove universal edges from an automaton.
-
+  ///
-
+  /// This procedure is restricted to weak alternating automata as
+  /// input, and produces TGBAs as output.  (Generalized Büchi
+  /// acceptance is only used in presence of size-1 rejecting-SCCs.)
+  ///
+  /// \param named_states name each state for easier debugging
+  SPOT_API
+  twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut,
+                                   bool named_states = false);
 }

tests/Makefile.am

@@ -302,6 +302,7 @@ if USE_PYTHON
 TESTS_ipython = \
   python/acc_cond.ipynb \
   python/accparse.ipynb \
+  python/alternation.ipynb \
   python/atva16-fig2a.ipynb \
   python/atva16-fig2b.ipynb \
   python/automata-io.ipynb \