implement dualize to complement automatons

* NEWS: Mention the implementation
* python/spot/impl.i: Add dualize() to python interface.
* spot/twaalgos/Makefile.am: Add dualize.cc,hh to the build
* spot/twaalgos/dualize.cc: Implement dualize() that takes an automaton
  and returns its dual
* spot/twaalgos/dualize.hh: Implement dualize()
* tests/Makefile.am: Add dualize tests to the test suite
* tests/python/dualize.py: Test cases for dualize

NEWS

@@ -21,6 +21,8 @@ New in spot 2.3.2.dev (not yet released)
   - twa objects have a new property: prop_complete().  This obviously
     acts as a cache for the is_complete() function.
 
+  - spot::dualize() implements the dual of any alternating automaton.
+
   Bug fixes:
 
   - In "lenient" mode the parser would fail to recover from

python/spot/impl.i

@@ -120,6 +120,7 @@
 #include <spot/twaalgos/cleanacc.hh>
 #include <spot/twaalgos/degen.hh>
 #include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/dualize.hh>
 #include <spot/twaalgos/copy.hh>
 #include <spot/twaalgos/complete.hh>
 #include <spot/twaalgos/complement.hh>
@@ -541,6 +542,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/ltl2tgba_fm.hh>
 %include <spot/twaalgos/compsusp.hh>
 %include <spot/twaalgos/determinize.hh>
+%include <spot/twaalgos/dualize.hh>
 %include <spot/twaalgos/langmap.hh>
 %include <spot/twaalgos/magic.hh>
 %include <spot/twaalgos/minimize.hh>

spot/twaalgos/Makefile.am

@@ -43,6 +43,7 @@ twaalgos_HEADERS = \
   dot.hh \
   dtbasat.hh \
   dtwasat.hh \
+  dualize.hh \
   emptiness.hh \
   emptiness_stats.hh \
   gv04.hh \
@@ -102,6 +103,7 @@ libtwaalgos_la_SOURCES = \
   dot.cc \
   dtbasat.cc \
   dtwasat.cc \
+  dualize.cc \
   emptiness.cc \
   gv04.cc \
   hoa.cc \

