Implement to_weak_alternating() which weakifies tgbas

* NEWS: mention the modification.
* python/spot/impl.i: makes to_weak_alternating visible from python
* spot/twaalgos/Makefile.am, spot/twaalgos/toweak.cc,
  spot/twaalgos/toweak.hh: Implements to_weak_alternating.
* tests/Makefile.am, tests/python/toweak.py: Test the results of
  to_weak_alternating.

NEWS

@@ -144,6 +144,10 @@ New in spot 2.3.5.dev (not yet released)
     more (this threshold can be changed, see -x relabel-bool=N in
     the spot-x(7) man page).
 
+  - The new function spot::to_weak_alternating() is able to take an
+    input automaton with generalized Büchi/co-Büchi acceptance and
+    convert it to a weak alternating automaton.
+
   Python:
 
   - The 'spot.gen' package exports the functions from libspotgen.

python/spot/impl.i

@@ -152,6 +152,7 @@
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/stutter.hh>
 #include <spot/twaalgos/translate.hh>
+#include <spot/twaalgos/toweak.hh>
 #include <spot/twaalgos/hoa.hh>
 #include <spot/twaalgos/dtwasat.hh>
 #include <spot/twaalgos/relabel.hh>
@@ -582,6 +583,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/sum.hh>
 %include <spot/twaalgos/stutter.hh>
 %include <spot/twaalgos/translate.hh>
+%include <spot/twaalgos/toweak.hh>
 %include <spot/twaalgos/hoa.hh>
 %include <spot/twaalgos/dtwasat.hh>
 %include <spot/twaalgos/relabel.hh>

spot/twaalgos/Makefile.am

@@ -84,6 +84,7 @@ twaalgos_HEADERS = \
   tau03.hh \
   tau03opt.hh \
   totgba.hh \
+  toweak.hh \
   translate.hh \
   word.hh
 
@@ -145,6 +146,7 @@ libtwaalgos_la_SOURCES = \
   tau03.cc \
   tau03opt.cc \
   totgba.cc \
+  toweak.cc \
   translate.cc \
   word.cc
 

