tgba.hh 9.99 KB
Newer Older
1
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
Guillaume Sadegh's avatar
Guillaume Sadegh committed
2
3
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
4
5
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
6
7
8
9
10
//
// 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
11
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
12
13
14
15
16
17
18
19
// (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
20
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
21

22
23
24
#ifndef SPOT_TGBA_TGBA_HH
# define SPOT_TGBA_TGBA_HH

25
#include "state.hh"
26
#include "succiter.hh"
27
#include "bdddict.hh"
28
29
30

namespace spot
{
31
  /// \defgroup tgba TGBA (Transition-based Generalized Büchi Automata)
32
33
34
35
36
37
38
39
40
41
42
43
44
  ///
  /// Spot is centered around the spot::tgba type.  This type and its
  /// cousins are listed \ref tgba_essentials "here".  This is an
  /// abstract interface.  Its implementations are either \ref
  /// tgba_representation "concrete representations", or \ref
  /// tgba_on_the_fly_algorithms "on-the-fly algorithms".  Other
  /// algorithms that work on spot::tgba are \ref tgba_algorithms
  /// "listed separately".

  /// \addtogroup tgba_essentials Essential TGBA types
  /// \ingroup tgba

  /// \ingroup tgba_essentials
45
  /// \brief A Transition-based Generalized Büchi Automaton.
46
47
48
49
50
51
52
53
  ///
  /// The acronym TGBA (Transition-based Generalized Büchi Automaton)
  /// was coined by Dimitra Giannakopoulou and Flavio Lerda
  /// in "From States to Transitions: Improving Translation of LTL
  /// Formulae to Büchi Automata".  (FORTE'02)
  ///
  /// TGBAs are transition-based, meanings their labels are put
  /// on arcs, not on nodes.  They use Generalized Büchi acceptance
54
  /// conditions: there are several acceptance sets (of
Alexandre Duret-Lutz's avatar
typos  
Alexandre Duret-Lutz committed
55
  /// transitions), and a path can be accepted only if it traverses
56
57
  /// at least one transition of each set infinitely often.
  ///
Alexandre Duret-Lutz's avatar
typos  
Alexandre Duret-Lutz committed
58
  /// Browsing such automaton can be achieved using two functions:
59
  /// \c get_init_state, and \c succ_iter.  The former returns
Alexandre Duret-Lutz's avatar
typos  
Alexandre Duret-Lutz committed
60
  /// the initial state while the latter lists the
61
62
63
64
65
66
  /// 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.
67
68
  class tgba
  {
69
70
  protected:
    tgba();
71

72
  public:
73
74
    virtual ~tgba();

75
76
77
    /// \brief Get the initial state of the automaton.
    ///
    /// The state has been allocated with \c new.  It is the
78
    /// responsability of the caller to \c destroy it when no
79
80
    /// longer needed.
    virtual state* get_init_state() const = 0;
81

82
    /// \brief Get an iterator over the successors of \a local_state.
83
84
85
86
87
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    ///
88
89
90
91
92
93
94
95
96
    /// During synchornized products, additional informations are
    /// passed about the entire product and its state.  Recall that
    /// products can be nested, forming a tree of spot::tgba where
    /// most values are computed on demand.  \a global_automaton
    /// designate the root spot::tgba, and \a global_state its
    /// state.  This two objects can be used by succ_iter() to
    /// restrict the set of successors to compute.
    ///
    /// \param local_state The state whose successors are to be explored.
97
    /// This pointer is not adopted in any way by \c succ_iter, and
98
    /// it is still the caller's responsability to destroy it when
99
100
    /// appropriate (this can be done during the lifetime of
    /// the iterator).
101
102
103
    /// \param global_state In a product, the state of the global
    /// product automaton.  Otherwise, 0.  Like \a locale_state,
    /// \a global_state is not adopted by \c succ_iter.
104
    /// \param global_automaton In a product, the global
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
    /// product automaton.  Otherwise, 0.
    virtual tgba_succ_iterator*
    succ_iter(const state* local_state,
	      const state* global_state = 0,
	      const tgba* global_automaton = 0) const = 0;

    /// \brief Get a formula that must hold whatever successor is taken.
    ///
    /// \return A formula which must be verified for all successors
    ///  of \a state.
    ///
    /// This can be as simple as \c bddtrue, or more completely
    /// the disjunction of the condition of all successors.  This
    /// is used as an hint by \c succ_iter() to reduce the number
    /// of successor to compute in a product.
    ///
    /// Sub classes should implement compute_support_conditions(),
    /// this function is just a wrapper that will cache the
    /// last return value for efficiency.
    bdd support_conditions(const state* state) const;

