ltl2tgba_fm.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/tl/formula.hh>
#include <spot/twa/twagraph.hh>
#include <spot/tl/apcollect.hh>
#include <spot/tl/simplify.hh>
#include <spot/twaalgos/powerset.hh>
 
namespace spot
{
  SPOT_API twa_graph_ptr
  ltl_to_tgba_fm(formula f, const bdd_dict_ptr& dict,
                 bool exprop = false, bool symb_merge = true,
                 bool branching_postponement = false,
                 bool fair_loop_approx = false,
                 const atomic_prop_set* unobs = nullptr,
                 tl_simplifier* simplifier = nullptr,
                 bool unambiguous = false,
                 const output_aborter* aborter = nullptr,
                 bool label_with_ltl = false,
                 bool force_obligation = false);
 
  struct SPOT_API fm_edge
  {
    bdd cond;              
    formula dst;           
    acc_cond::mark_t acc;  
  };
 
  struct SPOT_API fm_simple_edge
  {
    acc_cond::mark_t acc;  
    formula dst;           
  };
 
  class SPOT_API ltl_to_tgba_fm_otf final
  {
  public:
    struct options
    {
      bool exprop = false;
      bool symb_merge = true;
      bool branching_postponement = false;
      bool fair_loop_approx = false;
      bool unambiguous = false;
      bool force_obligation = false;
      options() {}
    };
 
    ltl_to_tgba_fm_otf(formula f, twa_graph_ptr aut,
                options opts = options(),
                tl_simplifier* simplifier = nullptr,
                const atomic_prop_set* unobs = nullptr);
 
    ~ltl_to_tgba_fm_otf();
 
    // Non-copyable, non-movable.
    ltl_to_tgba_fm_otf(const ltl_to_tgba_fm_otf&) = delete;
    ltl_to_tgba_fm_otf& operator=(const ltl_to_tgba_fm_otf&) = delete;
 
    // ---- State interface ----
 
    formula init_state() const;
 
    formula orig_formula() const;
 
    // ---- Symbolic successor view ----
 
    bdd succ_as_bdd(formula s);
 
    // ---- Explicit successor view ----
 
    std::vector<fm_edge> succ_as_edges(formula s);
 
    std::vector<fm_simple_edge> succ_as_acc_and_dest(formula s);
 
    // ---- Accessors for interpreting succ_as_bdd() results ----
 
    const bdd& var_set() const;
 
    const bdd& next_set() const;
 
    const bdd& a_set() const;
 
    formula conj_bdd_to_formula(bdd cube) const;
 
    acc_cond::mark_t bdd_to_mark(bdd a) const;
 
    int register_next_variable(formula f);
 
    const bdd_dict_ptr& get_dict() const;
 
  private:
    struct impl;
    std::unique_ptr<impl> impl_;
  };
 
}