postproc.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2012-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/twa/twagraph.hh>
 
namespace spot
{
  class option_map;
 
 
  class SPOT_API postprocessor
  {
  public:
    postprocessor(const option_map* opt = nullptr);
 
    enum output_type {
      TGBA = 0, // Historical.  Use GeneralizedBuchi instead
      GeneralizedBuchi = 0, // Introduced in Spot 2.10 to replace TGBA
      BA = 1, // Historical.  Implies Buchi and SBAcc.
      Monitor = 2,
      Generic = 3,
      Parity = 4,
      ParityMin = Parity | 8,
      ParityMax = Parity | 16,
      ParityOdd = Parity | 32,
      ParityEven = Parity | 64,
      ParityMinOdd = ParityMin | ParityOdd,
      ParityMaxOdd = ParityMax | ParityOdd,
      ParityMinEven = ParityMin | ParityEven,
      ParityMaxEven = ParityMax | ParityEven,
      CoBuchi = 128,
      Buchi = 256, // introduced in Spot 2.10, does not imply SBAcc
    };
 
    void
    set_type(output_type type)
    {
      type_ = type;
    }
 
    enum
    {
      Any = 0,
      Small = 1,                // Small and Deterministic
      Deterministic = 2,        // are exclusive choices.
      Complete = 4,
      SBAcc = 8,                // State-based acceptance.
      Unambiguous = 16,
      Colored = 32,             // Colored parity; requires parity acceptance
    };
    typedef int output_pref;
 
    void
    set_pref(output_pref pref)
    {
      pref_ = pref;
    }
 
    enum optimization_level { Low, Medium, High };
    void
    set_level(optimization_level level)
    {
      level_ = level;
    }
 
    twa_graph_ptr run(twa_graph_ptr input, formula f = nullptr);
 
  protected:
    twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt) const;
    twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt) const;
    twa_graph_ptr choose_degen(const twa_graph_ptr& input) const;
    twa_graph_ptr do_degen(const twa_graph_ptr& input) const;
    twa_graph_ptr do_degen_tba(const twa_graph_ptr& input) const;
    twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg) const;
    twa_graph_ptr do_scc_filter(const twa_graph_ptr& a) const;
    twa_graph_ptr finalize(twa_graph_ptr tmp) const;
 
    output_type type_ = TGBA;
    int pref_ = Small;
    optimization_level level_ = High;
    // Fine-tuning options fetched from the option_map.
    bool degen_reset_ = true;
    bool degen_order_ = false;
    int degen_cache_ = 1;
    bool degen_lskip_ = true;
    bool degen_lowinit_ = false;
    bool degen_remscc_ = true;
    bool det_scc_ = true;
    int det_simul_ = -1;
    bool det_stutter_ = true;
    int det_max_states_ = -1;
    int det_max_edges_ = -1;
    int simul_ = -1;
    int simul_method_ = -1;
    int simul_trans_pruning_ = 512;
    int dpa_simul_ = -1;
    int dba_simul_ = -1;
    int scc_filter_ = -1;
    int ba_simul_ = -1;
    bool tba_determinisation_ = false;
    int sat_minimize_ = 0;
    int sat_incr_steps_ = 0;
    bool sat_langmap_ = false;
    int sat_acc_ = 0;
    int sat_states_ = 0;
    int gen_reduce_parity_ = 1;
    bool state_based_ = false;
    int wdba_minimize_ = -1;
    int simul_max_ = 4096;
    int merge_states_min_ = 128;
    int wdba_det_max_ = 4096;
    bool acd_ = false;
    bool acd_was_used_;
  };
}