saba.hh 4.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
20
21
22
23
24
25
26
27
28

#ifndef SPOT_SABA_SABA_HH
# define SPOT_SABA_SABA_HH

#include "sabastate.hh"
#include "sabasucciter.hh"
#include <tgba/bdddict.hh>

namespace spot
{
29
  /// \defgroup saba SABA (State-based Alternating Büchi Automata)
30
31
32
33
34
35
36
37
38
39
40
  ///
  /// Spot was centered around non-deterministic \ref tgba.
  /// Alternating automata are an extension to non-deterministic
  /// automata, and are presented with spot::saba.
  /// This type and its cousins are listed \ref saba_essentials "here".
  /// This is an abstract interface.

  /// \addtogroup saba_essentials Essential SABA types
  /// \ingroup saba

  /// \ingroup saba_essentials
41
  /// \brief A State-based Alternating (Generalized) Büchi Automaton.
42
43
44
45
46
47
48
49
50
51
  ///
  /// Browsing such automaton can be achieved using two functions:
  /// \c get_init_state, and \c succ_iter.  The former returns
  /// the initial state while the latter lists the
  /// successor states of any state.
  ///
  /// Note that although this is a transition-based automata,
  /// we never represent transitions!  Transition informations are
  /// obtained by querying the iterator over the successors of
  /// a state.
52
  class SPOT_API saba
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
  {
  protected:
    saba();

  public:
    virtual ~saba();

    /// \brief Get the initial state of the automaton.
    ///
    /// The state has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    virtual saba_state* get_init_state() const = 0;

    /// \brief Get an iterator over the successors of \a local_state.
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    ///
    /// \param local_state The state whose successors are to be explored.
    /// This pointer is not adopted in any way by \c succ_iter, and
    /// it is still the caller's responsability to delete it when
    /// appropriate (this can be done during the lifetime of
    /// the iterator).
    virtual saba_succ_iterator*
    succ_iter(const saba_state* local_state) const = 0;

    /// \brief Get the dictionary associated to the automaton.
    ///
    /// State are represented as BDDs.  The dictionary allows
    /// to map BDD variables back to formulae, and vice versa.
    /// This is useful when dealing with several automata (which
    /// may use the same BDD variable for different formula),
    /// or simply when printing.
88
    virtual bdd_dict_ptr get_dict() const = 0;
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111

    /// \brief Format the state as a string for printing.
    ///
    /// This formating is the responsability of the automata
    /// that owns the state.
    virtual std::string format_state(const saba_state* state) const = 0;

    /// \brief Return the set of all acceptance conditions used
    /// by this automaton.
    ///
    /// The goal of the emptiness check is to ensure that
    /// a strongly connected component walks through each
    /// of these acceptiong conditions.  I.e., the union
    /// of the acceptiong conditions of all transition in
    /// the SCC should be equal to the result of this function.
    virtual bdd all_acceptance_conditions() const = 0;

    /// The number of acceptance conditions.
    virtual unsigned int number_of_acceptance_conditions() const;
  private:
    mutable int num_acc_;
  };

112
113
114
  typedef std::shared_ptr<saba> saba_ptr;
  typedef std::shared_ptr<const saba> const_saba_ptr;

115
116
117
118
} // end namespace spot.


#endif // SPOT_SABA_SABA_HH