spot 2.11.6.dev
Loading...
Searching...
No Matches
toparity.hh
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/fwd.hh>
23#include <spot/misc/common.hh>
24#include <vector>
25
26namespace spot
27{
31 {
33 unsigned nb_states_created = 0;
35 unsigned nb_edges_created = 0;
37 std::vector<std::string> algorithms_used;
38 };
39
43 {
47 bool search_ex = true;
51 bool use_last = true;
60 bool force_order = true;
64 bool partial_degen = true;
67 bool acc_clean = true;
70 bool parity_equiv = true;
73 bool car = true;
76 bool tar = false;
78 bool iar = true;
81 bool lar_dfs = true;
84 bool bscc = true;
92 bool parity_prefix = true;
99 bool generic_emptiness = false;
103 bool rabin_to_buchi = true;
113 bool reduce_col_deg = false;
117 bool propagate_col = true;
123 bool pretty_print = false;
126 };
127
144 SPOT_API twa_graph_ptr
145 to_parity(const const_twa_graph_ptr &aut,
146 const to_parity_options options = to_parity_options());
147
161 SPOT_API twa_graph_ptr
162 to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print = false);
163
184 SPOT_DEPRECATED("use to_parity() instead") // deprecated since Spot 2.9
185 SPOT_API twa_graph_ptr
186 iar(const const_twa_graph_ptr& aut, bool pretty_print = false);
187
194 SPOT_DEPRECATED("use to_parity() and spot::acc_cond::is_rabin_like() instead")
195 SPOT_API twa_graph_ptr // deprecated since Spot 2.9
196 iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print = false);
197
204 SPOT_API twa_graph_ptr
205 parity_type_to_parity(const twa_graph_ptr &aut);
206
213 SPOT_API twa_graph_ptr
214 buchi_type_to_buchi(const twa_graph_ptr &aut);
215
222 SPOT_API twa_graph_ptr
223 co_buchi_type_to_co_buchi(const twa_graph_ptr &aut);
224}
An acceptance condition.
Definition acc.hh:62
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 iar(const const_twa_graph_ptr &aut, bool pretty_print=false)
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
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:27
Definition toparity.hh:31
std::vector< std::string > algorithms_used
Name of algorithms used.
Definition toparity.hh:37
unsigned nb_states_created
Total number of states created.
Definition toparity.hh:33
unsigned nb_edges_created
Total number of edges created.
Definition toparity.hh:35
Options to control various optimizations of to_parity().
Definition toparity.hh:43
bool propagate_col
Definition toparity.hh:117
bool use_last
Definition toparity.hh:51
bool rabin_to_buchi
Definition toparity.hh:103
bool parity_equiv
Definition toparity.hh:70
bool pretty_print
Definition toparity.hh:123
bool car
Definition toparity.hh:73
to_parity_data * datas
Structure used to store some information about the construction.
Definition toparity.hh:125
bool parity_prefix
Definition toparity.hh:92
bool iar
If iar is true, to_parity will try to apply IAR.
Definition toparity.hh:78
bool generic_emptiness
Definition toparity.hh:99
bool use_generalized_rabin
Definition toparity.hh:120
bool bscc
Definition toparity.hh:84
bool reduce_col_deg
Definition toparity.hh:113
bool acc_clean
Definition toparity.hh:67
bool parity_prefix_general
Definition toparity.hh:96
bool tar
Definition toparity.hh:76
bool use_last_post_process
Definition toparity.hh:54
bool buchi_type_to_buchi
Definition toparity.hh:106
bool lar_dfs
Definition toparity.hh:81
bool force_order
Definition toparity.hh:60
bool parity_type_to_parity
Definition toparity.hh:109
bool partial_degen
Definition toparity.hh:64
bool search_ex
Definition toparity.hh:47

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.8