spot/twaalgos/dualize.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/minato.hh>
+#include <spot/twa/twagraph.hh>
+#include <spot/twaalgos/alternation.hh>
+#include <spot/twaalgos/cleanacc.hh>
+#include <spot/twaalgos/complete.hh>
+#include <spot/twaalgos/dualize.hh>
+#include <spot/twaalgos/isdet.hh>
+
+namespace spot
+{
+  namespace
+  {
+    class dualizer final
+    {
+    private:
+      // Input automaton
+      const const_twa_graph_ptr aut_;
+      // State id to bdd variable association
+      // [id] == bddtrue means the state will be accepting everything
+      // (true state) in the dual automaton.
+      // [id] == bddfalse means the state will be rejecting everything
+      // (sink) in the dual automaton, which can lead to the removal of
+      // the transitions going into that state and therefore to the removal
+      // of the state when applying purge_unreachable_states().
+      // When [id] != bddtrue/bddfalse, the value correspond to the state
+      // bdd variable.
+      std::vector<bdd> state_to_var_;
+      // bdd variable to state id association
+      std::map<int, unsigned> var_to_state_;
+      // Acceptance mark to bdd variable association
+      std::vector<int> mark_to_var_;
+      // bdd variable to acceptance mark association
+      std::map<int, unsigned> var_to_mark_;
+      // bdd representing all the state variables
+      bdd all_states_;
+      // bdd representing all the marks variables
+      bdd all_marks_;
+      // bdd representing states & marks variables
+      bdd all_vars_;
+      // Id of the true state sink. -1U if none.
+      unsigned true_state_;
+      // In case the acceptance condition is never unsatisfied, but the
+      // automaton is not complete, we do transform the acceptance condition
+      // to Büchi, and need to mark all the existing transitions with the
+      // proper mark, that will be stored in acc_. 0U if not used.
+      acc_cond::mark_t acc_;
+      // Whether aut_ has a state accepting all.
+      bool has_sink;
+
+      // Any sink state in the input automaton will become a true state in the
+      // output. Knowing those allows us to simplify some universal transitions.
+      // There could be more than one sink state in the input automaton, and in
+      // this case they will be squashed into a single true state in the output
+      // automaton.
+      void find_sink_states(acc_cond::mark_t& second)
+      {
+        // Loop over the states and search a state that has no outgoing
+        // transitions, or only self-loops labeled by the same non-accepting
+        // mark. A similar test is done in complete_here().
+        unsigned n = aut_->num_states();
+        for (unsigned i = 0; i < n; ++i)
+          {
+            bool sinkable = true;
+            bool first = true;
+            acc_cond::mark_t commonacc = second;
+            for (auto& t: aut_->out(i))
+              {
+                if (t.dst != i)
+                  {
+                    sinkable = false;
+                    break;
+                  }
+                if (first)
+                  {
+                    commonacc = t.acc;
+                    first = false;
+                  }
+                else if (t.acc != commonacc)
+                  {
+                    sinkable = false;
+                    break;
+                  }
+              }
+            if (sinkable && !aut_->acc().accepting(commonacc))
+              {
+                second = commonacc;
+                state_to_var_[i] = bddtrue;
+                true_state_ = i;
+                has_sink = true;
+              }
+          }
+      }
+      // Any true state in the input automaton will become a sink state in the
+      // output. Knowing those allow us to simplify some universal transitions.
+      // There could be more than one true state in the input automaton. All
+      // true states from the input automaton will be removed in the output
+      // and the transitions leading to those states will be removed as well.
+      void find_true_states()
+      {
+        // Loop over the states and search a state that has a self-loop on
+        // any letter (bddtrue), with an accepting mark.
+        unsigned n = aut_->num_states();
+        for (unsigned i = 0; i < n; ++i)
+          {
+            bool acc_all = false;
+            for (auto& t: aut_->out(i))
+              {
+                if (t.dst == i && t.cond == bddtrue
+                               && aut_->acc().accepting(t.acc))
+                  {
+                    acc_all = true;
+                    break;
+                  }
+              }
+            if (acc_all)
+              {
+                state_to_var_[i] = bddfalse;
+                has_sink = true;
+              }
+          }
+      }
+
+      void copy_edges(const twa_graph_ptr &res)
+      {
+        std::vector<unsigned> st;
+        unsigned n = aut_->num_states();
+        for (unsigned i = 0; i < n; ++i)
+          {
+            bdd delta = dualized_transition_function(i);
+            bdd ap = bdd_exist(bdd_support(delta), all_vars_);
+            bdd letters = bdd_exist(delta, all_vars_);
+
+            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_vars_);
+                    bdd dest = bdd_existcomp(cube, all_vars_);
+
+                    st.clear();
+                    acc_cond::mark_t m = bdd_to_state(dest, st);
+                    if  (st.empty())
+                      {
+                        st.push_back(true_state_);
+                        if (aut_->prop_state_acc())
+                          m = aut_->state_acc_sets(i);
+                      }
+                    res->new_univ_edge(i, st.begin(), st.end(), cond, m);
+                  }
+              }
+          }
+      }
+
+      // Handles the dualization of a universal initial transition.
+      // In theory the transition would be split into several existential 
+      // initial transitions, but since spot does not allow multiple initial 
+      // states, we rather use a trick: We add a new initial state, and then
+      // copy all exiting transitions from each of the state of the universal
+      // initial transition.
+      void univ_init(const twa_graph_ptr& res)
+      {
+        bdd comb = bddfalse;
+        outedge_combiner oe(res);
+        for (unsigned c : aut_->univ_dests(aut_->get_init_state_number()))
+          comb |= oe(c);
+
+        auto s = res->new_state();
+        res->set_init_state(s);
+        oe.new_dests(s, comb);
+      }
+
+      // Allocates the states and marks as variables into the bdd dictionary.
+      // Also adds the corresponding mapping, and sets all_states_, all_marks_,
+      // and all_vars_ to hold those variables as bdds.
+      void allocate_dict_vars(const twa_graph_ptr& res)
+      {
+        auto dict = aut_->get_dict();
+
+        unsigned numstates = aut_->num_states();
+        all_states_ = bddtrue;
+        for (unsigned i = 0; i < numstates; ++i)
+          {
+            int v = dict->register_anonymous_variables(1, this);
+            if (state_to_var_[i] != bddtrue)
+              state_to_var_[i] = bdd_ithvar(v);
+            var_to_state_[v] = i;
+            all_states_ &= bdd_ithvar(v);
+          }
+
+        unsigned numsets = res->num_sets();
+        all_marks_ = bddtrue;
+        for (unsigned i = 0; i < numsets; ++i)
+          {
+            int v = dict->register_anonymous_variables(1, this);
+            mark_to_var_.push_back(v);
+            var_to_mark_.emplace(v, i);
+            all_marks_ &= bdd_ithvar(v);
+          }
+        all_vars_ = all_states_ & all_marks_;
+      }
+
+      // Returns the dualized transition function of any input state as a bdd.
+      bdd dualized_transition_function(unsigned state_id)
+      {
+        if (state_to_var_[state_id] == bddtrue)
+          return bddfalse;
+
+        bdd res = bddtrue;
+        for (auto& e : aut_->out(state_id))
+          {
+            bdd dest = bddfalse;
+            for (unsigned d : aut_->univ_dests(e))
+              dest |= state_to_var_[d];
+
+            bdd mark_bdd = bddtrue;
+            acc_cond::mark_t m = acc_ ? acc_ : e.acc;
+            for (unsigned s: m.sets())
+              mark_bdd &= bdd_ithvar(mark_to_var_[s]);
+
+            res &= bdd_imp(e.cond, mark_bdd & dest);
+          }
+        return res;
+      }
+
+      // Given the bdd representation b of a transition, adds destination states
+      // to s, and returns the marks on the transition. s being empty means the 
+      // transition goes toward a "forever true" state. s with size one
+      // represents an existential transition, while size over one represents 
+      // a universal transition.
+      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
+              m.set(var_to_mark_[v]);
+
+            b = bdd_high(b);
+          }
+        return m;
+      }
+
+    public:
+      dualizer(const const_twa_graph_ptr& aut)
+        : aut_(aut),
+          state_to_var_(aut_->num_states(), bddfalse),
+          true_state_(-1U),
+          acc_(0U),
+          has_sink(false)
+      {
+      }
+
+      ~dualizer()
+      {
+        aut_->get_dict()->unregister_all_my_variables(this);
+      }
+
+      twa_graph_ptr run()
+      {
+        bool cmpl = is_complete(aut_);
+        auto um = aut_->acc().unsat_mark();
+
+        auto res = make_twa_graph(aut_->get_dict());
+        res->copy_ap_of(aut_);
+
+        if (!um.first && cmpl)
+          {
+            //Shortcut if dual is false
+            res->new_states(1);
+            res->new_edge(0, 0, bddtrue, 0U);
+            res->set_init_state(0);
+            res->set_acceptance(0, acc_cond::acc_code::f());
+
+            res->prop_terminal(true);
+            res->prop_complete(true);
+            res->prop_universal(true);
+            return res;
+          }
+        if (is_deterministic(aut_))
+          {
+            res = cleanup_acceptance_here(spot::complete(aut_));
+            res->set_acceptance(res->num_sets(),
+                                res->get_acceptance().complement());
+            // Complementing the acceptance is likely to break the terminal
+            // property, but not weakness.  We make a useless call to
+            // prop_keep() just so we remember to update it in the future if a
+            // new argument is added.
+            res->prop_keep({true, true, true, true, true, true});
+            res->prop_terminal(trival::maybe());
+            return res;
+          }
+
+        const_twa_graph_ptr autptr;
+        res->new_states(aut_->num_states());
+        if (!cmpl)
+          {
+            if (!um.first)
+              {
+                acc_ = res->set_buchi();
+                autptr = res;
+              }
+            else
+              {
+                find_sink_states(um.second);
+                autptr = aut_;
+              }
+            if (true_state_ == -1U)
+              true_state_ = res->new_state();
+          }
+        // This case does not cover cmpl && !um.first
+        // Due to previous test shortcutting automatons that accept all words.
+        else
+          {
+            assert(um.first);
+            find_sink_states(um.second);
+            autptr = aut_;
+          }
+        if (true_state_ != -1U)
+          res->new_edge(true_state_, true_state_, bddtrue, um.second);
+
+        res->set_acceptance(autptr->num_sets(),
+                            autptr->get_acceptance().complement());
+        allocate_dict_vars(res);
+        find_true_states();
+
+        copy_edges(res);
+
+        unsigned init_state = aut_->get_init_state_number();
+        if (aut_->is_univ_dest(init_state))
+          univ_init(res);
+        else
+          res->set_init_state(init_state);
+
+        res->merge_edges();
+        res->purge_unreachable_states();
+
+        res->prop_copy(aut_, {true, true, false, false, false, true});
+        res->prop_terminal(trival::maybe());
+        if (!has_sink)
+          res->prop_complete(true);
+
+        cleanup_acceptance_here(res);
+        return res;
+      }
+    };
+  }
+
+  twa_graph_ptr dualize(const const_twa_graph_ptr& aut)
+  {
+    dualizer du(aut);
+    return du.run();
+  }
+}

