1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2018-2020 Laboratoire de Recherche et Développement 3 // de l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <spot/twa/twagraph.hh> 23 24 namespace spot 25 { 26 /// \ingroup twa_acc_transform 27 /// \brief Options to control various optimizations of to_parity(). 28 struct to_parity_options 29 { 30 /// If \c search_ex is true, whenever CAR or IAR have to move 31 /// several elements in a record, it tries to find an order such 32 /// that the new permutation already exists. 33 bool search_ex = true; 34 /// If \c use_last is true and \a search_ex are true, we use the 35 /// most recent state when we find multiple existing state 36 /// compatible with the current move. 37 bool use_last = true; 38 /// If \c force_order is true, we force to use an order when CAR or IAR is 39 /// applied. Given a state s and a set E ({0}, {0 1}, {2} for example) we 40 /// construct an order on colors. With the given example, we ask to have 41 /// a permutation that start with [0 …], [0 1 …] or [2 …] in 42 /// that order of preference. 43 bool force_order = true; 44 /// If \c partial_degen is true, apply a partial 45 /// degeneralization to remove occurrences of acceptance 46 /// subformulas such as `Fin(x) | Fin(y)` or `Inf(x) & Inf(y)`. 47 bool partial_degen = true; 48 /// If \c force_degen is false, to_parity will checks if we can 49 /// get a better result if we don't apply partial_degeneralize. 50 bool force_degen = true; 51 /// If \c scc_acc_clean is true, to_parity() will ignore colors 52 /// not occurring in an SCC while processing this SCC. 53 bool acc_clean = true; 54 /// If \c parity_equiv is true, to_parity() will check if there 55 /// exists a permutations of colors such that the acceptance 56 /// condition is a parity condition. 57 bool parity_equiv = true; 58 /// If \c parity_prefix is true, to_parity() will use a special 59 /// handling for acceptance conditions of the form `Inf(m0) | 60 /// (Fin(m1) & (Inf(m2) | (… β)))` that start as a parity 61 /// condition (modulo a renumbering of `m0`, `m1`, `m2`, ...) but where 62 /// `β` can be an arbitrary formula. In this case, the paritization 63 /// algorithm is really applied only to `β`, and the marks of the 64 /// prefix are appended after a suitable renumbering. 65 /// 66 /// For technical reasons, activating this option (and this is the 67 /// default) causes reduce_parity() to be called at the end to 68 /// minimize the number of colors used. It is therefore 69 /// recommended to disable this option when one wants to follow 70 /// the output CAR/IAR constructions. 71 bool parity_prefix = true; 72 /// If \c rabin_to_buchi is true, to_parity() tries to convert a Rabin or 73 /// Streett condition to Büchi or co-Büchi with 74 /// rabin_to_buchi_if_realizable(). 75 bool rabin_to_buchi = true; 76 /// Only allow degeneralization if it reduces the number of colors in the 77 /// acceptance condition. 78 bool reduce_col_deg = false; 79 /// Use propagate_marks_here to increase the number of marks on transition 80 /// in order to move more colors (and increase the number of 81 /// compatible states) when we apply LAR. 82 bool propagate_col = true; 83 /// If \c pretty_print is true, states of the output automaton are 84 /// named to help debugging. 85 bool pretty_print = false; 86 }; 87 88 89 /// \ingroup twa_acc_transform 90 /// \brief Take an automaton with any acceptance condition and return an 91 /// equivalent parity automaton. 92 /// 93 /// If the input is already a parity automaton of any kind, it is 94 /// returned unchanged. Otherwise a new parity automaton with max 95 /// odd or max even condition is created. 96 /// 97 /// This procedure combines many strategies in an attempt to produce 98 /// the smallest possible parity automaton. Some of the strategies 99 /// include CAR (color acceptance record), IAR (index appearance 100 /// record), partial degenerazation, conversion from Rabin to Büchi 101 /// when possible, etc. 102 /// 103 /// The \a options argument can be used to selectively disable some of the 104 /// optimizations. 105 SPOT_API twa_graph_ptr 106 to_parity(const const_twa_graph_ptr &aut, 107 const to_parity_options options = to_parity_options()); 108 109 /// \ingroup twa_acc_transform 110 /// \brief Take an automaton with any acceptance condition and return an 111 /// equivalent parity automaton. 112 /// 113 /// The parity condition of the returned automaton is max even. 114 /// 115 /// This implements a straightforward adaptation of the LAR (latest 116 /// appearance record) to automata with transition-based marks. We 117 /// call this adaptation the CAR (color apperance record), as it 118 /// tracks colors (i.e., acceptance sets) instead of states. 119 /// 120 /// It is better to use to_parity() instead, as it will use better 121 /// strategies when possible, and has additional optimizations. 122 SPOT_API twa_graph_ptr 123 to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print = false); 124 125 /// \ingroup twa_acc_transform 126 /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton 127 /// based on the index appearence record (IAR) 128 /// 129 /// This is an implementation of \cite kretinsky.17.tacas . 130 /// If the input automaton has n states and k pairs, the output automaton has 131 /// at most k!*n states and 2k+1 colors. If the input automaton is 132 /// deterministic, the output automaton is deterministic as well, which is the 133 /// intended use case for this function. If the input automaton is 134 /// non-deterministic, the result is still correct, but way larger than an 135 /// equivalent Büchi automaton. 136 /// 137 /// If the input automaton is Rabin-like (resp. Streett-like), the output 138 /// automaton has max odd (resp. min even) acceptance condition. 139 /// 140 /// Throws an std::runtime_error if the input is neither Rabin-like nor 141 /// Street-like. 142 /// 143 /// It is better to use to_parity() instead, as it will use better 144 /// strategies when possible, and has additional optimizations. 145 SPOT_DEPRECATED("use to_parity() instead") // deprecated since Spot 2.9 146 SPOT_API twa_graph_ptr 147 iar(const const_twa_graph_ptr& aut, bool pretty_print = false); 148 149 /// \ingroup twa_acc_transform 150 /// \brief Turn a Rabin-like or Streett-like automaton into a parity automaton 151 /// based on the index appearence record (IAR) 152 /// 153 /// Returns nullptr if the input automaton is neither Rabin-like nor 154 /// Streett-like, and calls spot::iar() otherwise. 155 SPOT_DEPRECATED("use to_parity() and spot::acc_cond::is_rabin_like() instead") 156 SPOT_API twa_graph_ptr // deprecated since Spot 2.9 157 iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print = false); 158 159 } // namespace spot 160