From 1750c0fb6d29eb5c131ee7590819324a4c5319d3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 4 Apr 2020 14:43:47 +0200 Subject: [PATCH] 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 | 17 ++++++ python/spot/__init__.py | 2 +- spot/twaalgos/toparity.cc | 8 +-- spot/twaalgos/toparity.hh | 114 ++++++++++++++++++++++---------------- tests/python/toparity.py | 16 +++--- 5 files changed, 97 insertions(+), 60 deletions(-) diff --git a/doc/spot.bib b/doc/spot.bib index 87259d815..3dc3bc29f 100644 --- a/doc/spot.bib +++ b/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}}, diff --git a/python/spot/__init__.py b/python/spot/__init__.py index d92353026..dfd01dad1 100644 --- a/python/spot/__init__.py +++ b/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: diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 2bd5b6f94..0d6aca350 100644 --- a/spot/twaalgos/toparity.cc +++ b/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 num2car; std::map state2car; std::map car2num; -car_option options; +to_parity_options options; std::vector* 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(); } diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh index e9ad49907..b8a67b98c 100644 --- a/spot/twaalgos/toparity.hh +++ b/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. - struct car_option -{ - bool search_ex = true; - bool use_last = true; - bool force_order = true; - bool partial_degen = true; - bool acc_clean = true; - bool parity_equiv = true; - bool parity_prefix = true; - bool rabin_to_buchi = true; - bool reduce_col_deg = false; - bool propagate_col = true; - bool pretty_print = false; -}; + /// \ingroup twa_acc_transform + /// \brief Options to control various optimizations of to_parity(). + struct to_parity_options + { + /// If \c search_ex is true, whenever CAR or IAR have to move + /// several elements in a record, it tries to find an order such + /// that the new permutation already exists. + bool search_ex = true; + /// If \a use_last is true and \a search_ex are true, we use the + /// most recent state when we find multiple existing state + /// compatible with the current move. + bool use_last = true; + bool force_order = true; + /// 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 -/// \brief Take an automaton with any acceptance condition and return an -/// equivalent parity automaton. -/// -/// The parity condition of the returned automaton is max even or -/// 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. -/// If \a partial_degen is true, we apply a partial degeneralization to remove -// occurences of Fin | Fin and Inf & Inf. -/// If \a scc_acc_clean is true, we remove for each SCC the colors that don't -// appear. -/// If \a parity_equiv is true, we check if there exists a permutations of -// colors such that the acceptance -/// condition is a partity condition. -/// If \a use_last is true, we use the most recent state when looking for an -// existing state. -/// If \a pretty_print is true, we give a name to the states describing the -// state of the aut_ and the permutation. + /// \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 either max even or + /// max odd. + /// + /// This procedure combines many strategies in an attempt to produce + /// the smallest possible parity automaton. Some of the strategies + /// include CAR (color acceptance record), IAR (index appearance + /// record), partial degenerazation, conversion from Rabin to Büchi + /// when possible, etc. + /// + /// The \a options argument can be used to selectively disable some of the + /// optimizations. + SPOT_API twa_graph_ptr + to_parity(const twa_graph_ptr &aut, + const to_parity_options options = to_parity_options()); 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 \ No newline at end of file +} // namespace spot diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 90cc533df..78cb2afc0 100644 --- a/tests/python/toparity.py +++ b/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