spot  2.12
toparity.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <spot/twa/fwd.hh>
22 #include <spot/misc/common.hh>
23 #include <vector>
24 
25 namespace spot
26 {
30  {
32  unsigned nb_states_created = 0;
34  unsigned nb_edges_created = 0;
36  std::vector<std::string> algorithms_used;
37  };
38 
42  {
46  bool search_ex = true;
50  bool use_last = true;
53  bool use_last_post_process = false;
59  bool force_order = true;
63  bool partial_degen = true;
66  bool acc_clean = true;
69  bool parity_equiv = true;
72  bool car = true;
75  bool tar = false;
77  bool iar = true;
80  bool lar_dfs = true;
83  bool bscc = true;
91  bool parity_prefix = true;
95  bool parity_prefix_general = false;
98  bool generic_emptiness = false;
102  bool rabin_to_buchi = true;
105  bool buchi_type_to_buchi = false;
108  bool parity_type_to_parity = false;
112  bool reduce_col_deg = false;
116  bool propagate_col = true;
119  bool use_generalized_rabin = false;
122  bool pretty_print = false;
124  to_parity_data* datas = nullptr;
125  };
126 
143  SPOT_API twa_graph_ptr
144  to_parity(const const_twa_graph_ptr &aut,
145  const to_parity_options options = to_parity_options());
146 
160  SPOT_API twa_graph_ptr
161  to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print = false);
162 
183  SPOT_DEPRECATED("use to_parity() instead") // deprecated since Spot 2.9
184  SPOT_API twa_graph_ptr
185  iar(const const_twa_graph_ptr& aut, bool pretty_print = false);
186 
193  SPOT_DEPRECATED("use to_parity() and spot::acc_cond::is_rabin_like() instead")
194  SPOT_API twa_graph_ptr // deprecated since Spot 2.9
195  iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print = false);
196 
203  SPOT_API twa_graph_ptr
204  parity_type_to_parity(const twa_graph_ptr &aut);
205 
212  SPOT_API twa_graph_ptr
213  buchi_type_to_buchi(const twa_graph_ptr &aut);
214 
221  SPOT_API twa_graph_ptr
222  co_buchi_type_to_co_buchi(const twa_graph_ptr &aut);
223 }
An acceptance condition.
Definition: acc.hh:61
twa_graph_ptr co_buchi_type_to_co_buchi(const twa_graph_ptr &aut)
Convert an automaton into a co-Büchi automaton preserving structure when possible.
twa_graph_ptr to_parity(const const_twa_graph_ptr &aut, const to_parity_options options=to_parity_options())
Take an automaton with any acceptance condition and return an equivalent parity automaton.
twa_graph_ptr to_parity_old(const const_twa_graph_ptr &aut, bool pretty_print=false)
Take an automaton with any acceptance condition and return an equivalent parity automaton.
twa_graph_ptr parity_type_to_parity(const twa_graph_ptr &aut)
Convert an automaton into a parity max automaton preserving structure when possible.
twa_graph_ptr buchi_type_to_buchi(const twa_graph_ptr &aut)
Convert an automaton into a Büchi automaton preserving structure when possible.
Definition: automata.hh:26
Definition: toparity.hh:30
std::vector< std::string > algorithms_used
Name of algorithms used.
Definition: toparity.hh:36
unsigned nb_states_created
Total number of states created.
Definition: toparity.hh:32
unsigned nb_edges_created
Total number of edges created.
Definition: toparity.hh:34
Options to control various optimizations of to_parity().
Definition: toparity.hh:42
bool propagate_col
Definition: toparity.hh:116
bool use_last
Definition: toparity.hh:50
bool rabin_to_buchi
Definition: toparity.hh:102
bool parity_equiv
Definition: toparity.hh:69
bool pretty_print
Definition: toparity.hh:122
bool car
Definition: toparity.hh:72
to_parity_data * datas
Structure used to store some information about the construction.
Definition: toparity.hh:124
bool parity_prefix
Definition: toparity.hh:91
bool iar
If iar is true, to_parity will try to apply IAR.
Definition: toparity.hh:77
bool generic_emptiness
Definition: toparity.hh:98
bool use_generalized_rabin
Definition: toparity.hh:119
bool bscc
Definition: toparity.hh:83
bool reduce_col_deg
Definition: toparity.hh:112
bool acc_clean
Definition: toparity.hh:66
bool parity_prefix_general
Definition: toparity.hh:95
bool tar
Definition: toparity.hh:75
bool use_last_post_process
Definition: toparity.hh:53
bool buchi_type_to_buchi
Definition: toparity.hh:105
bool lar_dfs
Definition: toparity.hh:80
bool force_order
Definition: toparity.hh:59
bool parity_type_to_parity
Definition: toparity.hh:108
bool partial_degen
Definition: toparity.hh:63
bool search_ex
Definition: toparity.hh:46

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1