translate.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// 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/twaalgos/postproc.hh>
#include <spot/tl/simplify.hh>
 
namespace spot
{
  struct mtdswa;
  typedef std::shared_ptr<mtdswa> mtdswa_ptr;
 
  class SPOT_API translator: protected postprocessor
  {
  public:
    translator(tl_simplifier* simpl, const option_map* opt = nullptr)
      : postprocessor(opt), simpl_(simpl), simpl_owned_(nullptr)
    {
      SPOT_ASSERT(simpl);
      setup_opt(opt);
    }
 
    translator(const bdd_dict_ptr& dict, const option_map* opt = nullptr)
      : postprocessor(opt)
    {
      setup_opt(opt);
      build_simplifier(dict);
    }
 
    translator(const option_map* opt = nullptr)
      : postprocessor(opt)
    {
      setup_opt(opt);
      build_simplifier(make_bdd_dict());
    }
 
    ~translator()
    {
      // simpl_owned_ is 0 if simpl_ was supplied to the constructor.
      delete simpl_owned_;
    }
 
    using postprocessor::output_type;
 
    void
    set_type(output_type type)
    {
      this->postprocessor::set_type(type);
    }
 
    using postprocessor::output_pref;
 
    void
    set_pref(output_pref pref)
    {
      this->postprocessor::set_pref(pref);
    }
 
    using postprocessor::optimization_level;
 
    void
    set_level(optimization_level level)
    {
      level_ = level;
      if (simpl_owned_)
        {
          auto d = simpl_owned_->get_dict();
          delete simpl_owned_;
          build_simplifier(d);
        }
      if (!gf_guarantee_set_)
        gf_guarantee_ = level != Low;
    }
 
    twa_graph_ptr run(formula f);
 
    twa_graph_ptr run(formula* f);
 
    void clear_caches();
 
  protected:
    void setup_opt(const option_map* opt);
    void build_simplifier(const bdd_dict_ptr& dict);
    twa_graph_ptr run_aux(formula f);
    twa_graph_ptr run_q(formula f);
    twa_graph_ptr finish_obligation_mtdswa(formula f, mtdswa_ptr mtdwa);
    twa_graph_ptr translate_via_fm(formula f, bool unambiguous);
    static void add_leading_x(twa_graph_ptr& aut, unsigned n);
 
  private:
    tl_simplifier* simpl_;
    tl_simplifier* simpl_owned_;
    int comp_susp_;
    int early_susp_;
    int skel_wdba_;
    int skel_simul_;
    int relabel_bool_;
    int relabel_overlap_;
    int tls_impl_;
    int new_oblig_ = -1;
    bool gf_guarantee_ = true;
    bool gf_guarantee_set_ = false;
    bool ltl_split_;
    int branchpost_ = -1;
    unsigned tls_max_states_ = 64;
    unsigned tls_max_ops_ = 16;
    int exprop_;
    const option_map* opt_;
  };
 
}