Rabin to parity translation

* spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
  implement it
* spot/twaalgos/postproc.cc: use it
* spot/twaalgos/Makefile.am: build the new files
* NEWS: document the new function
* python/spot/impl.i: Python bindings for the new function
* tests/Makefile.am, tests/core/rabin2parity.test: test the new function

NEWS

@@ -83,6 +83,11 @@ New in spot 2.4.4.dev (net yet released)
 
   New functions in the library:
 
+  - spot::iar() and spot::iar_maybe() use index appearance records (IAR)
+    to translate Rabin-like automata into equivalent parity automaton.
+    This translation preserves determinism and is especially useful when
+    the input automaton is deterministic.
+
   - spot::print_aiger() encodes an automaton as an AIGER circuit, as
     required by the SYNTCOMP competition.  It relies on a new named
     property "synthesis outputs" that describes which atomic

python/spot/impl.i

@@ -163,6 +163,7 @@
 #include <spot/twaalgos/relabel.hh>
 #include <spot/twaalgos/word.hh>
 #include <spot/twaalgos/are_isomorphic.hh>
+#include <spot/twaalgos/rabin2parity.hh>
 
 #include <spot/parseaut/public.hh>
 
@@ -617,6 +618,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/word.hh>
 %template(list_bdd) std::list<bdd>;
 %include <spot/twaalgos/are_isomorphic.hh>
