spot 2.12.2
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
25namespace 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;
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;
98 bool generic_emptiness = false;
102 bool rabin_to_buchi = true;
112 bool reduce_col_deg = false;
116 bool propagate_col = true;
122 bool pretty_print = false;
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.4