spot/twaalgos/dualize.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/misc/common.hh>
+#include <spot/twa/fwd.hh>
+
+namespace spot
+{
+  /// \brief Complement an automaton by dualizing it.
+  ///
+  /// Given an automaton \a aut of any type, produces the dual as output. The
+  /// automaton will be completed if it isn't already. If it is deterministic
+  /// and complete, complementing the automaton can be done by just
+  /// complementing the acceptance condition.
+  ///
+  /// In particular, this implies that an input that use generalized Büchi will
+  /// be output as generalized co-Büchi.
+  ///
+  /// Functions like to_generalized_buchi() or remove_fin() are frequently
+  /// called on existential automatons after dualize() to obtain an easier
+  /// acceptance condition, but maybe at the cost of losing determinism.
+  ///
+  /// If the input automaton is deterministic, the output will be deterministic.
+  /// If the input automaton is existential, the output will be universal.
+  /// If the input automaton is universal, the output will be existential.
+  /// Finally, if the input automaton is alternating, the result is alternating.
+  /// More can be found on page 22 (Definition 1.6) of:
+  /** \verbatim
+      @mastersthesis{loding.98.methodsfor
+        author = {Christof Löding}
+        title  = {Methods for the Transformation of ω-Automata: Complexity
+                 and Connection to Second Order Logic}
+        school = {Institute of Computer Science and Applied Mathematics
+                  Christian-Albrechts-University of Kiel}
+        year   = {1998}
+      }
+      \endverbatim */
+  SPOT_API twa_graph_ptr
+  dualize(const const_twa_graph_ptr& aut);
+}

