twaalgos/cobuchi: Add nsa_to_nca()

* NEWS: Update.
* spot/twaalgos/cobuchi.hh: Declare to_dca() and nsa_to_nca().
* spot/twaalgos/cobuchi.cc: Implement them.
* python/spot/impl.i: Include new file for python bindings.
* spot/twaalgos/Makefile.am: Add new file.
* bin/autfilt.cc: Add --dca command line option. This option does not
return a deterministic automaton yet, but it will.
* tests/core/dca.test: Add tests for Büchi automata.
* tests/python/dca.py: Add a python script that builds a nondet. Streett
automaton.
* tests/python/dca.test: Add tests for Streett automata.
* tests/Makefile.am: Add all tests.

NEWS

@@ -19,6 +19,13 @@ New in spot 2.4.0.dev (not yet released)
     specified SCC. It must only be called on automata with a
     Streett-like acceptance condition.
 
+  - The new function nsa_to_nca() is able to convert when possible an
+    automaton with a Streett-like acceptance to an equivalent
+    automaton with a co-Büchi acceptance. Actually the resulting
+    automaton will always recognize at least the same language. It can
+    recognize more if the original language can not be expressed with
+    a co-Büchi acceptance condition.
+
   Deprecation notices:
 
   (These functions still work but compilers emit warnings.)

bin/autfilt.cc

@@ -47,6 +47,7 @@
 #include <spot/tl/exclusive.hh>
 #include <spot/twaalgos/are_isomorphic.hh>
 #include <spot/twaalgos/canonicalize.hh>
+#include <spot/twaalgos/cobuchi.hh>
 #include <spot/twaalgos/cleanacc.hh>
 #include <spot/twaalgos/dtwasat.hh>
 #include <spot/twaalgos/dualize.hh>
@@ -89,6 +90,7 @@ enum {
   OPT_COMPLEMENT,
   OPT_COMPLEMENT_ACC,
   OPT_COUNT,
+  OPT_DCA,
   OPT_DECOMPOSE_SCC,
   OPT_DESTUT,
   OPT_DUALIZE,
@@ -350,6 +352,12 @@ static const argp_option options[] =
       "solver can be set thanks to the SPOT_SATSOLVER environment variable"
       "(see spot-x)."
       , 0 },
