tgba.hh 11.3 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
#include "fwd.hh"
30 31 32

namespace spot
{
33 34 35
  class tgba_succ_iterator;

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

78
  public:
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

#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()
      {
106
	return it_->first() ? it_ : nullptr;
107 108 109 110 111 112 113 114 115
      }

      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
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
130
    virtual tgba_succ_iterator*
131
    succ_iter(const state* local_state) const = 0;
132

133
#ifndef SWIG
134 135 136 137
    /// \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>.
138
    succ_iterable
139 140 141 142
    succ(const state* s) const
    {
      return {this, succ_iter(s)};
    }
143 144 145 146 147 148 149 150 151 152 153 154 155
#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;
    }
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171

    /// \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;

172 173
    /// \brief Get the dictionary associated to the automaton.
    ///
174 175 176 177 178
    /// 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.
179
    virtual bdd_dict_ptr get_dict() const = 0;
180 181 182 183

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

187 188 189
    /// \brief Return a possible annotation for the transition
    /// pointed to by the iterator.
    ///
190 191 192 193 194
    /// 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).
195
    ///
196 197 198 199 200 201 202
    /// 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
203 204 205
    virtual std::string
    transition_annotation(const tgba_succ_iterator* t) const;

206
    /// \brief Project a state on an automaton.
207 208 209 210 211 212 213 214 215 216 217
    ///
    /// 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
218
    ///    destroyed by the caller.
219 220
    virtual state* project_state(const state* s,
				 const const_tgba_ptr& t) const;
221

222
    /// \brief Return the set of all acceptance conditions used
223 224 225 226 227 228 229
    /// 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.
230
    virtual bdd all_acceptance_conditions() const = 0;
231

232
    /// The number of acceptance conditions.
233
    virtual unsigned int number_of_acceptance_conditions() const;
234

235
    /// \brief Return the conjuction of all negated acceptance
236
    /// variables.
237
    ///
238
    /// For instance if the automaton uses variables <tt>Acc[a]</tt>,
239
    /// <tt>Acc[b]</tt> and <tt>Acc[c]</tt> to describe acceptance sets,
240
    /// this function should return <tt>!Acc[a]\&!Acc[b]\&!Acc[c]</tt>.
241
    ///
242
    /// This is useful when making products: each operand's condition
243
    /// set should be augmented with the neg_acceptance_conditions() of
244
    /// the other operand.
245
    virtual bdd neg_acceptance_conditions() const = 0;
246 247 248 249 250

  protected:
    /// Do the actual computation of tgba::support_conditions().
    virtual bdd compute_support_conditions(const state* state) const = 0;
    mutable const state* last_support_conditions_input_;
251 252
  private:
    mutable bdd last_support_conditions_output_;
253
    mutable int num_acc_;
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336

  protected:

    // Boolean properties.  Beware: true means that the property
    // holds, but false means the property is unknown.
    struct bprop
    {
      bool single_acc_set:1;	// A single acceptance set.
      bool state_based_acc:1;	// State-based acceptance.
      bool inherently_weak:1;	// Weak automaton.
      bool deterministic:1;	// Deterministic automaton.
    };
    union
    {
      unsigned props;
      bprop is;
    };

  public:

    bool has_single_acc_set() const
    {
      return is.single_acc_set;
    }

    void prop_single_acc_set(bool val = true)
    {
      is.single_acc_set = val;
    }

    bool has_state_based_acc() const
    {
      return is.state_based_acc;
    }

    void prop_state_based_acc(bool val = true)
    {
      is.state_based_acc = val;
    }

    bool is_sba() const
    {
      return has_state_based_acc() && has_single_acc_set();
    }

    bool is_inherently_weak() const
    {
      return is.inherently_weak;
    }

    void prop_inherently_weak(bool val = true)
    {
      is.inherently_weak = val;
    }

    bool is_deterministic() const
    {
      return is.deterministic;
    }

    void prop_deterministic(bool val = true)
    {
      is.deterministic = val;
    }

    // This is no default value here on purpose.  This way any time we
    // add a new property we cannot to update every call to prop_copy().
    void prop_copy(const const_tgba_ptr& other,
		   bool state_based,
		   bool single_acc,
		   bool inherently_weak,
		   bool deterministic)
    {
      if (state_based)
	prop_state_based_acc(other->has_state_based_acc());
      if (single_acc)
	prop_single_acc_set(other->has_single_acc_set());
      if (inherently_weak)
	prop_inherently_weak(other->is_inherently_weak());
      if (deterministic)
	prop_deterministic(other->is_deterministic());
    }

337
  };
338

339 340 341 342 343
  /// \addtogroup tgba_representation TGBA representations
  /// \ingroup tgba

  /// \addtogroup tgba_algorithms TGBA algorithms
  /// \ingroup tgba
344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361

  /// \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
362
}
363 364

#endif // SPOT_TGBA_TGBA_HH