tests/Makefile.am

@@ -332,6 +332,7 @@ TESTS_python = \
   python/bugdet.py \
   python/declenv.py \
   python/decompose_scc.py \
+  python/dualize.py \
   python/implies.py \
   python/interdep.py \
   python/ltl2tgba.test \

tests/python/dualize.py

+#!/usr/bin/python3
+# -*- 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
+import buddy
+
+match_strings = [('is_buchi', 'is_co_buchi'),\
+                 ('is_generalized_buchi', 'is_generalized_co_buchi'),\
+                 ('is_all', 'is_none'),\
+                 ('is_all', 'is_all'),
+                 ('is_buchi', 'is_all')]
+
+def dualtype(aut, dual):
+  if dual.acc().is_none(): return True
+  return (not spot.is_deterministic(aut) or spot.is_deterministic(dual))\
+         and (spot.is_universal(dual) or not aut.is_existential())\
+         and (dual.is_existential() or not spot.is_universal(aut))
+
+def produce_phi(rg, n):
+  phi = []
+  while len(phi) < n:
+    phi.append(rg.next())
+  return phi
+
+def produce_automaton(phi):
+  aut = []
+  for f in phi:
+    aut.append(spot.translate(f))
+  return aut
+
+def test_aut(aut, d = None):
+  if d is None:
+    d = spot.dualize(aut)
+  aa = aut.acc()
+  da = d.acc()
+
+  complete = spot.is_complete(aut)
+  univ = aut.is_univ_dest(aut.get_init_state_number())
+  an = aut.num_states()
+  dn = d.num_states()
+
+  if not dualtype(aut, d):
+    return (False, 'Incorrect transition mode resulting of dual')
+  for p in match_strings:
+    if ((getattr(aa, p[0])() and getattr(da, p[1])())\
+      or (getattr(aa, p[1])() and getattr(da, p[0])())):
+      return (True, '')
+  return (False, 'Incorrect acceptance type dual')
+
+def test_assert(a, d=None):
+  t = test_aut(a, d)
+  if not t[0]:
+    print (t[1])
+    print (a.to_str('hoa'))
+    print (spot.dualize(a).to_str('hoa'))
+    assert False
+
+aut = spot.translate('a')
+
+test_assert(aut)
+
+dual = spot.dualize(aut)
+h = dual.to_str('hoa')
+
+assert h == """HOA: v1
+States: 3
+Start: 1
+AP: 1 "a"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic stutter-invariant weak
+--BODY--
+State: 0 {0}
+[t] 0
+State: 1
+[0] 0
+[!0] 2
+State: 2
+[t] 2
+--END--"""
+
+aut = spot.automaton("""
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[0] 1
+[0] 2
+State: 1 {0}
+[0] 1
+State: 2 {0}
+[1] 2
+--END--""")
+
+test_assert(aut)
+dual = spot.dualize(aut)
+h = dual.to_str('hoa')
+
+assert h == """HOA: v1
+States: 4
+Start: 0
+AP: 2 "a" "b"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels state-acc complete