+    { "dca", OPT_DCA, nullptr, 0,
+      "convert to deterministic co-Büchi. The resulting automaton will always "
+      "recognize at least the same language. Actually, it can recognize "
+      "more if the original language can not be expressed using a co-Büchi "
+      "acceptance condition."
+      , 0 },
     { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
     { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
       OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
@@ -511,6 +519,7 @@ static const char* opt_sat_minimize = nullptr;
 static int opt_highlight_nondet_states = -1;
 static int opt_highlight_nondet_edges = -1;
 static bool opt_highlight_languages = false;
+static bool opt_dca = false;
 
 static spot::twa_graph_ptr
 ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
@@ -594,6 +603,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_COMPLEMENT_ACC:
       opt_complement_acc = true;
       break;
+     case OPT_DCA:
+      opt_dca = true;
+      break;
     case OPT_DECOMPOSE_SCC:
       opt_decompose_scc = arg;
       break;
@@ -1190,6 +1202,8 @@ namespace
         aut = spot::to_generalized_rabin(aut, opt_gra == GRA_SHARE_INF);
       if (opt_gsa)
         aut = spot::to_generalized_streett(aut, opt_gsa == GSA_SHARE_FIN);
+      if (opt_dca)
+        aut = spot::to_dca(aut, false);
 
       if (opt_simplify_exclusive_ap && !opt->excl_ap.empty())
         aut = opt->excl_ap.constrain(aut, true);

python/spot/impl.i

@@ -121,6 +121,8 @@
 #include <spot/twaalgos/degen.hh>
 #include <spot/twaalgos/dot.hh>
 #include <spot/twaalgos/dualize.hh>
+#include <spot/twaalgos/cobuchi.hh>
+#include <spot/twaalgos/copy.hh>
 #include <spot/twaalgos/complete.hh>
 #include <spot/twaalgos/complement.hh>
 #include <spot/twaalgos/emptiness.hh>
@@ -537,6 +539,8 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/cleanacc.hh>
 %include <spot/twaalgos/degen.hh>
 %include <spot/twaalgos/dot.hh>
+%include <spot/twaalgos/cobuchi.hh>
+%include <spot/twaalgos/copy.hh>
 %include <spot/twaalgos/complete.hh>
 %feature("flatnested") spot::twa_run::step;
 %include <spot/twaalgos/emptiness.hh>

spot/twaalgos/Makefile.am

@@ -33,6 +33,7 @@ twaalgos_HEADERS = \
   bfssteps.hh \
   canonicalize.hh \
   cleanacc.hh \
+  cobuchi.hh \
   complete.hh \
   complement.hh \
   compsusp.hh \
@@ -95,6 +96,7 @@ libtwaalgos_la_SOURCES = \
   bfssteps.cc \
   canonicalize.cc \
   cleanacc.cc \
+  cobuchi.cc \
   complete.cc \
   complement.cc \
   compsusp.cc \

spot/twaalgos/cobuchi.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/twaalgos/cobuchi.hh>
+
+#include <spot/misc/bitvect.hh>
+#include <spot/twaalgos/powerset.hh>
+#include <spot/twaalgos/product.hh>
+#include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/totgba.hh>
+
+#include <stack>
+#include <unordered_map>
+
+namespace spot
+{
+  namespace
+  {
+    typedef std::pair<unsigned, unsigned> pair_state_nca;
+
+    // Helper function that returns the called 'augmented subset construction'
+    // of the given automaton, i.e. the product of the automaton  with its
+    // powerset construction.
+    //
+    // 'aut_power' is the automaton that will be used for the powerset
+    // construction and 'aut_prod' is the one that will be used for the
+    // product. They may be confusing in the sense that why the same automaton
+    // is not used for the product and the powerset construction. Actually,
+    // when dealing with an automaton A with Rabin acceptance, it is firstly
+    // converted into an automaton B with Streett-like acceptance. The powerset
+    // construction of B happens to be isomorphic with the powerset construction
+    // of A. Therefore, you would like to use A (which is smaller than B) for
+    // the powerset construction and B for the product.
+    static
+    twa_graph_ptr
+    aug_subset_cons(const const_twa_graph_ptr& aut_prod,
+                    const const_twa_graph_ptr& aut_power,
+                    bool named_states,
+                    struct power_map& pmap)
+    {
+      twa_graph_ptr res = product(aut_prod, tgba_powerset(aut_power, pmap));
+
+      if (named_states)
+        {
+          const product_states* res_map = res->get_named_prop
+            <product_states>("product-states");
+
+          auto v = new std::vector<std::string>;
+          res->set_named_prop("state-names", v);
+
+          auto get_st_name =
+            [&](const pair_state_nca& x)
+            {
+              std::stringstream os;
+              os << x.first << ",{";
+              bool not_first = false;
+              for (auto& a : pmap.states_of(x.second))
+                {
+                  if (not_first)
+                    os << ',';
+                  else
+                    not_first = true;
+                  os << a;
+                }
+              os << '}';
+              return os.str();
+            };
+
+          unsigned num_states = res->num_states();
+          for (unsigned i = 0; i < num_states; ++i)
+            v->emplace_back(get_st_name((*res_map)[i]));
+        }
+      return res;
+    }
+
+    class nsa_to_nca_converter final
+    {
+      protected:
+        struct power_map pmap_;                 // Sets of sts (powerset cons.).
+
+        const_twa_graph_ptr aut_;               // The given automaton.
+        bool state_based_;                      // Is it state based?
+        std::vector<acc_cond::rs_pair> pairs_;  // All pairs of the acc. cond.
+        unsigned nb_pairs_;                     // Nb pair in the acc. cond.
+        bool named_states_;                     // Name states for display?
+        twa_graph_ptr res_;                     // The augmented subset const.
+        product_states* res_map_;               // States of the aug. sub. cons.
+        scc_info si_;                           // SCC information.
+        unsigned nb_states_;                    // Number of states.
+        unsigned was_rabin_;                    // Was it Rabin before Streett?
+        std::vector<unsigned>* orig_states_;    // Match old Rabin st. from new.
+        unsigned orig_num_st_;                  // Rabin original nb states.
+
+        // Keep information of states that are wanted to be seen infinitely
+        // often (cf Header).
+        void save_inf_nca_st(unsigned s, acc_cond::mark_t m,
+                             vect_nca_info* nca_info)
+        {
+          if (was_rabin_ && m)
+            {
+              for (unsigned p = 0; p < nb_pairs_; ++p)
+                if (pairs_[p].fin || m & pairs_[p].inf)
+                  {
+                    const pair_state_nca& st = (*res_map_)[s];
+                    auto bv = make_bitvect(orig_num_st_);
+                    for (unsigned state : pmap_.states_of(st.second))
+                      bv->set(state);
+                    assert(!was_rabin_
+                            || ((int)(*orig_states_)[st.first] >= 0));
+                    unsigned state = was_rabin_ ? (*orig_states_)[st.first]
+                                              : st.first;
+                    unsigned clause_nb = was_rabin_ ? p / 2 : p;
+                    nca_info->push_back(new nca_st_info(clause_nb, state, bv));
+                  }
+            }
+          else if (!was_rabin_)
+            {
+              const pair_state_nca& st = (*res_map_)[s];
+              auto bv = make_bitvect(aut_->num_states());
+              for (unsigned state : pmap_.states_of(st.second))
+                bv->set(state);
+              nca_info->push_back(new nca_st_info(0, st.first, bv));
+            }
+        }
+
+        // Helper function that marks states that we want to see finitely often
+        // and save some information about states that we want to see infinitely
+        // often (cf Header).
+        void set_marks_using(std::vector<bool>& nca_is_inf_state,
+                             vect_nca_info* nca_info)
+        {
+          for (unsigned s = 0; s < nb_states_; ++s)
+            {
+              unsigned src_scc = si_.scc_of(s);
+              if (nca_is_inf_state[s])
+                {
+                  acc_cond::mark_t m = 0u;
+                  for (auto& e : res_->out(s))
+                    {
+                      if (nca_info && e.acc && (si_.scc_of(e.dst) == src_scc
+                                                   || state_based_))
+                        m |= e.acc;
+                      e.acc = 0u;
+                    }
+
+                  if (nca_info)
+                    save_inf_nca_st(s, m, nca_info);
+                }
+              else
+                {
+                  for (auto& e : res_->out(s))
+                    {
+                      if (si_.scc_of(e.dst) == src_scc || state_based_)
+                          e.acc = acc_cond::mark_t({0});
+                      else
+                        e.acc = 0u;
+                    }
+                }
+            }
+        }
+
+      public:
+
+        nsa_to_nca_converter(const const_twa_graph_ptr ref_prod,
+                             const const_twa_graph_ptr ref_power,
+                             std::vector<acc_cond::rs_pair>& pairs,
+                             bool named_states = false,
+                             bool was_rabin = false,
+                             unsigned orig_num_st = 0)
+          : aut_(ref_prod),
+            state_based_((bool)aut_->prop_state_acc()),
+            pairs_(pairs),
+            nb_pairs_(pairs.size()),
+            named_states_(named_states),
+            res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)),
+            res_map_(res_->get_named_prop<product_states>("product-states")),
+            si_(scc_info(res_)),
+            nb_states_(res_->num_states()),
+            was_rabin_(was_rabin),
+            orig_num_st_(orig_num_st)
+        {
+          if (was_rabin)
+            orig_states_ = ref_prod->get_named_prop<std::vector<unsigned>>
+                                      ("original-states");
+        }
+
+        ~nsa_to_nca_converter()
+        {}
+
+        twa_graph_ptr run(vect_nca_info* nca_info)
+        {
+          std::vector<bool> nca_is_inf_state;    // Accepting or rejecting sts.
+          nca_is_inf_state.resize(nb_states_, false);
+
+          // Iterate over all SCCs and check for accepting states. A state 's'
+          // is accepting if there is a cycle containing 's' that visits
+          // finitely often all acceptance sets marked as Fin or infinitely
+          // often acceptance sets marked by Inf.
+          unsigned nb_scc = si_.scc_count();
+          for (unsigned scc = 0; scc < nb_scc; ++scc)
+            for (unsigned st : si_.states_on_acc_cycle_of(scc))
+              nca_is_inf_state[st] = true;
+
+          set_marks_using(nca_is_inf_state, nca_info);
+
+          res_->prop_state_acc(state_based_);
+          res_->set_co_buchi();
+          res_->merge_edges();
+          return res_;
+        }
+    };
+  }
+
+
+  twa_graph_ptr
+  nsa_to_nca(const const_twa_graph_ptr& ref,
+             bool named_states,
+             vect_nca_info* nca_info)
+  {
+    twa_graph_ptr ref_tmp = ref->acc().is_parity() ? to_generalized_streett(ref)
+                                                   : nullptr;
+    std::vector<acc_cond::rs_pair> pairs;
+    if (!(ref_tmp ? ref_tmp : ref)->acc().is_streett_like(pairs))
+      throw std::runtime_error("nsa_to_nca() only works with Streett-like or "
+                               "Parity acceptance condition");
+
+    nsa_to_nca_converter nca_converter(ref_tmp ? ref_tmp : ref,
+                                       ref_tmp ? ref_tmp : ref,
+                                       pairs,
+                                       named_states,
+                                       false);
+    return nca_converter.run(nca_info);
+  }
+
+
+  twa_graph_ptr
+  to_dca(const const_twa_graph_ptr& aut, bool named_states)
+  {
+    std::vector<acc_cond::rs_pair> pairs;
+    if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity())
+      return nsa_to_nca(aut, named_states);
+    else
+      throw std::runtime_error("to_dca() only works with Streett-like or Parity"
+                               " acceptance condition");
+  }
+}

