rabin_to_buchi_if_realizable: new function

* spot/twaalgos/remfin.cc, spot/twaalgos/remfin.hh: Implement it.
* tests/python/tra2tba.py: Test it.
* NEWS: Mention it.

NEWS

@@ -79,6 +79,12 @@ New in spot 2.8.5.dev (not yet released)
     should be on each transition; propagate_marks_here() actually
     modifies the automaton.
 
+  - rabin_to_buchi_if_realizable() is a new variant of
+    rabin_to_buchi_maybe() that converts a Rabin-like automaton into a
+    Büchi automaton only if the resulting Büchi automaton can keep the
+    same transition structure (where the ..._maybe() variant would
+    modify the Rabin automaton if needed).
+
   Bugs fixed:
 
   - degeneralize_tba() was incorrectly not honnoring the "skip_level"

spot/twaalgos/remfin.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -791,6 +791,37 @@ namespace spot
     return true;
   }
 
+  twa_graph_ptr
+  rabin_to_buchi_if_realizable(const const_twa_graph_ptr& aut)
+  {
+    std::vector<acc_cond::rs_pair> pairs;
+    if (!aut->acc().is_rabin_like(pairs))
+      return nullptr;
+
+    auto aut_pairs = rs_pairs_view(pairs);
+    auto code = aut->get_acceptance();
+    if (code.is_t())
+      return nullptr;
+
+    scc_info si(aut, scc_info_options::TRACK_STATES);
+    std::vector<bool> final(aut->edge_vector().size(), false);
+    std::vector<bool> keep(aut->edge_vector().size(), true);
+
+    for (unsigned scc = 0; scc < si.scc_count(); ++scc)
+      if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final))
+        return nullptr;
+
+    auto res = make_twa_graph(aut, twa::prop_set::all());
+    auto m = res->set_buchi();
+
+    auto& ev = res->edge_vector();
+    unsigned edgecount = ev.size();
+    for (unsigned eidx = 1; eidx < edgecount; ++eidx)
+      ev[eidx].acc = final[eidx] ? m : acc_cond::mark_t{};
+
+    return res;
+  }
+
   twa_graph_ptr
   rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
   {

spot/twaalgos/remfin.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et
+// Copyright (C) 2015, 2017, 2018, 2020 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -24,15 +24,37 @@
 namespace spot
 {
   /// \ingroup twa_acc_transform
-  /// \brief Check if \aut is Büchi-realizable. This is inspired
+  /// \brief Check if \a aut is Rablin-like and Büchi-realizable.
-  /// from rabin_to_buchi_maybe()'s algorithm. The main difference is that
+  ///
-  /// here, no automaton is built.
+  /// This is inspired from rabin_to_buchi_maybe()'s algorithm. The
+  /// main difference is that here, no automaton is built.
+  ///
+  /// If the input is non-deterministic, this algorithm may fail
+  /// to detect Büchi-realizability (false-negative).
   SPOT_API bool
   rabin_is_buchi_realizable(const const_twa_graph_ptr& aut);
 
   /// \ingroup twa_acc_transform
-  /// \brief Convert a Rabin automaton to Büchi automaton, preserving
+  /// \brief Convert a Rabin-like automaton into a Büchi automaton only
-  /// determinism when possible.
+  /// when it can be done without changing the automaton structure.
+  ///
+  /// If \a aut is a Rabin-like automaton that is not Büchi-realizable,
+  /// this returns a Büchi automaton equivalent to \a aut that use
+  /// exactly the same transition structure (the order of edges is
+  /// even preserved).  In particular, determinism is preserved.
+  ///
+  /// If \a aut is not a Rabin-like automaton or is not
+  /// Büchi-realizable, return `nullptr`.
+  ///
+  /// If the input is non-deterministic, this algorithm may fail
+  /// to detect Büchi-realizability (false-negative).
+  SPOT_API twa_graph_ptr
+  rabin_to_buchi_if_realizable(const const_twa_graph_ptr& aut);
+
+  /// \ingroup twa_acc_transform
+  ///
+  /// \brief Convert a Rabin-like automaton into a Büchi automaton,
+  /// preserving determinism when possible.
   ///
   /// Return nullptr if the input is not a Rabin (or Rabin-like)
   /// automaton.
@@ -43,7 +65,8 @@ namespace spot
   ///
   /// Unless you know what you are doing, you are probably better off
   /// calling remove_fin() instead, as this will call more specialized
-  /// algorithms (e.g., for weak automata) when appropriate.
+  /// algorithms (e.g., for weak automata) when appropriate, and will
+  /// deal with more than just Rabin-like automata.
   SPOT_API twa_graph_ptr
   rabin_to_buchi_maybe(const const_twa_graph_ptr& aut);
 

tests/python/tra2tba.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016-2018  Laboratoire de Recherche et Développement
+# Copyright (C) 2016-2018, 2020  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -482,10 +482,31 @@ State: 1
 [0] 1 {0}
 --END--"""
 
-
 res = spot.remove_fin(aut)
 assert(res.to_str('hoa') == exp)
 
+# Different order for rabin_to_buchi_if_realizable() due to merge_edges() not
+# being called.  This is on purpose: the edge order should match exactly the
+# original automaton.
+exp2 = """HOA: v1
+States: 2
+Start: 0
+AP: 2 "p0" "p2"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[0] 1
+[!0] 0 {0}
+State: 1
+[0] 1 {0}
+[!0] 0 {0}
+--END--"""
+res = spot.rabin_to_buchi_if_realizable(aut)
+assert(res.to_str('hoa') == exp2)
+
 # Test 12.
 aut = spot.automaton("""
 HOA: v1
@@ -574,6 +595,32 @@ State: 1
 res = spot.remove_fin(aut)
 assert(res.to_str('hoa') == exp)
 
+# rabin_to_buchi_if_realizable() does not call merge_edges() on purpose: the
+# edge order should match exactly the original automaton.
+exp2 = """HOA: v1
+States: 2
+Start: 0
+AP: 2 "p3" "p2"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[0&1] 1
+[0&!1] 0 {0}
+[!0&1] 1
+[!0&!1] 0 {0}
+State: 1
+[0&1] 1 {0}
+[0&!1] 0 {0}
+[!0&1] 1 {0}
+[!0&!1] 0 {0}
+--END--"""
+
+res = spot.rabin_to_buchi_if_realizable(aut)
+assert(res.to_str('hoa') == exp2)
+
 # Test 14.
 aut = spot.automaton("""
 HOA: v1
@@ -608,3 +655,4 @@ State: 1
 
 res = spot.remove_fin(aut)
 assert(res.to_str('hoa') == exp)
+assert spot.rabin_to_buchi_if_realizable(aut) is None