+%include <spot/twaalgos/rabin2parity.hh>
 
 %pythonprepend spot::twa::dtwa_complement %{
   from warnings import warn

spot/twaalgos/Makefile.am

@@ -67,6 +67,7 @@ twaalgos_HEADERS = \
   postproc.hh \
   powerset.hh \
   product.hh \
+  rabin2parity.hh \
   randomgraph.hh \
   randomize.hh \
   reachiter.hh \
@@ -132,6 +133,7 @@ libtwaalgos_la_SOURCES = \
   postproc.cc \
   powerset.cc \
   product.cc \
+  rabin2parity.cc \
   randomgraph.cc \
   randomize.cc \
   reachiter.cc \

spot/twaalgos/postproc.cc

@@ -38,6 +38,7 @@
 #include <spot/twaalgos/parity.hh>
 #include <spot/twaalgos/cobuchi.hh>
 #include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/rabin2parity.hh>
 
 namespace spot
 {
@@ -240,7 +241,15 @@ namespace spot
     if ((via_gba && !a->acc().is_generalized_buchi())
         || (want_parity && !a->acc().is_parity()))
       {
-        a = to_generalized_buchi(a);
+        twa_graph_ptr b = nullptr;
+        if (want_parity && is_deterministic(a))
+          b = iar_maybe(a);
+        // possible only if a was deterministic and Rabin-like and
+        // we want parity
+        if (b)
+          a = b;
+        else
+          a = to_generalized_buchi(a);
         if (PREF_ == Any && level_ == Low)
           a = do_scc_filter(a, true);
       }

spot/twaalgos/rabin2parity.cc

@@ -0,0 +1,293 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2017-2018 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/>.
+
+#include <deque>
+
+#include <spot/twaalgos/rabin2parity.hh>
+
+#include <spot/twaalgos/sccinfo.hh>
+#include <spot/twaalgos/isdet.hh>
+
+namespace spot
+{
+  namespace
+  {
+
+    using perm_t = std::vector<unsigned>;
+    struct iar_state
+    {
+      unsigned state;
+      perm_t perm;
+
+      bool
+      operator<(const iar_state& other) const
+      {
+        return state == other.state ? perm < other.perm : state < other.state;
+      }
+    };
+
+    class iar_generator
+    {
+    public:
+      explicit iar_generator(const const_twa_graph_ptr& a,
+                             const std::vector<acc_cond::rs_pair>& p)
+      : aut_(a)
+      , pairs_(p)
+      , scc_(scc_info(a))
+      {}
+
+      twa_graph_ptr
+      run()
+      {
+        res_ = make_twa_graph(aut_->get_dict());
+        res_->copy_ap_of(aut_);
+
+        build_iar_scc(scc_.initial());
+
+        // resulting automaton has acceptance condition: parity max odd
+        // with priorities ranging from 0 to 2*(nb Rabin pairs)
+        // /!\ priorities are shifted by -1 compared to the original paper
+        res_->set_acceptance(2*pairs_.size() + 1,
+            acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1));
+
+        // set initial state
+        res_->set_init_state(
+            iar2num.at(state2iar.at(aut_->get_init_state_number())));
+
+        // there could be quite a number of unreachable states, prune them
+        res_->purge_unreachable_states();
+
+        return res_;
+      }
+
+      void
+      build_iar_scc(unsigned scc_num)
+      {
+        // we are working on an SCC: the state we start from does not matter
+        unsigned init = scc_.one_state_of(scc_num);
+
+        std::deque<iar_state> todo;
+        auto get_state = [&](const iar_state& s)
+          {
+            auto it = iar2num.find(s);
+            if (it == iar2num.end())
+              {
+                unsigned nb = res_->new_state();
+                iar2num[s] = nb;
+                num2iar[nb] = s;
+                todo.push_back(s);
+                return nb;
+              }
+            return it->second;
+          };
+
+        auto get_other_scc = [this](unsigned state)
+          {
+            auto it = state2iar.find(state);
+            // recursively build the destination SCC if we detect that it has
+            // not been already built.
+            if (it == state2iar.end())
+              build_iar_scc(scc_.scc_of(state));
+            return iar2num.at(state2iar.at(state));
+          };
+
+        if (scc_.is_trivial(scc_num))
+          {
+            iar_state iar_s{init, perm_t()};
+            state2iar[init] = iar_s;
+            unsigned src_num = get_state(iar_s);
+            // Do not forget to connect to subsequent SCCs
+            for (const auto& e : aut_->out(init))
+              res_->new_edge(src_num, get_other_scc(e.dst), e.cond);
+            return;
+          }
+
+        // determine the Rabin pairs that appear in the SCC
+        auto colors = scc_.acc_sets_of(scc_num);
+        std::set<unsigned> scc_pairs;
+        for (unsigned k = 0; k != pairs_.size(); ++k)
+          if (colors & (pairs_[k].fin | pairs_[k].inf))
+            scc_pairs.insert(k);
+
+        perm_t p0;
+        for (unsigned k : scc_pairs)
+          p0.push_back(k);
+
+        iar_state s0{init, p0};
+        get_state(s0); // put s0 in todo
+
+        // the main loop
+        while (!todo.empty())
+          {
+            iar_state current = todo.front();
+            todo.pop_front();
+
+            unsigned src_num = get_state(current);
+
+            for (const auto& e : aut_->out(current.state))
+              {
+                // connect to the appropriate state
+                if (scc_.scc_of(e.dst) != scc_num)
+                  res_->new_edge(src_num, get_other_scc(e.dst), e.cond);
+                else
+                  {
+                    // find the new permutation
+                    perm_t new_perm = current.perm;
+                    // Count pairs whose fin-part is seen on this transition
+                    unsigned seen_nb = 0;
+                    std::vector<unsigned> seen;
+                    // consider the pairs for this SCC only
+                    for (unsigned k : scc_pairs)
+                      if (e.acc & pairs_[k].fin)
+                        {
+                          ++seen_nb;
+                          auto it = std::find(new_perm.begin(),
+                                              new_perm.end(),
+                                              k);
+                          // move the pair in front of the permutation
+                          std::rotate(new_perm.begin(), it, it+1);
+                        }
+
+                    iar_state dst;
+                    unsigned dst_num = -1U;
+
+                    // Optimization: when several indices are seen in the
+                    // transition, they move at the front of new_perm in any
+                    // order. Check whether there already exists an iar_state
+                    // that matches this condition.
+                    for (unsigned i = 0; i != num2iar.size(); ++i)
+                      if (num2iar[i].state == e.dst)
+                        if (std::equal(new_perm.begin() + seen_nb,
+                                       new_perm.end(),
+                                       num2iar[i].perm.begin() + seen_nb))
+                          {
+                            dst = num2iar[i];
+                            dst_num = i;
+                            break;
+                          }
+                    // if such a state was not found, build it
+                    if (dst_num == -1U)
+                      {
+                        dst = iar_state{e.dst, new_perm};
+                        dst_num = get_state(dst);
+                      }
+
+                    // find the maximal index encountered by this transition
+                    unsigned maxint = -1U;
+                    for (unsigned k = 0; k != current.perm.size(); ++k)
+                      {
+                        unsigned pk = current.perm[k];
+                        if (e.acc & (pairs_[pk].fin | pairs_[pk].inf))
+                          // k increases in the loop, so k > maxint necessarily
+                          maxint = k;
+                      }
+
+                    acc_cond::mark_t acc = 0U;
+                    if (maxint == -1U)
+                      acc = {0};
+                    else if (e.acc & pairs_[current.perm[maxint]].fin)
+                      acc = {2*maxint+2};
+                    else
+                      acc = {2*maxint+1};
+
+                    res_->new_edge(src_num, dst_num, e.cond, acc);
+                  }
+              }
+          }
+
+        // Optimization: find the bottom SCC of the sub-automaton we have just
+        // built. To that end, we have to ignore edges going out of scc_num.
+        auto leaving_edge = [&](unsigned d)
+          {
+            return scc_.scc_of(num2iar.at(d).state) != scc_num;
+          };
+        auto filter_edge = [](const twa_graph::edge_storage_t&,
+                              unsigned dst,
+                              void* filter_data)
+          {
+            decltype(leaving_edge)* data =
+              static_cast<decltype(leaving_edge)*>(filter_data);
+
+            if ((*data)(dst))
+              return scc_info::edge_filter_choice::ignore;
+            return scc_info::edge_filter_choice::keep;
+          };
+        scc_info sub_scc(res_, get_state(s0), filter_edge, &leaving_edge);
+        // SCCs are numbered in reverse topological order, so the bottom SCC has
+        // index 0.
+        const unsigned bscc = 0;
+        assert(sub_scc.succ(0).empty());
+        assert(
+            [&]()
+            {
+              for (unsigned s = 1; s != sub_scc.scc_count(); ++s)
+                if (sub_scc.succ(s).empty())
+                  return false;
+              return true;
+            } ());
+
+        assert(sub_scc.states_of(bscc).size()
+            >= scc_.states_of(scc_num).size());
+
+        // update state2iar
+        for (const auto& scc_state : sub_scc.states_of(bscc))
+          {
+            iar_state iar = num2iar.at(scc_state);
+            if (state2iar.find(iar.state) == state2iar.end())
+              state2iar[iar.state] = iar;
+          }
+      }
+
+    private:
+      const const_twa_graph_ptr& aut_;
+      const std::vector<acc_cond::rs_pair>& pairs_;
+      const scc_info scc_;
+      twa_graph_ptr res_;
+
+      // to be used when entering a new SCC
+      // maps a state of aut_ onto an iar_state with the appropriate perm
+      std::map<unsigned, iar_state> state2iar;
+
+      std::map<iar_state, unsigned> iar2num;
+      std::map<unsigned, iar_state> num2iar;
+    };
+  }
+
+  twa_graph_ptr
+  iar_maybe(const const_twa_graph_ptr& aut)
+  {
+    std::vector<acc_cond::rs_pair> rabin_pairs;
+    if (!aut->acc().is_rabin_like(rabin_pairs))
+      return nullptr;
+
+    iar_generator gen(aut, rabin_pairs);
+    return gen.run();
+  }
+
+  twa_graph_ptr
+  iar(const const_twa_graph_ptr& aut)
+  {
+    auto res = iar_maybe(aut);
+    if (!res)
+      throw std::runtime_error("rabin2parity works only for Rabin-like "
+          "automata");
+
+    return res;
+  }
+}
+

spot/twaalgos/rabin2parity.hh

@@ -0,0 +1,46 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2017-2018 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/>.
+
+#pragma once
+
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+  /// \brief Turn a Rabin-like automaton into a parity automaton based on the
+  /// index appearence record (IAR)
+  ///
+  /// If the input automaton has n states and k pairs, the output automaton has
+  /// at most k!*n states and 2k+1 colors. If the input automaton is
+  /// deterministic, the output automaton is deterministic as well, which is the
+  /// intended use case for this function. If the input automaton is
+  /// non-deterministic, the result is still correct, but way larger than an
+  /// equivalent Büchi automaton. The output parity automaton has max odd
+  /// acceptance condition.
+  /// Details on the algorithm can be found in:
+  ///   https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)
+  SPOT_API
+  twa_graph_ptr
+  iar(const const_twa_graph_ptr& aut);
+
+  /// Return nullptr if the input automaton is not Rabin-like, and calls iar()
+  /// otherwise.
+  SPOT_API
+  twa_graph_ptr
+  iar_maybe(const const_twa_graph_ptr& aut);
+}

tests/Makefile.am

@@ -313,7 +313,8 @@ TESTS_twa = \
   core/dnfstreett.test \
   core/parity.test \
   core/parity2.test \
-  core/ltlsynt.test
+  core/ltlsynt.test \
+  core/rabin2parity.test
 
 ############################## PYTHON ##############################
 

tests/core/rabin2parity.test

@@ -0,0 +1,49 @@
+#!/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 <<EOF
+HOA: v1
+name: "FXGa"
+properties: deterministic
+properties: complete
+States: 2
+Start: 0
+acc-name: Rabin 1
+Acceptance: 2 Fin(0)&Inf(1)
+AP: 1 "a"
+--BODY--
+State: 0
+[t] 1 {0 1 }
+State: 1
+[0] 1 {1 }
+[!0] 1 {0 1 }
+--END--
+EOF
+# random automata
+randaut 5 -n100 -u -D --acceptance="Rabin 0..6"
+) | \
+autcross \
+  "autfilt --parity" \
+  "autfilt"
+