spot/twaalgos/cobuchi.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/bitvect.hh>
+#include <spot/twa/fwd.hh>
+
+#include <vector>
+
+namespace spot
+{
+  /// A vector of nca_st_info is given as argument to nsa_to_nca(). Each
+  /// nca_st_info has information about a state that must be seen infinitely
+  /// often. For a state 's' visited infinitely often by a run, the information
+  /// provided is:
+  ///  - the clause number satisfied by the run (from left to right)
+  ///  - the state number of 's'
+  ///  - destinations of all outgoing edges of 's' (represented as a bitvect)
+  struct nca_st_info
+  {
+    unsigned clause_num;
+    unsigned state_num;
+    bitvect* all_dst;
+
+    nca_st_info(unsigned clause, unsigned st, bitvect* dst)
+    {
+      clause_num = clause;
+      state_num = st;
+      all_dst = dst;
+    }
+
+    ~nca_st_info()
+    {
+      delete all_dst;
+    }
+  };
+
+  typedef std::vector<struct nca_st_info*> vect_nca_info;
+
+  /// \brief Converts a nondet Streett-like aut. to a nondet. co-Büchi aut.
+  ///
+  /// This function works in top of the augmented subset construction algorithm
+  /// and is described in section 3.1 of:
+  /** \verbatim
+      @Article{boker.2009.lcs,
+        author    = {Udi Boker and Orna Kupferman},
+        title     = {Co-Büching Them All},
+        booktitle = {Foundations of Software Science and Computational
+                     Structures - 14th International Conference, FOSSACS 2011}
+        year      = {2011},
+        pages     = {184--198},
+        url       = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
+      }
+      \endverbatim */
+  /// This implementation is quite different from the described algorithm. It
+  /// is made to work with automaton with Street-like acceptance (including
+  /// Büchi).
+  ///
+  /// \a aut The automaton to convert.
+  /// \a named_states name each state for easier debugging.
+  /// \a nca_info retrieve information about state visited infinitely often.
+  SPOT_API twa_graph_ptr
+  nsa_to_nca(const const_twa_graph_ptr& aut,
+             bool named_states = false,
+             vect_nca_info* nca_info = nullptr);
+
+  /// \brief Converts any ω-automata to det. co-buchi (when possible)
+  ///
+  /// The resulting automaton will always recognize at least the same language.
+  /// Actually, it can recognize more if the original language can not be
+  /// expressed using a co-Büchi acceptance condition.
+  SPOT_API twa_graph_ptr
+  to_dca(const const_twa_graph_ptr& aut, bool named_states = false);
+}