spot/twaalgos/toweak.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2017 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// 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/misc/bddlt.hh>
+#include <spot/misc/minato.hh>
+#include <spot/twa/twagraph.hh>
+#include <spot/twaalgos/dualize.hh>
+#include <spot/twaalgos/strength.hh>
+#include <spot/twaalgos/toweak.hh>
+
+#include <queue>
+#include <functional>
+
+namespace spot
+{
+  namespace
+  {
+    struct rc_state
+    {
+      unsigned id;
+      unsigned rank;
+      acc_cond::mark_t mark;
+
+      rc_state(unsigned state_id, unsigned state_rank, acc_cond::mark_t m = 0U)
+       : id(state_id), rank(state_rank), mark(m)
+      {
+      }
+    };
+
+    struct rc_state_hash
+    {
+      size_t
+      operator()(const rc_state& s) const
+      {
+        using std::hash;
+        return ((hash<int>()(s.id)
+                 ^ (hash<int>()(s.rank)))
+                 ^ (hash<int>()(s.mark.id)));
+      }
+    };
+
+    struct rc_state_equal
+    {
+      size_t
+      operator()(const rc_state& left, const rc_state& right) const
+      {
+        return left.id == right.id
+               && left.rank == right.rank
+               && left.mark == right.mark;
+      }
+    };
+
+    class to_weak
+    {
+      private:
+        const const_twa_graph_ptr aut_;
+        const unsigned numsets_;
+        std::unordered_map<rc_state,
+                           unsigned,
+                           rc_state_hash,
+                           rc_state_equal> state_map_;
+        std::vector<bdd> state_to_var_;
+        std::unordered_map<bdd, unsigned, spot::bdd_hash> var_to_state_;
+        bdd all_states_;
+        twa_graph_ptr res_;
+        std::queue<rc_state> todo_;
+        bool less_;
+
+        unsigned new_state(unsigned st, unsigned rank, acc_cond::mark_t mark)
+        {
+          rc_state s(st, rank, mark);
+          auto p = state_map_.emplace(s, 0);
+          if (p.second)
+            {
+              p.first->second = res_->new_state();
+              todo_.emplace(s);
+              int v = aut_->get_dict()->register_anonymous_variables(1, this);
+              bdd var = bdd_ithvar(v);
+              all_states_ &= var;
+              state_to_var_.push_back(var);
+              var_to_state_.emplace(var, p.first->second);
+            }
+          return p.first->second;
+        };
+
+        bdd transition_function(rc_state st)
+        {
+          unsigned id = st.id;
+          unsigned rank = st.rank;
+
+          bdd res = bddfalse;
+
+          bool rank_odd = rank % 2;
+          for (auto& e : aut_->out(id))
+            {
+              // If we are on odd level and the edge is marked with the set we
+              // don't want to see, skip. (delete transition).
+              if (rank_odd && (e.acc & st.mark))
+                continue;
+
+              bdd dest = bddtrue;
+              for (unsigned d : aut_->univ_dests(e.dst))
+                {
+                  bdd levels = bddfalse;
+                  int curr = static_cast<int>(rank);
+                  // We must always be able to go to the previous even rank
+                  int lower = less_ ? ((curr - 1) & ~1) : 0;
+                  for (int i = curr; i >= lower; --i)
+                    {
+                      if (i % 2)
+                        for (unsigned m = 0; m < numsets_; ++m)
+                          levels |= state_to_var_[new_state(d, i, {m})];
+                      else
+                        levels |= state_to_var_[new_state(d, i, 0U)];
+                    }
+                  dest &= levels;
+                }
+              res |= (dest & e.cond);
+            }
+          return res;
+        }
+
+      public:
+        to_weak(const const_twa_graph_ptr& aut, bool less)
+          : aut_(aut),
+            numsets_(aut_->num_sets()),
+            all_states_(bddtrue),
+            res_(make_twa_graph(aut_->get_dict())),
+            less_(less)
+        {
+          res_->copy_ap_of(aut_);
+          res_->set_buchi();
+          res_->prop_weak(true);
+        }
+
+        ~to_weak()
+        {
+          aut_->get_dict()->unregister_all_my_variables(this);
+        }
+
+        twa_graph_ptr run()
+        {
+          std::vector<unsigned> states;
+          for (unsigned d: aut_->univ_dests(aut_->get_init_state_number()))
+            states.push_back(new_state(d, aut_->num_states() * 2, 0U));
+
+          res_->set_univ_init_state(states.begin(), states.end());
+
+          while (!todo_.empty())
+            {
+              rc_state st = todo_.front();
+
+              acc_cond::mark_t mark = 0U;
+              if (st.rank % 2)
+                mark = {0};
+
+              bdd delta = transition_function(st);
+              bdd ap = bdd_exist(bdd_support(delta), all_states_);
+              bdd letters = bdd_exist(delta, all_states_);
+
+              while (letters != bddfalse)
+                {
+                  bdd oneletter = bdd_satoneset(letters, ap, bddtrue);
+                  letters -= oneletter;
+
+                  minato_isop isop(delta & oneletter);
+                  bdd cube;
+
+                  while ((cube = isop.next()) != bddfalse)
+                    {
+                      bdd cond = bdd_exist(cube, all_states_);
+                      bdd dest = bdd_existcomp(cube, all_states_);
+
+                      states.clear();
+                      while (dest != bddtrue)
+                        {
+                          assert(bdd_low(dest) == bddfalse);
+                          bdd v = bdd_ithvar(bdd_var(dest));
+                          auto it = var_to_state_.find(v);
+                          assert(it != var_to_state_.end());
+                          states.push_back(it->second);
+                          dest = bdd_high(dest);
+                        }
+                      res_->new_univ_edge(new_state(st.id, st.rank, st.mark),
+                                          states.begin(), states.end(),
+                                          cond, mark);
+                    }
+                }
+              todo_.pop();
+            }
+          res_->merge_edges();
+          return res_;
+        }
+    };
+  }
+  twa_graph_ptr to_weak_alternating(const_twa_graph_ptr& aut, bool less)
+  {
+    if (is_weak_automaton(aut))
+      return make_twa_graph(aut, twa::prop_set::all());
+    /* The current implementation of is_inherently_weak does not support
+       alternating automata. In case the input automaton is inherently weak,
+       it can be easily transformed to weak without the need to call to_weak
+    */
+    if (aut->acc().is_generalized_buchi())
+      return dualize(to_weak(dualize(aut), less).run());
+    else if (aut->acc().is_generalized_co_buchi())
+      return to_weak(aut, less).run();
+
+    throw std::runtime_error("to_weak_alternating does only support gen. Büchi"
+                             " and gen. co-Büchi automata.");
+  }
+}

