to_parity: improve doc, and rename car_option into to_parity_options

* spot/twaalgos/toparity.hh: Improve doc, and rename car_option into
to_parity_options.
* doc/spot.bib: Add one reference.
* python/spot/__init__.py, spot/twaalgos/toparity.cc,
tests/python/toparity.py: Adjust.

doc/spot.bib

@@ -425,6 +425,23 @@
   pages		= {51--61}
 }
 
+@InProceedings{	  kretinsky.17.tacas,
+  author	= {Jan K\v{r}et{\'{\i}}nsk{\'{y}} and Tobias Meggendorfer and
+		  Clara Waldmann and Maximilian Weininger},
+  editor	= {Axel Legay and Tiziana Margaria},
+  title		= {Index Appearance Record for Transforming {R}abin Automata
+		  into Parity Automata},
+  booktitle	= {Proceedings of the 23st International Conference on Tools
+		  and Algorithms for the Construction and Analysis of Systems
+		  (TACAS'17)},
+  part		= {I},
+  series	= {Lecture Notes in Computer Science},
+  volume	= {10205},
+  pages		= {443--460},
+  year		= {2017},
+  doi		= {10.1007/978-3-662-54577-5_26}
+}
+
 @InProceedings{	  kretisnky.12.cav,
   author	= {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza},
   title		= {Deterministic Automata for the {(F,G)}-Fragment of {LTL}},

python/spot/__init__.py

@@ -1293,7 +1293,7 @@ class scc_and_mark_filter:
 
 
 def to_parity(aut, **kwargs):
-    option = car_option()
+    option = to_parity_options()
     if "search_ex" in kwargs:
         option.search_ex = kwargs.get("search_ex")
     if "use_last" in kwargs:

spot/twaalgos/toparity.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2018-2020 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -799,7 +799,7 @@ get_iar_to_vector(const twa_graph_ptr& aut, algorithm algo,
 }
 
 public:
-explicit car_generator(const const_twa_graph_ptr &a, car_option options)
+explicit car_generator(const const_twa_graph_ptr &a, to_parity_options options)
     : aut_(a)
     , scc_(scc_info(a))
     , is_odd(false)
@@ -1600,7 +1600,7 @@ std::vector<car_state> num2car;
 std::map<unsigned, car_state> state2car;
 std::map<car_state, unsigned> car2num;
 
-car_option options;
+to_parity_options options;
 
 std::vector<std::string>* names;
 }; // car_generator
@@ -1624,7 +1624,7 @@ remove_false_transitions(const twa_graph_ptr a)
 }
 
 twa_graph_ptr
-to_parity(const twa_graph_ptr &aut, const car_option options)
+to_parity(const twa_graph_ptr &aut, const to_parity_options options)
 {
     return car_generator(remove_false_transitions(aut), options).run();
 }

spot/twaalgos/toparity.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
+// Copyright (C) 2018-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -23,81 +23,101 @@
 
 namespace spot
 {
-  // The version that combines CAR, IAR and multiple optimizations.
+  /// \ingroup twa_acc_transform
-  struct car_option
+  /// \brief Options to control various optimizations of to_parity().
-{
+  struct to_parity_options
-  bool search_ex      = true;
+  {
-  bool use_last       = true;
+    /// If \c search_ex is true, whenever CAR or IAR have to move
-  bool force_order    = true;
+    /// several elements in a record, it tries to find an order such
-  bool partial_degen  = true;
+    /// that the new permutation already exists.
-  bool acc_clean      = true;
+    bool search_ex      = true;
-  bool parity_equiv   = true;
+    /// If \a use_last is true and \a search_ex are true, we use the
-  bool parity_prefix  = true;
+    /// most recent state when we find multiple existing state
-  bool rabin_to_buchi = true;
+    /// compatible with the current move.
-  bool reduce_col_deg = false;
+    bool use_last       = true;
-  bool propagate_col  = true;
+    bool force_order    = true;
-  bool pretty_print   = false;
+    /// If \c partial_degen is true, apply a partial
-};
+    /// degeneralization to remove occurrences of acceptance
+    /// subformulas such as `Fin(x) | Fin(y)` or `Inf(x) & Inf(y)`.
+    bool partial_degen  = true;
+    /// If \c scc_acc_clean is true, to_parity() will ignore colors
+    /// no occoring in an SCC while processing this SCC.
+    bool acc_clean      = true;
+    /// If \a parity_equiv is true, to_parity() will check if there
+    /// exists a permutations of colors such that the acceptance
+    /// condition is a parity condition.
+    bool parity_equiv   = true;
+    bool parity_prefix  = true;
+    bool rabin_to_buchi = true;
+    bool reduce_col_deg = false;
+    bool propagate_col  = true;
+    /// If \a pretty_print is true, states of the output automaton are
+    /// named to help debugging.
+    bool pretty_print   = false;
+  };
 
 
 
-/// \ingroup twa_acc_transform
+  /// \ingroup twa_acc_transform
-/// \brief Take an automaton with any acceptance condition and return an
+  /// \brief Take an automaton with any acceptance condition and return an
-/// equivalent parity automaton.
+  /// equivalent parity automaton.
-///
+  ///
-/// The parity condition of the returned automaton is max even or
+  /// The parity condition of the returned automaton is either max even or
-/// max odd.
+  /// max odd.
-/// If \a search_ex is true, when we move several elements, we
+  ///
-/// try to find an order  such that the new permutation already exists.
+  /// This procedure combines many strategies in an attempt to produce
-/// If \a partial_degen is true, we apply a partial degeneralization to remove
+  /// the smallest possible parity automaton.  Some of the strategies
-// occurences of Fin | Fin and Inf & Inf.
+  /// include CAR (color acceptance record), IAR (index appearance
-/// If \a scc_acc_clean is true, we remove for each SCC the colors that don't
+  /// record), partial degenerazation, conversion from Rabin to Büchi
-// appear.
+  /// when possible, etc.
-/// If \a parity_equiv is true, we check if there exists a permutations of
+  ///
-// colors such that the acceptance
+  /// The \a options argument can be used to selectively disable some of the
-/// condition is a partity condition.
+  /// optimizations.
-/// If \a use_last is true, we use the most recent state when looking for an
+  SPOT_API twa_graph_ptr
-// existing state.
+  to_parity(const twa_graph_ptr &aut,
-/// If \a pretty_print is true, we give a name to the states describing the
+            const to_parity_options options = to_parity_options());
-// state of the aut_ and the permutation.
 
   SPOT_API twa_graph_ptr
   remove_false_transitions(const twa_graph_ptr a);
 
-  SPOT_API twa_graph_ptr
-  to_parity(const twa_graph_ptr &aut, const car_option options = car_option());
-
-
-  // Old version of CAR
 
   /// \ingroup twa_acc_transform
   /// \brief Take an automaton with any acceptance condition and return an
   /// equivalent parity automaton.
   ///
   /// The parity condition of the returned automaton is max even.
+  ///
+  /// This implements a straightforward adaptation of the LAR (latest
+  /// appearance record) to automata with transition-based marks.  We
+  /// call this adaptation the CAR (color apperance record), as it
+  /// tracks colors (i.e., acceptance sets) instead of states.
+  ///
+  /// It is better to use to_parity() instead, as it will use better
+  /// strategies when possible, and has additional optimizations.
   SPOT_API twa_graph_ptr
   to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print=false);
 
-  // Old version of IAR
   /// \ingroup twa_acc_transform
   /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton
   /// based on the index appearence record (IAR)
   ///
+  /// This is an implementation of \cite kretinsky.17.tacas .
   /// 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.
+  ///
   /// If the input automaton is Rabin-like (resp. Streett-like), the output
   /// automaton has max odd (resp. min even) acceptance condition.
-  /// Details on the algorithm can be found in:
-  ///   https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)
   ///
   /// Throws an std::runtime_error if the input is neither Rabin-like nor
   /// Street-like.
-  SPOT_API
+  ///
-  twa_graph_ptr
+  /// It is better to use to_parity() instead, as it will use better
+  /// strategies when possible, and has additional optimizations.
+  SPOT_API twa_graph_ptr
   iar_old(const const_twa_graph_ptr& aut, bool pretty_print = false);
 
   /// \ingroup twa_acc_transform
@@ -105,9 +125,9 @@ namespace spot
   /// based on the index appearence record (IAR)
   ///
   /// Returns nullptr if the input automaton is neither Rabin-like nor
-  /// Streett-like, and calls spot::iar() otherwise.
+  /// Streett-like, and calls spot::iar_old() otherwise.
   SPOT_API
   twa_graph_ptr
   iar_maybe_old(const const_twa_graph_ptr& aut, bool pretty_print = false);
 
-} // namespace spot
+} // namespace spot

