tgba.hh 11.4 KB
Newer Older
1 2 3
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
5 6
// 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
7 8 9 10 11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13 14 15 16 17 18 19 20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23 24 25
#ifndef SPOT_TGBA_TGBA_HH
# define SPOT_TGBA_TGBA_HH

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

namespace spot
{
32 33 34
  class tgba_succ_iterator;

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

77
  public:
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115

#ifndef SWIG
    class succ_iterable
    {
    protected:
      const tgba* aut_;
      tgba_succ_iterator* it_;
    public:
      succ_iterable(const tgba* aut, tgba_succ_iterator* it)
	: aut_(aut), it_(it)
      {
      }

      succ_iterable(succ_iterable&& other)
	: aut_(other.aut_), it_(other.it_)
      {
	other.it_ = nullptr;
      }

      ~succ_iterable()
      {
	if (it_)
	  aut_->release_iter(it_);
      }

      internal::succ_iterator begin()
      {
	it_->first();
	return it_->done() ? nullptr : it_;
      }

      internal::succ_iterator end()
      {
	return nullptr;
      }
    };
#endif

116 117
    virtual ~tgba();

118 119 120
    /// \brief Get the initial state of the automaton.
    ///
    /// The state has been allocated with \c new.  It is the
121
    /// responsability of the caller to \c destroy it when no
122 123
    /// longer needed.
    virtual state* get_init_state() const = 0;
124

125
    /// \brief Get an iterator over the successors of \a local_state.
126 127 128 129 130
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    ///
131 132 133 134 135 136 137 138 139
    /// 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.
140
    /// This pointer is not adopted in any way by \c succ_iter, and
141
    /// it is still the caller's responsability to destroy it when
142 143
    /// appropriate (this can be done during the lifetime of
    /// the iterator).
144 145 146
    /// \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.
147
    /// \param global_automaton In a product, the global
148 149 150
    /// product automaton.  Otherwise, 0.
    virtual tgba_succ_iterator*
    succ_iter(const state* local_state,
151 152 153
	      const state* global_state = nullptr,
	      const tgba* global_automaton = nullptr) const = 0;

154
#ifndef SWIG
155 156 157 158
    /// \brief Build an iterable over the successors of \a s.
    ///
    /// This is meant to be used as
    /// <code>for (auto i: aut->out(s)) { /* i->current_state() */ }</code>.
159
    succ_iterable
160 161 162 163
    succ(const state* s) const
    {
      return {this, succ_iter(s)};
    }
164 165 166 167 168 169 170 171 172 173 174 175 176
#endif

    /// \brief Release an iterator after usage.
    ///
    /// This iterator can then be reused by succ_iter() to avoid
    /// memory allocation.
    void release_iter(tgba_succ_iterator* i) const
    {
      if (iter_cache_)
	delete i;
      else
	iter_cache_ = i;
    }
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205

    /// \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;
206 207 208

    /// \brief Get the dictionary associated to the automaton.
    ///
209 210 211 212 213
    /// Atomic propositions and acceptance conditions 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.
214
    virtual bdd_dict* get_dict() const = 0;
215 216 217 218

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

222 223 224
    /// \brief Return a possible annotation for the transition
    /// pointed to by the iterator.
    ///
225 226 227 228 229
    /// 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).
230
    ///
231 232 233 234 235 236 237
    /// 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
238 239 240
    virtual std::string
    transition_annotation(const tgba_succ_iterator* t) const;

241
    /// \brief Project a state on an automaton.
242 243 244 245 246 247 248 249 250 251 252
    ///
    /// 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
253
    ///    destroyed by the caller.
254 255
    virtual state* project_state(const state* s, const tgba* t) const;

256
    /// \brief Return the set of all acceptance conditions used
257 258 259 260 261 262 263
    /// 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.
264
    virtual bdd all_acceptance_conditions() const = 0;
265

266
    /// The number of acceptance conditions.
267
    virtual unsigned int number_of_acceptance_conditions() const;
268

269
    /// \brief Return the conjuction of all negated acceptance
270
    /// variables.
271
    ///
272
    /// For instance if the automaton uses variables <tt>Acc[a]</tt>,
273
    /// <tt>Acc[b]</tt> and <tt>Acc[c]</tt> to describe acceptance sets,
274
    /// this function should return <tt>!Acc[a]\&!Acc[b]\&!Acc[c]</tt>.
275
    ///
276
    /// This is useful when making products: each operand's condition
277
    /// set should be augmented with the neg_acceptance_conditions() of
278
    /// the other operand.
279
    virtual bdd neg_acceptance_conditions() const = 0;
280 281 282 283 284 285

  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;
286
  protected:
287 288
    mutable const state* last_support_conditions_input_;
    mutable const state* last_support_variables_input_;
289 290
  private:
    mutable bdd last_support_conditions_output_;
291
    mutable bdd last_support_variables_output_;
292
    mutable int num_acc_;
293
  };
294

295 296 297 298 299
  /// \addtogroup tgba_representation TGBA representations
  /// \ingroup tgba

  /// \addtogroup tgba_algorithms TGBA algorithms
  /// \ingroup tgba
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317

  /// \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
318
}
319 320

#endif // SPOT_TGBA_TGBA_HH