spot/twaalgos/toweak.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2017 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <spot/twa/twa.hh>
+
+namespace spot
+{
+  /// \brief Convert an alternating automaton to a weak alternating automaton.
+  ///
+  /// The input automaton must have a generalized co-Büchi or Büchi acceptance
+  /// condition.
+  /// The automaton will be converted into a weak Büchi automaton. If the input
+  /// automaton is already weak, it will simply be copied.
+  ///
+  /// For details about the algorithm used, see the following papers:
+  /** \verbatim
+      @article{kupferman.01.tocl,
+        author      = {Orna Kupferman and Moshe Y. Vardi},
+        title       = {Weak alternating automata are not that weak},
+        journal     = {ACM Transactions on Computational Logic (TOCL)},
+        month       = {July},
+        year        = 2001,
+        pages       = {408--429},
+        volume      = {2},
+        number      = {3},
+        publisher   = {ACM New York, NY, USA}
+      }
+      @article{kupferman.05.tcs,
+        author      = {Orna Kupferman and Moshe Y. Vardi},
+        title       = {From complementation to certification},
+        journal     = {Theoretical Computer Science},
+        month       = {November},
+        year        = 2005,
+        pages       = {83--100},
+        volume      = {345},
+        number      = {1},
+        publisher   = {Elsevier}
+      }
+      \endverbatim */
+  /// Although at the end of the above paper there is a hint at an optimization
+  /// that greatly reduces the number of transition in the resulting automaton,
+  /// but in return makes the run of remove_alternation algorithm way slower.
+  /// Hence, the optimization is disabled by default.
+  ///
+  /// \param aut the automaton to convert to weak
+  /// \param less whether to activate the optimization on the number of
+  /// transitions or not, disabled by default
+  SPOT_API
+  twa_graph_ptr to_weak_alternating(const_twa_graph_ptr& aut,
+                                    bool less = false);
+}

tests/Makefile.am

@@ -371,6 +371,7 @@ TESTS_python = \
   python/trival.py \
   python/tra2tba.py \
   python/twagraph.py \
+  python/toweak.py \
   $(TESTS_ipython)
 endif
 

tests/python/toweak.py

+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2017  Laboratoire de Recherche et Développement
+# de l'Epita
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+import spot
+
+phi1 = """GFb
+X(!b | GF!a)
+!a U X(b | GF!b)
+GFa
+G(a M b)
+(!a | b) & GFb
+(a U Xa) | G(b & Fa)
+GF!b
+(b & GF!b) | (!b & FGb)
+b | (a & XF(b R a)) | (!a & XG(!b U !a))"""
+
+phi1 = phi1.split('\n')
+
+bdddict = spot.make_bdd_dict()
+
+def equivalent(a, phi):
+  negphi = spot.formula.Not(phi)
+  nega = spot.dualize(a)
+  a2 = spot.translate(phi, 'TGBA', 'SBAcc' )
+  nega2 = spot.translate(negphi, 'TGBA', 'SBAcc')
+  ra = spot.remove_alternation(a)
+  ran = spot.remove_alternation(nega)
+  return spot.product(spot.remove_alternation(a), nega2).is_empty()\
+         and spot.product(spot.remove_alternation(nega), a2).is_empty()
+
+def test_phi(phi):
+  a =  spot.translate(phi, 'TGBA', 'SBAcc')
+  a0 = spot.dualize(a)
+
+  res = spot.to_weak_alternating(a0)
+  assert equivalent(res, spot.formula.Not(spot.formula(phi)))
+
+for p in phi1:
+  test_phi(p)