succiterconcrete.hh 2.65 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

22
23
24
#ifndef SPOT_TGBA_SUCCITERCONCRETE_HH
# define SPOT_TGBA_SUCCITERCONCRETE_HH

25
#include "statebdd.hh"
26
27
28
29
30
#include "succiter.hh"
#include "tgbabddcoredata.hh"

namespace spot
{
31
  /// A concrete iterator over successors of a TGBA state.
32
33
34
  class tgba_succ_iterator_concrete: public tgba_succ_iterator
  {
  public:
35
    /// \brief Build a spot::tgba_succ_iterator_concrete.
36
    ///
37
    /// \param successors The set of successors with ingoing
38
    ///   conditions and acceptance conditions, represented as a BDD.
39
40
    ///   The job of this iterator will be to enumerate the
    ///   satisfactions of that BDD and split them into destination
41
    ///   states and conditions, and compute acceptance conditions.
42
    /// \param d The core data of the automata.
43
    ///   These contains sets of variables useful to split a BDD, and
44
    ///   compute acceptance conditions.
45
46
    tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors);
    virtual ~tgba_succ_iterator_concrete();
47

48
49
50
    // iteration
    void first();
    void next();
51
    bool done() const;
52

53
    // inspection
54
55
    state_bdd* current_state() const;
    bdd current_condition() const;
56
    bdd current_acceptance_conditions() const;
57

58
  private:
59
    const tgba_bdd_core_data& data_; ///< Core data of the automaton.
60
    bdd succ_set_;	///< The set of successors.
61
    bdd succ_set_left_;	///< Unexplored successors (including current_).
62
63
64
65
    bdd current_;	///< \brief Current successor, as a conjunction of
			///         atomic proposition and Next variables.
    bdd current_state_;	///< \brief Current successor, as a
			///         conjunction of Now variables.
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
66
67
    bdd current_acc_;   ///< \brief Accepting conditions for the current
			///         transition.
68
69
70
71
  };
}

#endif // SPOT_TGBA_SUCCITERCONCRETE_HH