succiterconcrete.hh 2.93 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement de
3
// l'Epita (LRDE).
4
// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
6
7
8
9
10
11
// 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
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_SUCCITERCONCRETE_HH
# define SPOT_TGBA_SUCCITERCONCRETE_HH

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

namespace spot
{
32
  /// A concrete iterator over successors of a TGBA state.
33
  /// \ingroup tgba_representation
34
35
  class SPOT_API tgba_succ_iterator_concrete:
    public tgba_succ_iterator
36
37
  {
  public:
38
    /// \brief Build a spot::tgba_succ_iterator_concrete.
39
    ///
40
    /// \param successors The set of successors with ingoing
41
    ///   conditions and acceptance conditions, represented as a BDD.
42
43
    ///   The job of this iterator will be to enumerate the
    ///   satisfactions of that BDD and split them into destination
44
    ///   states and conditions, and compute acceptance conditions.
45
    /// \param d The core data of the automata.
46
    ///   These contains sets of variables useful to split a BDD, and
47
    ///   compute acceptance conditions.
48
49
50
51
52
53
54
55
56
57
58
59
60
    tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors)
      : data_(d)
    {
      recycle(successors);
    }

    void recycle(bdd successors)
    {
      succ_set_ = successors;
      succ_set_left_ = successors;
      current_ = bddfalse;
    }

61
    virtual ~tgba_succ_iterator_concrete();
62

63
64
65
    // iteration
    void first();
    void next();
66
    bool done() const;
67

68
    // inspection
69
70
    state_bdd* current_state() const;
    bdd current_condition() const;
71
    bdd current_acceptance_conditions() const;
72

73
  private:
74
    const tgba_bdd_core_data& data_; ///< Core data of the automaton.
75
    bdd succ_set_;	///< The set of successors.
76
    bdd succ_set_left_;	///< Unexplored successors (including current_).
77
78
79
80
    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.
81
    bdd current_acc_;   ///< \brief Acceptance conditions for the current
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
82
			///         transition.
83
84
85
86
  };
}

#endif // SPOT_TGBA_SUCCITERCONCRETE_HH