tests/python/toparity.py

@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -22,7 +22,7 @@ import spot
 
 # Tests for the new version of to_parity
 
-no_option = spot.car_option()
+no_option = spot.to_parity_options()
 no_option.search_ex = False
 no_option.use_last = False
 no_option.force_order = False
@@ -33,7 +33,7 @@ no_option.parity_prefix = False
 no_option.rabin_to_buchi = False
 no_option.propagate_col = False
 
-acc_clean_search_opt = spot.car_option()
+acc_clean_search_opt = spot.to_parity_options()
 acc_clean_search_opt.force_order = False
 acc_clean_search_opt.partial_degen = False
 acc_clean_search_opt.parity_equiv = False
@@ -41,7 +41,7 @@ acc_clean_search_opt.parity_prefix = False
 acc_clean_search_opt.rabin_to_buchi = False
 acc_clean_search_opt.propagate_col = False
 
-partial_degen_opt = spot.car_option()
+partial_degen_opt = spot.to_parity_options()
 partial_degen_opt.search_ex = False
 partial_degen_opt.force_order = False
 partial_degen_opt.parity_equiv = False
@@ -49,7 +49,7 @@ partial_degen_opt.parity_prefix = False
 partial_degen_opt.rabin_to_buchi = False
 partial_degen_opt.propagate_col = False
 
-parity_equiv_opt = spot.car_option()
+parity_equiv_opt = spot.to_parity_options()
 parity_equiv_opt.search_ex = False
 parity_equiv_opt.use_last = False
 parity_equiv_opt.force_order = False
@@ -58,7 +58,7 @@ parity_equiv_opt.parity_prefix = False
 parity_equiv_opt.rabin_to_buchi = False
 parity_equiv_opt.propagate_col = False
 
-rab_to_buchi_opt = spot.car_option()
+rab_to_buchi_opt = spot.to_parity_options()
 rab_to_buchi_opt.use_last = False
 rab_to_buchi_opt.force_order = False
 rab_to_buchi_opt.partial_degen = False
@@ -67,14 +67,14 @@ rab_to_buchi_opt.parity_prefix = False
 rab_to_buchi_opt.propagate_col = False
 
 # Force to use CAR or IAR for each SCC
-use_car_opt = spot.car_option()
+use_car_opt = spot.to_parity_options()
 use_car_opt.partial_degen = False
 use_car_opt.parity_equiv = False
 use_car_opt.parity_prefix = False
 use_car_opt.rabin_to_buchi = False
 use_car_opt.propagate_col = False
 
-all_opt = spot.car_option()
+all_opt = spot.to_parity_options()
 all_opt.pretty_print = True