ta.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 <set>
 
#include <cassert>
#include <spot/misc/bddlt.hh>
#include <spot/twa/twa.hh>
 
namespace spot
{
 
  // Forward declarations.  See below.
  class ta_succ_iterator;
 
 
 
 
  class SPOT_API ta
  {
  protected:
    acc_cond acc_;
    bdd_dict_ptr dict_;
 
  public:
    ta(const bdd_dict_ptr& d)
      : dict_(d)
    {
    }
 
    virtual
    ~ta()
    {
    }
 
    typedef std::set<state*, state_ptr_less_than> states_set_t;
    typedef std::set<const state*, state_ptr_less_than> const_states_set_t;
 
    virtual const_states_set_t
    get_initial_states_set() const = 0;
 
    virtual const spot::state*
    get_artificial_initial_state() const
    {
      return nullptr;
    }
 
    virtual ta_succ_iterator*
    succ_iter(const spot::state* state) const = 0;
 
    virtual ta_succ_iterator*
    succ_iter(const spot::state* state, bdd changeset) const = 0;
 
    bdd_dict_ptr
    get_dict() const
    {
      return dict_;
    }
 
    virtual std::string
    format_state(const spot::state* s) const = 0;
 
    virtual bool
    is_accepting_state(const spot::state* s) const = 0;
 
    virtual bool
    is_livelock_accepting_state(const spot::state* s) const = 0;
 
    virtual bool
    is_initial_state(const spot::state* s) const = 0;
 
    virtual bdd
    get_state_condition(const spot::state* s) const = 0;
 
    virtual void
    free_state(const spot::state* s) const = 0;
 
 
    const acc_cond& acc() const
    {
      return acc_;
    }
 
    acc_cond& acc()
    {
      return acc_;
    }
 
  };
 
  typedef std::shared_ptr<ta> ta_ptr;
  typedef std::shared_ptr<const ta> const_ta_ptr;
 
  class ta_succ_iterator : public twa_succ_iterator
  {
  public:
    virtual
    ~ta_succ_iterator()
    {
    }
  };
 
#ifndef SWIG
  // A stack of Strongly-Connected Components
  class scc_stack_ta
  {
  public:
    struct connected_component
    {
    public:
      connected_component(int index = -1) noexcept;
 
      int index;
 
      bool is_accepting;
 
      acc_cond::mark_t condition;
 
      std::list<const state*> rem;
    };
 
    void
    push(int index);
 
    connected_component&
    top();
 
    const connected_component&
    top() const;
 
    void
    pop();
 
    size_t
    size() const;
 
    std::list<const state*>&
    rem();
 
    bool
    empty() const;
 
    typedef std::list<connected_component> stack_type;
    stack_type s;
  };
#endif // !SWIG
 
 
 
 
 
 
 
 
}