toparity.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2018-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/twa/fwd.hh>
#include <spot/misc/common.hh>
#include <vector>
 
namespace spot
{
  struct to_parity_data
  {
    unsigned nb_states_created = 0;
    unsigned nb_edges_created = 0;
    std::vector<std::string> algorithms_used;
  };
 
  struct to_parity_options
  {
    bool search_ex = true;
    bool use_last = true;
    bool use_last_post_process = false;
    bool force_order = true;
    bool partial_degen = true;
    bool acc_clean = true;
    bool parity_equiv = true;
    bool car = true;
    bool tar = false;
    bool iar = true;
    bool lar_dfs = true;
    bool bscc = true;
    bool parity_prefix = true;
    bool parity_prefix_general = false;
    bool generic_emptiness = false;
    bool rabin_to_buchi = true;
    bool buchi_type_to_buchi = false;
    bool parity_type_to_parity = false;
    bool reduce_col_deg = false;
    bool propagate_col = true;
    bool use_generalized_rabin = false;
    bool pretty_print = false;
    to_parity_data* datas = nullptr;
  };
 
  SPOT_API twa_graph_ptr
  to_parity(const const_twa_graph_ptr &aut,
            const to_parity_options options = to_parity_options());
 
  SPOT_API twa_graph_ptr
  to_parity_old(const const_twa_graph_ptr& aut, bool pretty_print = false);
 
  SPOT_DEPRECATED("use to_parity() instead") // deprecated since Spot 2.9
  SPOT_API twa_graph_ptr
  iar(const const_twa_graph_ptr& aut, bool pretty_print = false);
 
  SPOT_DEPRECATED("use to_parity() and spot::acc_cond::is_rabin_like() instead")
  SPOT_API twa_graph_ptr   // deprecated since Spot 2.9
  iar_maybe(const const_twa_graph_ptr& aut, bool pretty_print = false);
 
  SPOT_API twa_graph_ptr
  parity_type_to_parity(const twa_graph_ptr &aut);
 
  SPOT_API twa_graph_ptr
  buchi_type_to_buchi(const twa_graph_ptr &aut);
 
  SPOT_API twa_graph_ptr
  co_buchi_type_to_co_buchi(const twa_graph_ptr &aut);
}