    /// \brief Get the conjunctions of variables tested by
    ///        the outgoing transitions of \a state.
    ///
    /// All variables tested by outgoing transitions must be
    /// returned.  This is mandatory.
    ///
    /// This is used as an hint by some \c succ_iter() to reduce the
    /// number of successor to compute in a product.
    ///
    /// Sub classes should implement compute_support_variables(),
    /// this function is just a wrapper that will cache the
    /// last return value for efficiency.
    bdd support_variables(const state* state) const;
139
140
141
142
143
144
145
146

    /// \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.
147
    virtual bdd_dict* get_dict() const = 0;
148
149
150
151

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

155
156
157
    /// \brief Return a possible annotation for the transition
    /// pointed to by the iterator.
    ///
158
159
160
161
162
    /// You may decide to use annotations when building a tgba class
    /// that represents the state space of a model, for instance to
    /// indicate how the tgba transitions relate to the original model
    /// (e.g. the annotation could be the name of a PetriNet
    /// transition, or the line number of some textual formalism).
163
    ///
164
165
166
167
168
169
170
    /// Implementing this method is optional; the default annotation
    /// is the empty string.
    ///
    /// This method is used for instance in dotty_reachable(),
    /// and replay_tgba_run().
    ///
    /// \param t a non-done tgba_succ_iterator for this automaton
171
172
173
    virtual std::string
    transition_annotation(const tgba_succ_iterator* t) const;

174
    /// \brief Project a state on an automaton.
175
176
177
178
179
180
181
182
183
184
185
    ///
    /// This converts \a s, into that corresponding spot::state for \a
    /// t.  This is useful when you have the state of a product, and
    /// want restrict this state to a specific automata occuring in
    /// the product.
    ///
    /// It goes without saying that \a s and \a t should be compatible
    /// (i.e., \a s is a state of \a t).
    ///
    /// \return 0 if the projection fails (\a s is unrelated to \a t),
    ///    or a new \c state* (the projected state) that must be
186
    ///    destroyed by the caller.
187
188
    virtual state* project_state(const state* s, const tgba* t) const;

189
    /// \brief Return the set of all acceptance conditions used
190
191
192
193
194
195
196
    /// 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.
197
    virtual bdd all_acceptance_conditions() const = 0;
198

199
    /// The number of acceptance conditions.
200
    virtual unsigned int number_of_acceptance_conditions() const;
201

202
    /// \brief Return the conjuction of all negated acceptance
203
    /// variables.
204
    ///
205
    /// For instance if the automaton uses variables <tt>Acc[a]</tt>,
206
    /// <tt>Acc[b]</tt> and <tt>Acc[c]</tt> to describe acceptance sets,
207
    /// this function should return <tt>!Acc[a]\&!Acc[b]\&!Acc[c]</tt>.
208
    ///
209
    /// This is useful when making products: each operand's condition
210
    /// set should be augmented with the neg_acceptance_conditions() of
211
    /// the other operand.
212
    virtual bdd neg_acceptance_conditions() const = 0;
213
214
215
216
217
218

  protected:
    /// Do the actual computation of tgba::support_conditions().
    virtual bdd compute_support_conditions(const state* state) const = 0;
    /// Do the actual computation of tgba::support_variables().
    virtual bdd compute_support_variables(const state* state) const = 0;
219
  protected:
220
221
    mutable const state* last_support_conditions_input_;
    mutable const state* last_support_variables_input_;
222
223
  private:
    mutable bdd last_support_conditions_output_;
224
    mutable bdd last_support_variables_output_;
225
    mutable int num_acc_;
226
  };
227

228
229
230
231
232
  /// \addtogroup tgba_representation TGBA representations
  /// \ingroup tgba

  /// \addtogroup tgba_algorithms TGBA algorithms
  /// \ingroup tgba
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250

  /// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms
  /// \ingroup tgba_algorithms

  /// \addtogroup tgba_io Input/Output of TGBA
  /// \ingroup tgba_algorithms

  /// \addtogroup tgba_ltl Translating LTL formulae into TGBA
  /// \ingroup tgba_algorithms

  /// \addtogroup tgba_generic Algorithm patterns
  /// \ingroup tgba_algorithms

  /// \addtogroup tgba_reduction TGBA simplifications
  /// \ingroup tgba_algorithms

  /// \addtogroup tgba_misc Miscellaneous algorithms on TGBA
  /// \ingroup tgba_algorithms
251
}
252
253

#endif // SPOT_TGBA_TGBA_HH