tests/Makefile.am

@@ -299,7 +299,8 @@ TESTS_twa = \
   core/complementation.test \
   core/randpsl.test \
   core/cycles.test \
-  core/acc_word.test
+  core/acc_word.test \
+  core/dca.test
 
 ############################## PYTHON ##############################
 
@@ -340,6 +341,7 @@ TESTS_python = \
   python/bdditer.py \
   python/bddnqueen.py \
   python/bugdet.py \
+  python/dca.test \
   python/declenv.py \
   python/decompose_scc.py \
   python/dualize.py \
@@ -390,6 +392,7 @@ nb-html: $(TESTS_ipython:.ipynb=.html)
 EXTRA_DIST = \
   $(TESTS) \
   python/ltl2tgba.py \
+  python/dca.py \
   python/ipnbdoctest.py
 
 

tests/core/dca.test

+#!/bin/sh
+# -*- 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/>.
+
+. ./defs
+set -e
+
+cat >formulas <<'EOF'
+0
+F!(!b <-> FGb)
+1
+a W F(a -> b)
+((0 R Xa) R a) -> Fa
+!Xa & (Gb R (Xa W 0))
+(1 U b) | F(Fb W (a <-> FXa))
+(a M 1) | (!a W a)
+(G!a W ((b M 1) -> Fa)) -> !a
+!a xor (a <-> b)
+b & (a <-> b)
+b
+(a | b | (a -> b)) R b
+Xa
+!b
+!Fb | !Xb
+!(b | Gb)
+XXX(b | Gb)
+(a & F(a | FG(a W b))) U a
+FGXb M (!b M b)
+a
+((a & !b) W Ga) W a
+(b <-> FGb) M 1
+X!b
+FX!(a xor !a)
+Fb R (a & (a <-> b))
+XXb | (b W 0)
+1 U (b xor !b)
+G!(b M 1) W (1 U b)
+!(Fa M Xa)
+
+
+(!b U b) U X(!a -> Fb)
+(b | (Fa R (b W a))) M 1
+1 U (a xor b)
+XF!b
+X(!(!b | (a M b)) -> XXa)
+(FXXF(a R Fa) R Xb) U XFb
+!Gb
+F(Xb xor XXb)
+F(XF!a & (Fb U !a))
+!b M 1
+b M Fb
+!(a xor (b xor ((b W Ga) -> b)))
+!(a -> (a & !a)) xor !(a U !b)
+!(0 R !b)
+Fa M FXb
+Fa & (Fa | (!a -> Gb))
+Xb M X!a
+Gb xor (b W !b)
+F!(a | (b W a))
+F(1 U b)
+F(!a M 1)
+XF((b <-> (a <-> b)) | Fb)
+F(a U !b)
+(!a | b) U (1 U F(a M !b))
+!(Xb -> (b W a))
+!(0 R !X(Fb U a))
+X((a -> b) M 1)
+Fb M F(a W b)
+FXF(a <-> (Xb -> b))
+Xa | !((b W 0) & (a | Fb))
+
+
+!(F!b M 1)
+X(!a W Xb)
+!Fb xor G((b xor (Xa M b)) U b)
+(0 R b) R (a R Xa)
+Gb
+a W X(b | Xb)
+a W b
+X(Xb & (!Ga R Ga))
+!Fb
+a & GXa
+XX(X(a xor b) W 0)
+!a -> ((a xor !GFa) W 0)
+b M Gb
+Xa R XXG(!a & (Fa W Gb))
+G!b W b
+G(b | G!a)
+a xor ((!Xb M 1) & (b M a))
+
+G(b xor (a <-> !a))
+!((a | (XXa & (a M Gb))) U b)
+!(!b -> b) W a
+b | !(b M 1)
+G((Fa W !a) xor !(0 R b))
+0 R ((Ga xor Xb) -> (0 R a))
+G!Xa
+!(X!b M a)
+!(!b M a) W !a
+G(a & X!Xb)
+Xb -> Gb
+(b | X!b) W a
+b W (!b xor (!a M FXb))
+
+
+((b M 1) M 1) xor (a xor Ga)
+b <-> (a M 1)
+a xor F(!X!Fa xor (b U Xa))
+G!(!b R (Xb W b))
+(Fa & Xb) | G(b U Ga)
+!(a R Gb) R !a
+!(Gb U a)
+(FXb & XGa) xor F(Xa M 1)
+Gb <-> !((1 U a) -> b)
+(a U b) & ((b U a) R FX!Ga)
+Xb <-> F!a
+!(a xor F(1 U Fb))
+Fa <-> G(a R b)