parity.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2016-2019, 2022 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/misc/common.hh>
#include <spot/twa/fwd.hh>
#include <vector>
 
namespace spot
{
 
 
  enum parity_kind
  {
    parity_kind_max,
    parity_kind_min,
    parity_kind_same,
    parity_kind_any
  };
 
  enum parity_style
  {
    parity_style_odd,
    parity_style_even,
    parity_style_same,
    parity_style_any
  };
 
  SPOT_API twa_graph_ptr
  change_parity(const const_twa_graph_ptr& aut,
                parity_kind kind, parity_style style);
 
  SPOT_API twa_graph_ptr
  change_parity_here(twa_graph_ptr aut, parity_kind kind, parity_style style);
 
  SPOT_API twa_graph_ptr
  cleanup_parity(const const_twa_graph_ptr& aut,
                            bool keep_style = false);
 
  SPOT_API twa_graph_ptr
  cleanup_parity_here(twa_graph_ptr aut, bool keep_style = false);
 
  SPOT_API twa_graph_ptr
  colorize_parity(const const_twa_graph_ptr& aut, bool keep_style = false);
 
  SPOT_API twa_graph_ptr
  colorize_parity_here(twa_graph_ptr aut, bool keep_style = false);
 
  SPOT_API twa_graph_ptr
  reduce_parity(const const_twa_graph_ptr& aut,
                bool colored = false, bool layered = false);
 
  SPOT_API twa_graph_ptr
  reduce_parity_here(twa_graph_ptr aut,
                     bool colored = false, bool layered = false);
 
 
  struct SPOT_API reduce_parity_data
  {
    bool parity_max;       
    bool parity_odd;       
    std::vector<int> piprime1;
    std::vector<int> piprime2;
 
    reduce_parity_data(const const_twa_graph_ptr& aut, bool layered = false);
  };
 
}